# HG changeset patch
# User wenzelm
# Date 1213647659 -7200
# Node ID df85326af57c244ab35be057042d20e641b173b1
# Parent  817d34377170800f58f5234c7b00c7ded6dfa64d
* Rules and tactics that read instantiations now demand a proper context;

diff -r 817d34377170 -r df85326af57c NEWS
--- a/NEWS	Mon Jun 16 22:13:54 2008 +0200
+++ b/NEWS	Mon Jun 16 22:20:59 2008 +0200
@@ -53,6 +53,15 @@
 theorems.  Changes in simp rules.  INCOMPATIBILITY.
 
 
+*** ML ***
+
+* Rules and tactics that read instantiations (read_instantiate,
+res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
+context, which is required for parsing and type-checking.  Moreover,
+the variables are specified as plain indexnames, not string encodings
+thereof.  INCOMPATIBILITY.
+
+
 
 New in Isabelle2008 (June 2008)
 -------------------------------