--- a/NEWS Wed Jun 30 00:42:59 2004 +0200
+++ b/NEWS Wed Jun 30 14:04:58 2004 +0200
@@ -96,6 +96,11 @@
the old record representation. The type generated for a record is
called <record_name>_ext_type.
+* HOL/record: Reference record_definition_quick_and_dirty_sensitive
+ can be enabled to skip the proofs triggered by a record definition
+ (if quick_and_dirty is enabled). Definitions of large records can
+ take quite long.
+
* HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
syntax (epsilon)