--- a/NEWS Sun Jan 16 19:45:42 2011 +0100
+++ b/NEWS Sun Jan 16 20:54:30 2011 +0100
@@ -12,6 +12,13 @@
* Significantly improved Isabelle/Isar implementation manual.
+* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
+(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
+while the default heap location within that directory lacks that extra
+suffix. This isolates multiple Isabelle installations from each
+other, avoiding problems with old settings in new versions.
+INCOMPATIBILITY, need to copy/upgrade old user settings manually.
+
* Source files are always encoded as UTF-8, instead of old-fashioned
ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require
the following package declarations:
@@ -27,16 +34,11 @@
consistent view on symbols, while raw explode (or String.explode)
merely give a byte-oriented representation.
-* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
-(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
-while the default heap location within that directory lacks that extra
-suffix. This isolates multiple Isabelle installations from each
-other, avoiding problems with old settings in new versions.
-INCOMPATIBILITY, need to copy/upgrade old user settings manually.
-
-* Theory loading: only the master source file is looked-up in the
-implicit load path, all other files are addressed relatively to its
-directory. Minor INCOMPATIBILITY, subtle change in semantics.
+* Theory loader: source files are primarily located via the master
+directory of each theory node (where the .thy file itself resides).
+The global load path is still partially available as legacy feature.
+Minor INCOMPATIBILITY due to subtle change in file lookup: use
+explicit paths, relatively to the theory.
* Special treatment of ML file names has been discontinued.
Historically, optional extensions .ML or .sml were added on demand --
@@ -88,15 +90,15 @@
floating-point notation that coincides with the inner syntax for
float_token.
-* Theory loader: implicit load path is considered legacy. Use
-explicit file specifications instead, relatively to the directory of
-the enclosing theory file.
-
-* Discontinued support for Poly/ML 5.0 and 5.1 versions.
+* Support for real valued preferences (with approximative PGIP type):
+front-ends need to accept "pgint" values in float notation.
+INCOMPATIBILITY.
* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
DejaVu Sans.
+* Discontinued support for Poly/ML 5.0 and 5.1 versions.
+
*** Pure ***
@@ -110,17 +112,15 @@
* Command 'notepad' replaces former 'example_proof' for
experimentation in Isar without any result. INCOMPATIBILITY.
-* Support for real valued preferences (with approximative PGIP type).
-
* Locale interpretation commands 'interpret' and 'sublocale' accept
lists of equations to map definitions in a locale to appropriate
entities in the context of the interpretation. The 'interpretation'
command already provided this functionality.
-* New diagnostic command 'print_dependencies' prints the locale
-instances that would be activated if the specified expression was
-interpreted in the current context. Variant 'print_dependencies!'
-assumes a context without interpretations.
+* Diagnostic command 'print_dependencies' prints the locale instances
+that would be activated if the specified expression was interpreted in
+the current context. Variant "print_dependencies!" assumes a context
+without interpretations.
* Diagnostic command 'print_interps' prints interpretations in proofs
in addition to interpretations in theories.
@@ -135,8 +135,8 @@
* The "prems" fact, which refers to the accidental collection of
foundational premises in the context, is now explicitly marked as
-legacy feature and will be discontinued eventually. Consider using
-"assms" of the head statement or reference facts by explicit names.
+legacy feature and will be discontinued soon. Consider using "assms"
+of the head statement or reference facts by explicit names.
* Document antiquotations @{class} and @{type} print classes and type
constructors.
@@ -147,16 +147,10 @@
*** HOL ***
-* Simproc "list_to_set_comprehension" rewrites list comprehensions
-applied to List.set to set comprehensions. Occasional
-INCOMPATIBILITY, may be deactivated like this:
-
- declare [[simproc del: list_to_set_comprehension]]
-
-* Functions can be declared as coercions and type inference will add
-them as necessary upon input of a term. Theory Complex_Main declares
-real :: nat => real and real :: int => real as coercions. A coercion
-function f is declared like this:
+* Coercive subtyping: functions can be declared as coercions and type
+inference will add them as necessary upon input of a term. Theory
+Complex_Main declares real :: nat => real and real :: int => real as
+coercions. A coercion function f is declared like this:
declare [[coercion f]]
@@ -179,25 +173,25 @@
src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy
for examples.
-* Scala (2.8 or higher) has been added to the target languages of the
-code generator.
-
-* Inductive package: now offers command 'inductive_simps' to
-automatically derive instantiated and simplified equations for
-inductive predicates, similar to 'inductive_cases'.
-
* Function package: f.psimps rules are no longer implicitly declared
as [simp]. INCOMPATIBILITY.
* Datatype package: theorems generated for executable equality (class
"eq") carry proper names and are treated as default code equations.
+* Inductive package: now offers command 'inductive_simps' to
+automatically derive instantiated and simplified equations for
+inductive predicates, similar to 'inductive_cases'.
+
* Command 'enriched_type' allows to register properties of the
functorial structure of types.
* Improved infrastructure for term evaluation using code generator
techniques, in particular static evaluation conversions.
+* Code generator: Scala (2.8 or higher) has been added to the target
+languages.
+
* Code generator: globbing constant expressions "*" and "Theory.*"
have been replaced by the more idiomatic "_" and "Theory._".
INCOMPATIBILITY.
@@ -208,14 +202,10 @@
* Code generator: do not print function definitions for case
combinators any longer.
-* Simplification with rules determined by code generator with
+* Code generator: simplification with rules determined with
src/Tools/Code/code_simp.ML and method "code_simp".
-* Records: logical foundation type for records does not carry a
-'_type' suffix any longer (obsolete due to authentic syntax).
-INCOMPATIBILITY.
-
-* Code generation for records: more idiomatic representation of record
+* Code generator for records: more idiomatic representation of record
types. Warning: records are not covered by ancient SML code
generation any longer. INCOMPATIBILITY. In cases of need, a suitable
rep_datatype declaration helps to succeed then:
@@ -224,6 +214,10 @@
...
rep_datatype foo_ext ...
+* Records: logical foundation type for records does not carry a
+'_type' suffix any longer (obsolete due to authentic syntax).
+INCOMPATIBILITY.
+
* Quickcheck now by default uses exhaustive testing instead of random
testing. Random testing can be invoked by "quickcheck [random]",
exhaustive testing by "quickcheck [exhaustive]".
@@ -314,56 +308,14 @@
* Boogie output files (.b2i files) need to be declared in the theory
header.
+* Simplification procedure "list_to_set_comprehension" rewrites list
+comprehensions applied to List.set to set comprehensions. Occasional
+INCOMPATIBILITY, may be deactivated like this:
+
+ declare [[simproc del: list_to_set_comprehension]]
+
* Removed old version of primrec package. INCOMPATIBILITY.
-* Multivariate Analysis: Introduced a type class for euclidean
-space. Most theorems are now stated in terms of euclidean spaces
-instead of finite cartesian products.
-
- types
- real ^ 'n ~> 'a::real_vector
- ~> 'a::euclidean_space
- ~> 'a::ordered_euclidean_space
- (depends on your needs)
-
- constants
- _ $ _ ~> _ $$ _
- \<chi> x. _ ~> \<chi>\<chi> x. _
- CARD('n) ~> DIM('a)
-
-Also note that the indices are now natural numbers and not from some
-finite type. Finite cartesian products of euclidean spaces, products
-of euclidean spaces the real and complex numbers are instantiated to
-be euclidean_spaces. INCOMPATIBILITY.
-
-* Session Probability: Introduced pextreal as positive extended real
-numbers. Use pextreal as value for measures. Introduce the
-Radon-Nikodym derivative, product spaces and Fubini's theorem for
-arbitrary sigma finite measures. Introduces Lebesgue measure based on
-the integral in Multivariate Analysis. INCOMPATIBILITY.
-
-* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
-INCOMPATIBILITY.
-
-* Theory Library/Monad_Syntax provides do-syntax for monad types.
-Syntax in Library/State_Monad has been changed to avoid ambiguities.
-INCOMPATIBILITY.
-
-* Theory SetsAndFunctions has been split into Function_Algebras and
-Set_Algebras; canonical names for instance definitions for functions;
-various improvements. INCOMPATIBILITY.
-
-* Theory Library/Multiset provides stable quicksort implementation of
-sort_key.
-
-* Former theory Library/Enum is now part of the HOL-Main image.
-INCOMPATIBILITY: all constants of the Enum theory now have to be
-referred to by its qualified name.
-
- enum ~> Enum.enum
- nlists ~> Enum.nlists
- product ~> Enum.product
-
* Removed simplifier congruence rule of "prod_case", as has for long
been the case with "split". INCOMPATIBILITY.
@@ -390,9 +342,6 @@
* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
avoid confusion with finite sets. INCOMPATIBILITY.
-* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
-INCOMPATIBILITY.
-
* Abandoned locales equiv, congruent and congruent2 for equivalence
relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same
for congruent(2)).
@@ -488,8 +437,61 @@
* Removed lemma "Option.is_none_none" which duplicates "is_none_def".
INCOMPATIBILITY.
-* New commands to load and prove verification conditions generated by
-the SPARK Ada program verifier. See src/HOL/SPARK.
+* Former theory Library/Enum is now part of the HOL-Main image.
+INCOMPATIBILITY: all constants of the Enum theory now have to be
+referred to by its qualified name.
+
+ enum ~> Enum.enum
+ nlists ~> Enum.nlists
+ product ~> Enum.product
+
+* Theory Library/Monad_Syntax provides do-syntax for monad types.
+Syntax in Library/State_Monad has been changed to avoid ambiguities.
+INCOMPATIBILITY.
+
+* Theory Library/SetsAndFunctions has been split into
+Library/Function_Algebras and Library/Set_Algebras; canonical names
+for instance definitions for functions; various improvements.
+INCOMPATIBILITY.
+
+* Theory Library/Multiset provides stable quicksort implementation of
+sort_key.
+
+* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
+INCOMPATIBILITY.
+
+* Session Multivariate_Analysis: introduced a type class for euclidean
+space. Most theorems are now stated in terms of euclidean spaces
+instead of finite cartesian products.
+
+ types
+ real ^ 'n ~> 'a::real_vector
+ ~> 'a::euclidean_space
+ ~> 'a::ordered_euclidean_space
+ (depends on your needs)
+
+ constants
+ _ $ _ ~> _ $$ _
+ \<chi> x. _ ~> \<chi>\<chi> x. _
+ CARD('n) ~> DIM('a)
+
+Also note that the indices are now natural numbers and not from some
+finite type. Finite cartesian products of euclidean spaces, products
+of euclidean spaces the real and complex numbers are instantiated to
+be euclidean_spaces. INCOMPATIBILITY.
+
+* Session Probability: introduced pextreal as positive extended real
+numbers. Use pextreal as value for measures. Introduce the
+Radon-Nikodym derivative, product spaces and Fubini's theorem for
+arbitrary sigma finite measures. Introduces Lebesgue measure based on
+the integral in Multivariate Analysis. INCOMPATIBILITY.
+
+* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
+INCOMPATIBILITY.
+
+* Session SPARK (with image HOL-SPARK) provides commands to load and
+prove verification conditions generated by the SPARK Ada program
+verifier. See also src/HOL/SPARK and src/HOL/SPARK/Examples.
*** HOL-Algebra ***
@@ -688,8 +690,17 @@
*** ML ***
-* Renamed structure MetaSimplifier to Raw_Simplifier. Note that the
-main functionality is provided by structure Simplifier.
+* Antiquotation @{assert} inlines a function bool -> unit that raises
+Fail if the argument is false. Due to inlining the source position of
+failed assertions is included in the error output.
+
+* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
+text is in practice always evaluated with a stable theory checkpoint.
+Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
+
+* Antiquotation @{theory A} refers to theory A from the ancestry of
+the current context, not any accidental theory loader state as before.
+Potential INCOMPATIBILITY, subtle change in semantics.
* Syntax.pretty_priority (default 0) configures the required priority
of pretty-printed output and thus affects insertion of parentheses.
@@ -700,6 +711,9 @@
* Former exception Library.UnequalLengths now coincides with
ListPair.UnequalLengths.
+* Renamed structure MetaSimplifier to Raw_Simplifier. Note that the
+main functionality is provided by structure Simplifier.
+
* Renamed raw "explode" function to "raw_explode" to emphasize its
meaning. Note that internally to Isabelle, Symbol.explode is used in
almost all situations.
@@ -708,14 +722,6 @@
See implementation manual for further details on exceptions in
Isabelle/ML.
-* Antiquotation @{assert} inlines a function bool -> unit that raises
-Fail if the argument is false. Due to inlining the source position of
-failed assertions is included in the error output.
-
-* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
-text is in practice always evaluated with a stable theory checkpoint.
-Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
-
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
meaning.
@@ -733,17 +739,12 @@
INCOMPATIBILITY, superseded by static antiquotations @{thm} and
@{thms} for most purposes.
-* ML structure Unsynchronized never opened, not even in Isar
+* ML structure Unsynchronized is never opened, not even in Isar
interaction mode as before. Old Unsynchronized.set etc. have been
discontinued -- use plain := instead. This should be *rare* anyway,
since modern tools always work via official context data, notably
configuration options.
-* ML antiquotations @{theory} and @{theory_ref} refer to named
-theories from the ancestry of the current context, not any accidental
-theory loader state as before. Potential INCOMPATIBILITY, subtle
-change in semantics.
-
* Parallel and asynchronous execution requires special care concerning
interrupts. Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt. User code must not absorb