--- a/NEWS Sun Oct 21 12:33:12 2007 +0200
+++ b/NEWS Sun Oct 21 14:21:44 2007 +0200
@@ -109,37 +109,15 @@
*** Pure ***
-* Class-context aware syntax for class target ("user space type system"):
-Local operations in class context (fixes, definitions, axiomatizations,
-abbreviations) are identified with their global counterparts during reading and
-printing of terms. Practically, this allows to use the same syntax for
-both local *and* global operations. Syntax declarations referring directly to
-local fixes, definitions, axiomatizations and abbreviations are applied to their
-global counterparts instead (but explicit notation declarations still are local);
-the special treatment of \<^loc> in local syntax declarations has been abandoned.
-INCOMPATIBILITY. Most affected theories shall work after the following
-purgatory:
-
- perl -i -pe 's/\\<\^loc>//g;' THYFILENAME1 THYFILENAME2 ...
-
-Current limitations:
-- printing of local abbreviations sometimes yields unexpected results.
-- some facilities (e.g. attribute of, legacy tac-methods) still do not use
-canonical interfaces for printing and reading terms.
-
-* Code generator: consts in 'consts_code' Isar commands are now
-referred to by usual term syntax (including optional type
-annotations).
-
-* Code generator: basic definitions (from 'definition', 'constdefs',
-or primitive 'instance' definitions) are added automatically to the
-table of defining equations. Primitive defs are not used as defining
-equations by default any longer. Defining equations are now definitly
-restricted to meta "==" and object equality "=".
-
* The 'class' package offers a combination of axclass and locale to
-achieve Haskell-like type classes in Isabelle. See
-HOL/ex/Classpackage.thy for examples.
+achieve Haskell-like type classes in Isabelle. Definitions and
+theorems within a class context produce both relative results (with
+implicit parameters according to the locale context), and polymorphic
+constants with qualified polymorphism (according to the class
+context). Within the body context of a 'class' target, a separate
+syntax layer ("user space type system") takes care of converting
+between global polymorphic consts and internal locale representation.
+See HOL/ex/Classpackage.thy for examples (as well as main HOL).
* Yet another code generator framework allows to generate executable
code for ML and Haskell (including Isabelle classes). A short usage
@@ -186,6 +164,16 @@
generation from Isabelle/HOL theories is available via "isatool doc
codegen".
+* Code generator: consts in 'consts_code' Isar commands are now
+referred to by usual term syntax (including optional type
+annotations).
+
+* Code generator: basic definitions (from 'definition', 'constdefs',
+or primitive 'instance' definitions) are added automatically to the
+table of defining equations. Primitive defs are not used as defining
+equations by default any longer. Defining equations are now definitly
+restricted to meta "==" and object equality "=".
+
* Command 'no_translations' removes translation rules from theory
syntax.
@@ -562,17 +550,30 @@
*** HOL ***
-* localized monotonicity predicate in theory "Orderings";
-integrated lemmas max_of_mono and min_of_mono with this predicate.
+* Method "metis" proves goals by applying the Metis general-purpose
+resolution prover (see also http://gilith.com/software/metis/).
+Examples are in the directory MetisExamples. WARNING: the
+Isabelle/HOL-Metis integration does not yet work properly with
+multi-threading.
+
+* Command 'sledgehammer' invokes external automatic theorem provers as
+background processes. It generates calls to the "metis" method if
+successful. These can be pasted into the proof. Users do not have to
+wait for the automatic provers to return. WARNING: does not really
+work with multi-threading.
+
+* Localized monotonicity predicate in theory "Orderings"; integrated
+lemmas max_of_mono and min_of_mono with this predicate.
INCOMPATIBILITY.
-* class "div" now inherits from class "times" rather than "type".
+* Class "div" now inherits from class "times" rather than "type".
INCOMPATIBILITY.
* New "auto_quickcheck" feature tests outermost goal statements for
potential counter-examples. Controlled by ML references
auto_quickcheck (default true) and auto_quickcheck_time_limit (default
-5000 milliseconds).
+5000 milliseconds). Fails silently if statements is outside of
+executable fragment, or any other codgenerator problem occurs.
* Internal reorganisation of `size' of datatypes: size theorems
"foo.size" are no longer subsumed by "foo.simps" (but are still
@@ -595,6 +596,8 @@
Linorder etc. have disappeared; operations defined in terms of
fold_set now are named Inf_fin, Sup_fin. INCOMPATIBILITY.
+* HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY.
+
* HOL-Word: New extensive library and type for generic, fixed size
machine words, with arithemtic, bit-wise, shifting and rotating
operations, reflection into int, nat, and bool lists, automation for
@@ -724,18 +727,6 @@
sets or predicates are now called "p_1.cases" ... "p_k.cases". The
list of rules "p_1_..._p_k.elims" is no longer available.
-* Method "metis" proves goals by applying the Metis general-purpose
-resolution prover. Examples are in the directory MetisExamples. See
-also http://gilith.com/software/metis/
-
-WARNING: the Isabelle/HOL-Metis integration does not yet work properly
-with multi-threading.
-
-* Command 'sledgehammer' invokes external automatic theorem provers as
-background processes. It generates calls to the "metis" method if
-successful. These can be pasted into the proof. Users do not have to
-wait for the automatic provers to return.
-
* Case-expressions allow arbitrary constructor-patterns (including
"_") and take their order into account, like in functional
programming. Internally, this is translated into nested