diff -r 70fa52503cf3 -r 69982744c427 NEWS --- 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 - _ $ _ ~> _ $$ _ - \ x. _ ~> \\ 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 + _ $ _ ~> _ $$ _ + \ x. _ ~> \\ 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