# HG changeset patch
# User wenzelm
# Date 1438012568 -7200
# Node ID 067658d63c5d6c6168148c6df38e1f678438596d
# Parent  7664e0916eec4e8f8b462426287200196952eeba
NEWS;

diff -r 7664e0916eec -r 067658d63c5d 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).