NEWS
changeset 14556 c5078f6c99a9
parent 14551 2cb6ff394bfb
child 14561 c53396af770e
     1.1 --- a/NEWS	Tue Apr 13 20:22:26 2004 +0200
     1.2 +++ b/NEWS	Tue Apr 13 20:31:55 2004 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    Replaces linorder.ML.
     1.5  
     1.6  * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
     1.7 -  (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler
     1.8 +  (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and euler
     1.9    (\<a>...\<z>), are now considered normal letters, and can therefore
    1.10    be used anywhere where an ASCII letter (a...zA...Z) has until
    1.11    now. COMPATIBILITY: This obviously changes the parsing of some
    1.12 @@ -54,6 +54,7 @@
    1.13    (somewhat) independet of content. It is copied from lib/html/isabelle.css. 
    1.14    It can be changed to alter the colors/layout of generated pages.
    1.15  
    1.16 +
    1.17  *** Isar ***
    1.18  
    1.19  * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
    1.20 @@ -72,8 +73,9 @@
    1.21      theorems to have too special types in some circumstances.
    1.22    - "where" permits explicit instantiations of type variables.
    1.23  
    1.24 -* Calculation commands "moreover" and "also":
    1.25 -  Do not reset facts ("this") any more.
    1.26 +* Calculation commands "moreover" and "also" no longer interfere with
    1.27 +  current facts ("this"), admitting arbitrary combinations with "then"
    1.28 +  and derived forms.
    1.29  
    1.30  * Locales:
    1.31    - Goal statements involving the context element "includes" no longer
    1.32 @@ -100,6 +102,7 @@
    1.33  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.34    (Isar) contexts.
    1.35  
    1.36 +
    1.37  *** HOL ***
    1.38  
    1.39  * Simplifier: