--- a/NEWS Fri Aug 29 15:19:02 2003 +0200
+++ b/NEWS Fri Aug 29 15:40:11 2003 +0200
@@ -17,6 +17,22 @@
symbols. Call 'isatool fixgreek' to try to fix parsing errors in
existing theory and ML files.
+*** Isar ***
+
+* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
+
+ - Now understand static (Isar) contexts. As a consequence, users of Isar
+ locales are no longer forced to write Isar proof scripts.
+ For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
+ emulations.
+ - INCOMPATIBILITY: names of variables to be instantiated may no
+ longer be enclosed in quotes. Instead, precede variable names containing
+ dots with `?'. This is consistent with the instantiation attribute
+ "where".
+
+* HOL: Tactic emulation methods induct_tac and case_tac understand static
+ (Isar) contexts.
+
*** HOL ***
* 'specification' command added, allowing for definition by