# HG changeset patch
# User wenzelm
# Date 1635501469 -7200
# Node ID e495ab64c6949e14aec203b642b6705d516b7125
# Parent  43142ac556e65e1ff770044a6cc0c1b817ed5baa
added Thm.instantiate_beta;
tuned;

diff -r 43142ac556e6 -r e495ab64c694 NEWS
--- a/NEWS	Thu Oct 28 06:39:36 2021 +0000
+++ b/NEWS	Fri Oct 29 11:57:49 2021 +0200
@@ -340,9 +340,39 @@
 adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
 accumulation of items.
 
-* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
-corresponding functions for the object-logic of the ML compilation
-context. This supersedes older mk_Trueprop / dest_Trueprop operations.
+* Thm.instantiate_beta applies newly emerging abstractions to their
+arguments in the term, but leaves other beta-redexes unchanged --- in
+contrast to Drule.instantiate_normalize.
+
+* ML antiquotation "instantiate" allows to instantiate formal entities
+(types, terms, theorems) with values given ML. This works uniformly for
+"typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a
+keyword after the instantiation.
+
+A mode "(schematic)" behind the keyword means that some variables may
+remain uninstantiated (fixed in the specification and schematic in the
+result); by default, all variables need to be instantiated.
+
+Newly emerging abstractions are applied to their arguments in the term
+(using Thm.instantiate_beta).
+
+Examples in HOL:
+
+  fun make_assoc_type (A, B) =
+    \<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>;
+
+  val make_assoc_list =
+    map (fn (x, y) =>
+      \<^instantiate>\<open>'a = \<open>fastype_of x\<close> and 'b = \<open>fastype_of y\<close> and
+        x and y in term \<open>(x, y)\<close> for x :: 'a and y :: 'b\<close>);
+
+  fun symmetry x y =
+    \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y in
+      lemma \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
+
+  fun symmetry_schematic A =
+    \<^instantiate>\<open>'a = A in
+      lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
 
 * ML antiquotations for type constructors and term constants:
 
@@ -373,31 +403,9 @@
   fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
   val dest_eq = \<^Const_fn>\<open>HOL.eq T for t u => \<open>(T, (t, u))\<close>\<close>;
 
-* ML antiquotation "instantiate" allows to instantiate formal entities
-(types, terms, theorems) with values given ML. This works uniformly for
-"typ", "term", "prop", "ctyp", "cterm", "cprop", "lemma" --- given as a
-keyword after the instantiation. A mode "(schematic)" behind the keyword
-means that some variables may remain uninstantiated (fixed in the
-specification and schematic in the result); by default, all variables
-need to be instantiated.
-
-Examples in HOL:
-
-  fun make_assoc_type (A, B) =
-    \<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>;
-
-  val make_assoc_list =
-    map (fn (x, y) =>
-      \<^instantiate>\<open>'a = \<open>fastype_of x\<close> and 'b = \<open>fastype_of y\<close> and
-        x and y in term \<open>(x, y)\<close> for x :: 'a and y :: 'b\<close>);
-
-  fun symmetry x y =
-    \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm x\<close> and x and y in
-      lemma \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
-
-  fun symmetry_schematic A =
-    \<^instantiate>\<open>'a = A in
-      lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>
+* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
+corresponding functions for the object-logic of the ML compilation
+context. This supersedes older mk_Trueprop / dest_Trueprop operations.
 
 * The "build" combinators of various data structures help to build
 content from bottom-up, by applying an "add" function the "empty" value.