NEWS
changeset 14254 342634f38451
parent 14243 0e2ec694784d
child 14255 e6e3e3f0deed
     1.1 --- a/NEWS	Fri Oct 31 06:54:22 2003 +0100
     1.2 +++ b/NEWS	Thu Nov 06 14:18:05 2003 +0100
     1.3 @@ -48,6 +48,8 @@
     1.4      Resolve particular premise with <locale>.intro to obtain old form.
     1.5    - Fixed bug in type inference ("unify_frozen") that prevented mix of target
     1.6      specification and "includes" elements in goal statement.
     1.7 +  - Rule sets <locale>.intro and <locale>.axioms no longer declared as
     1.8 +    [intro?] and [elim?] (respectively) by default.
     1.9  
    1.10  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.11    (Isar) contexts.