# HG changeset patch # User wenzelm # Date 1291410494 -3600 # Node ID ad8535384c340c6204dc9dd4644a0eb53ca38ddd # Parent 58fa450b05e1ab340478c5e5806ef9158cad695f minor tuning for release; diff -r 58fa450b05e1 -r ad8535384c34 NEWS --- a/NEWS Fri Dec 03 21:34:54 2010 +0100 +++ b/NEWS Fri Dec 03 22:08:14 2010 +0100 @@ -6,22 +6,15 @@ *** General *** +* Significantly improved Isabelle/Isar implementation manual. + * Source files are always encoded as UTF-8, instead of old-fashioned ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require -the following packages declarations: +the following package declarations: \usepackage[utf8]{inputenc} \usepackage{textcomp} -* 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. - -* Significantly improved Isabelle/Isar implementation manual. - * Explicit treatment of UTF8 sequences as Isabelle symbols, such that a Unicode character is treated as a single symbol, not a sequence of non-ASCII bytes as before. Since Isabelle/ML string literals may @@ -30,6 +23,13 @@ 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. @@ -71,18 +71,18 @@ "no_abbrevs" with inverted meaning. * More systematic naming of some configuration options. - INCOMPATIBILTY. +INCOMPATIBILTY. trace_simp ~> simp_trace debug_simp ~> simp_debug - -*** Pure *** - * Support for real valued configuration options, using simplistic floating-point notation that coincides with the inner syntax for float_token. + +*** Pure *** + * Support for real valued preferences (with approximative PGIP type). * Interpretation command 'interpret' accepts a list of equations like @@ -96,7 +96,7 @@ Sign.root_path and Sign.local_path may be applied directly where this feature is still required for historical reasons. -* Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use +* Discontinued obsolete 'constdefs' command. INCOMPATIBILITY, use 'definition' instead. * Document antiquotations @{class} and @{type} print classes and type @@ -135,31 +135,35 @@ declare [[coercion_enabled]] -* Abandoned locales equiv, congruent and congruent2 for equivalence relations. -INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)). - -* Code generator: globbing constant expressions "*" and "Theory.*" have been -replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY. - -* Theory Enum (for explicit enumerations of finite types) 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. - constants - enum -> Enum.enum - nlists -> Enum.nlists - product -> Enum.product +* Abandoned locales equiv, congruent and congruent2 for equivalence +relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same +for congruent(2)). + +* Code generator: globbing constant expressions "*" and "Theory.*" +have been replaced by the more idiomatic "_" and "Theory._". +INCOMPATIBILITY. + +* Theory Enum (for explicit enumerations of finite types) 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 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to avoid confusion with finite sets. INCOMPATIBILITY. -* Quickcheck's generator for random generation is renamed from "code" to -"random". INCOMPATIBILITY. - -* Theory Multiset provides stable quicksort implementation of sort_key. - -* Quickcheck now has a configurable time limit which is set to 30 seconds -by default. This can be changed by adding [timeout = n] to the quickcheck -command. The time limit for Auto Quickcheck is still set independently. +* Quickcheck's generator for random generation is renamed from "code" +to "random". INCOMPATIBILITY. + +* Quickcheck now has a configurable time limit which is set to 30 +seconds by default. This can be changed by adding [timeout = n] to the +quickcheck command. The time limit for Auto Quickcheck is still set +independently. + +* Theory Multiset provides stable quicksort implementation of +sort_key. * New command 'partial_function' provides basic support for recursive function definitions over complete partial orders. Concrete instances @@ -168,11 +172,11 @@ HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for examples. -* Predicates `distinct` and `sorted` now defined inductively, with nice -induction rules. INCOMPATIBILITY: former distinct.simps and sorted.simps -now named distinct_simps and sorted_simps. - -* Constant `contents` renamed to `the_elem`, to free the generic name +* Predicates "distinct" and "sorted" now defined inductively, with +nice induction rules. INCOMPATIBILITY: former distinct.simps and +sorted.simps now named distinct_simps and sorted_simps. + +* Constant "contents" renamed to "the_elem", to free the generic name contents for other uses. INCOMPATIBILITY. * Dropped syntax for old primrec package. INCOMPATIBILITY. @@ -182,36 +186,34 @@ * String.literal is a type, but not a datatype. INCOMPATIBILITY. -* Renamed lemmas: - expand_fun_eq -> fun_eq_iff - expand_set_eq -> set_eq_iff - set_ext -> set_eqI - INCOMPATIBILITY. - -* Renamed lemma list: nat_number -> eval_nat_numeral - -* Renamed class eq and constant eq (for code generation) to class equal -and constant equal, plus renaming of related facts and various tuning. -INCOMPATIBILITY. - -* Scala (2.8 or higher) has been added to the target languages of -the code generator. +* Renamed facts: + expand_fun_eq ~> fun_eq_iff + expand_set_eq ~> set_eq_iff + set_ext ~> set_eqI + nat_number ~> eval_nat_numeral + +* Renamed class eq and constant eq (for code generation) to class +equal and constant equal, plus renaming of related facts and various +tuning. INCOMPATIBILITY. + +* Scala (2.8 or higher) has been added to the target languages of the +code generator. * Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY. -* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY. - -* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras; -canonical names for instance definitions for functions; various improvements. -INCOMPATIBILITY. - -* Records: logical foundation type for records do not carry a '_type' suffix -any longer. INCOMPATIBILITY. - -* Code generation 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: +* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY. + +* Theory SetsAndFunctions has been split into Function_Algebras and +Set_Algebras; canonical names for instance definitions for functions; +various improvements. INCOMPATIBILITY. + +* Records: logical foundation type for records do not carry a '_type' +suffix any longer. INCOMPATIBILITY. + +* Code generation 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: record 'a foo = ... ... @@ -223,24 +225,24 @@ * Quickcheck in locales considers interpretations of that locale for counter example search. -* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax -in Library/State_Monad has been changed to avoid ambiguities. +* Theory Library/Monad_Syntax provides do-syntax for monad types. +Syntax in Library/State_Monad has been changed to avoid ambiguities. INCOMPATIBILITY. * Code generator: export_code without explicit file declaration prints to standard output. INCOMPATIBILITY. -* Abolished symbol type names: "prod" and "sum" replace "*" and "+" -respectively. INCOMPATIBILITY. - -* Name "Plus" of disjoint sum operator "<+>" is now hidden. - Write Sum_Type.Plus. - -* Constant "split" has been merged with constant "prod_case"; names -of ML functions, facts etc. involving split have been retained so far, +* Abolished some non-alphabetic type names: "prod" and "sum" replace +"*" and "+" respectively. INCOMPATIBILITY. + +* Name "Plus" of disjoint sum operator "<+>" is now hidden. Write +Sum_Type.Plus. + +* Constant "split" has been merged with constant "prod_case"; names of +ML functions, facts etc. involving split have been retained so far, though. INCOMPATIBILITY. -* Dropped old infix syntax "mem" for List.member; use "in set" +* Dropped old infix syntax "mem" for List.member; use "in set" instead. INCOMPATIBILITY. * Refactoring of code-generation specific operations in List.thy @@ -253,7 +255,7 @@ null_empty ~> null_def INCOMPATIBILITY. Note that these were not suppossed to be used -regularly unless for striking reasons; their main purpose was code +regularly unless for striking reasons; their main purpose was code generation. * Some previously unqualified names have been qualified: @@ -292,9 +294,8 @@ * Removed simplifier congruence rule of "prod_case", as has for long been the case with "split". INCOMPATIBILITY. -* Datatype package: theorems generated for executable equality -(class eq) carry proper names and are treated as default code -equations. +* Datatype package: theorems generated for executable equality (class +eq) carry proper names and are treated as default code equations. * Removed lemma Option.is_none_none (Duplicate of is_none_def). INCOMPATIBILITY. @@ -304,15 +305,15 @@ * Multiset.thy: renamed empty_idemp -> empty_neutral -* code_simp.ML and method code_simp: simplification with rules determined -by code generator. +* code_simp.ML and method code_simp: simplification with rules +determined by code generator. * code generator: do not print function definitions for case combinators any longer. -* Multivariate Analysis: Introduced a type class for euclidean space. Most -theorems are now stated in terms of euclidean spaces instead of finite -cartesian products. +* 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 @@ -325,31 +326,32 @@ \ 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. - -* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal -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. - -* Inductive package: offers new command "inductive_simps" to automatically -derive instantiated and simplified equations for inductive predicates, -similar to inductive_cases. +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. + +* Probability: Introduced pinfreal as real numbers with infinity. Use +pinfreal 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. + +* Inductive package: offers new command 'inductive_simps' to +automatically derive instantiated and simplified equations for +inductive predicates, similar to 'inductive_cases'. * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an abbreviation of "range f = UNIV". The theorems bij_def and surj_def are unchanged. INCOMPATIBILITY. -* Function package: .psimps rules are no longer implicitly declared [simp]. -INCOMPATIBILITY. - -* Weaker versions of the "meson" and "metis" proof methods are now available in - "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become - more powerful after "Hilbert_Choice" is loaded in "HOL-Main". +* Function package: .psimps rules are no longer implicitly declared +[simp]. INCOMPATIBILITY. + +* Weaker versions of the "meson" and "metis" proof methods are now +available in "HOL-Plain", without dependency on "Hilbert_Choice". The +proof methods become more powerful after "Hilbert_Choice" is loaded in +"HOL-Main". * MESON: Renamed lemmas: meson_not_conjD ~> Meson.not_conjD @@ -373,8 +375,8 @@ meson_disj_FalseD2 ~> Meson.disj_FalseD2 INCOMPATIBILITY. -* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as - "solve_direct". +* Auto Solve: Renamed "Auto Solve Direct". The tool is now available +manually as command 'solve_direct'. * Sledgehammer: - Added "smt" and "remote_smt" provers based on the "smt" proof method. See @@ -403,8 +405,9 @@ (and "ms" and "min" are no longer supported) INCOMPATIBILITY. -* Metis and Meson now have configuration options "meson_trace", "metis_trace", - and "metis_verbose" that can be enabled to diagnose these tools. E.g. +* Metis and Meson now have configuration options "meson_trace", +"metis_trace", and "metis_verbose" that can be enabled to diagnose +these tools. E.g. using [[metis_trace = true]] @@ -435,8 +438,8 @@ cvc3_options yices_options -* Boogie output files (.b2i files) need to be declared in the -theory header. +* Boogie output files (.b2i files) need to be declared in the theory +header. * Removed [split_format ... and ... and ...] version of [split_format]. Potential INCOMPATIBILITY. @@ -487,7 +490,7 @@ cont2cont_Rep_CFun ~> cont2cont_APP * The Abs and Rep functions for various types have changed names. -Related theorem names have also changed to match. INCOMPATIBILITY. +Related theorem names have also changed to match. INCOMPATIBILITY. Rep_CFun ~> Rep_cfun Abs_CFun ~> Abs_cfun Rep_Sprod ~> Rep_sprod @@ -505,8 +508,8 @@ - Variable names in bisim_def and coinduct rules have changed. INCOMPATIBILITY. -* Case combinators generated by the domain package for type 'foo' -are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY. +* Case combinators generated by the domain package for type 'foo' are +now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY. * Several theorems have been renamed to more accurately reflect the names of constants and types involved. INCOMPATIBILITY. @@ -572,12 +575,7 @@ less_sinrD ~> below_sinrD -*** FOL *** - -* All constant names are now qualified. INCOMPATIBILITY. - - -*** ZF *** +*** FOL and ZF *** * All constant names are now qualified. INCOMPATIBILITY.