# HG changeset patch
# User ballarin
# Date 1064927258 -7200
# Node ID 7286c187596d8a7528267ed18b21ef0d3a7ce71e
# Parent  69e48401da98915d8a50c2ca4d3cd04023c84513
Improvements to Isar/Locales:  premises generated by "includes" elements
changed.  Bugfix "unify_frozen".

diff -r 69e48401da98 -r 7286c187596d NEWS
--- a/NEWS	Fri Sep 26 11:08:18 2003 +0200
+++ b/NEWS	Tue Sep 30 15:07:38 2003 +0200
@@ -20,15 +20,21 @@
 *** 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".
+    longer be enclosed in quotes.  Instead, precede variable name with `?'.
+    This is consistent with the instantiation attribute "where".
+
+* Locales:
+  - Goal statements involving the context element "includes" no longer
+    generate theorems with internal delta predicates (those ending on
+    "_axioms") in the premise.
+    Resolve particular premise with <locale>.intro to obtain old form.
+  - Fixed bug in type inference ("unify_frozen") that prevented mix of target
+    specification and "includes" elements in goal statement.
 
 * HOL: Tactic emulation methods induct_tac and case_tac understand static
   (Isar) contexts.