<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>