--- a/NEWS Fri Oct 31 06:54:22 2003 +0100
+++ b/NEWS Thu Nov 06 14:18:05 2003 +0100
@@ -48,6 +48,8 @@
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.
+ - Rule sets <locale>.intro and <locale>.axioms no longer declared as
+ [intro?] and [elim?] (respectively) by default.
* HOL: Tactic emulation methods induct_tac and case_tac understand static
(Isar) contexts.