NEWS;
authorwenzelm
Mon, 27 Jul 2015 17:56:08 +0200
changeset 60802 067658d63c5d
parent 60801 7664e0916eec
child 60803 e11f47dd0786
NEWS;
NEWS
--- a/NEWS	Mon Jul 27 17:44:55 2015 +0200
+++ b/NEWS	Mon Jul 27 17:56:08 2015 +0200
@@ -246,6 +246,18 @@
 
 *** ML ***
 
+* Instantiation rules have been re-organized as follows:
+
+  Thm.instantiate  (*low-level instantiation with named arguments*)
+  Thm.instantiate' (*version with positional arguments*)
+
+  Drule.infer_instantiate  (*instantiation with type inference*)
+  Drule.infer_instantiate'  (*version with positional arguments*)
+
+The LHS only requires variable specifications, instead of full terms.
+Old cterm_instantiate is superseded by infer_instantiate.
+INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
+
 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been
 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
 instead (with proper context).