
<html xmlns="http://www.w3.org/1999/xhtml">


<head>


<meta http-equiv="Content-Type" content="text/html; charset=utf-8">


<title></title>


</head>


<body>


<div name="messageBodySection">


<div dir="auto">Thanks for the suggestion and code. I wonder however how common it is to normalise a theorem wrt an environment. Environments are an internal data structure largely tied up with unification and not used to that much outside the kernel.</div>


</div>


<div name="messageSignatureSection"><br>


<div class="matchFont">


<div dir="auto">Larry Paulson</div>


</div>


</div>


<div name="messageReplySection">On 28 Sep 2021, 11:19 +0100, Kevin Kappelmann <kevin.kappelmann@tum.de>, wrote:<br>


<blockquote type="cite" style="border-left-color: grey; border-left-width: thin; border-left-style: solid; margin: 5px 5px;padding-left: 10px;">


<br>


<div>I see that there are functions to normalise a type (Envir.norm_type) and<br>


a term (Envir.norm_term) wrt an environment. Is there also a function to<br>


normalise a theorem wrt an environment? If not, I think doing such a<br>


normalisation is very common and should be added to Isabelle/Pure.<br>


<br>


Attached, find my proposal for such a function (norm_thm) and some<br>


examples why a simpler alternative (that is akin to the function<br>


described in the Isabelle/ML cookbook [1, page 57]) does not work. The<br>


file compiles using the current Isabelle development version.<br>


</div>


</blockquote>


</div>


</body>


</html>