NEWS
changeset 15012 28fa57b57209
parent 15011 35be762f58f9
child 15018 0a84ca4e0f90
     1.1 --- a/NEWS	Wed Jun 30 00:42:59 2004 +0200
     1.2 +++ b/NEWS	Wed Jun 30 14:04:58 2004 +0200
     1.3 @@ -96,6 +96,11 @@
     1.4    the old record representation. The type generated for a record is
     1.5    called <record_name>_ext_type.
     1.6  
     1.7 +* HOL/record: Reference record_definition_quick_and_dirty_sensitive
     1.8 +  can be enabled to skip the proofs triggered by a record definition
     1.9 +  (if quick_and_dirty is enabled). Definitions of large records can
    1.10 +  take quite long.
    1.11 +
    1.12  * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
    1.13  
    1.14    syntax (epsilon)