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