NEWS
changeset 15018 0a84ca4e0f90
parent 15012 28fa57b57209
child 15022 9a9a79fb33ee
     1.1 --- a/NEWS	Tue Jul 06 20:32:20 2004 +0200
     1.2 +++ b/NEWS	Tue Jul 06 20:34:49 2004 +0200
     1.3 @@ -42,6 +42,14 @@
     1.4    'nonterminals' rather than 'types'.  INCOMPATIBILITY for new
     1.5    object-logic specifications.
     1.6  
     1.7 +* Pure/Tactic: print_tac now outputs the goal through the trace 
     1.8 +  channel.
     1.9 +
    1.10 +* Pure/Namespace: reference Namespace.unique_names included.
    1.11 +  If true the (shortest) namespace-prefix is printed to disambiguate 
    1.12 +  conflicts (as yet). If false the first entry wins (as during 
    1.13 +  parsing). Default value is true.
    1.14 +
    1.15  * Pure/Syntax: inner syntax includes (*(*nested*) comments*).
    1.16  
    1.17  * Pure/Syntax: pretty pinter now supports unbreakable blocks,
    1.18 @@ -96,9 +104,9 @@
    1.19    the old record representation. The type generated for a record is
    1.20    called <record_name>_ext_type.
    1.21  
    1.22 -* HOL/record: Reference record_definition_quick_and_dirty_sensitive
    1.23 +* HOL/record: Reference record_quick_and_dirty_sensitive
    1.24    can be enabled to skip the proofs triggered by a record definition
    1.25 -  (if quick_and_dirty is enabled). Definitions of large records can
    1.26 +  or a simproc (if quick_and_dirty is enabled). Definitions of large records can
    1.27    take quite long.
    1.28  
    1.29  * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
    1.30 @@ -112,9 +120,10 @@
    1.31    \<epsilon> becomes available as variable, constant etc.
    1.32  
    1.33  * Simplifier: "record_upd_simproc" for simplification of multiple
    1.34 -  record updates enabled by default.  INCOMPATIBILITY: old proofs
    1.35 -  break occasionally, since simplification is more powerful by
    1.36 -  default.
    1.37 +  record updates enabled by default. Moreover trivial updates are
    1.38 +  also removed: r(|x := x r|) = r. 
    1.39 +  INCOMPATIBILITY: old proofs break occasionally, since simplification 
    1.40 +  is more powerful by default.
    1.41  
    1.42  
    1.43  *** HOLCF ***