1.1 --- a/NEWS Sun Jan 16 19:45:42 2011 +0100
1.2 +++ b/NEWS Sun Jan 16 20:54:30 2011 +0100
1.3 @@ -12,6 +12,13 @@
1.4
1.5 * Significantly improved Isabelle/Isar implementation manual.
1.6
1.7 +* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
1.8 +(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
1.9 +while the default heap location within that directory lacks that extra
1.10 +suffix. This isolates multiple Isabelle installations from each
1.11 +other, avoiding problems with old settings in new versions.
1.12 +INCOMPATIBILITY, need to copy/upgrade old user settings manually.
1.13 +
1.14 * Source files are always encoded as UTF-8, instead of old-fashioned
1.15 ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require
1.16 the following package declarations:
1.17 @@ -27,16 +34,11 @@
1.18 consistent view on symbols, while raw explode (or String.explode)
1.19 merely give a byte-oriented representation.
1.20
1.21 -* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
1.22 -(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
1.23 -while the default heap location within that directory lacks that extra
1.24 -suffix. This isolates multiple Isabelle installations from each
1.25 -other, avoiding problems with old settings in new versions.
1.26 -INCOMPATIBILITY, need to copy/upgrade old user settings manually.
1.27 -
1.28 -* Theory loading: only the master source file is looked-up in the
1.29 -implicit load path, all other files are addressed relatively to its
1.30 -directory. Minor INCOMPATIBILITY, subtle change in semantics.
1.31 +* Theory loader: source files are primarily located via the master
1.32 +directory of each theory node (where the .thy file itself resides).
1.33 +The global load path is still partially available as legacy feature.
1.34 +Minor INCOMPATIBILITY due to subtle change in file lookup: use
1.35 +explicit paths, relatively to the theory.
1.36
1.37 * Special treatment of ML file names has been discontinued.
1.38 Historically, optional extensions .ML or .sml were added on demand --
1.39 @@ -88,15 +90,15 @@
1.40 floating-point notation that coincides with the inner syntax for
1.41 float_token.
1.42
1.43 -* Theory loader: implicit load path is considered legacy. Use
1.44 -explicit file specifications instead, relatively to the directory of
1.45 -the enclosing theory file.
1.46 -
1.47 -* Discontinued support for Poly/ML 5.0 and 5.1 versions.
1.48 +* Support for real valued preferences (with approximative PGIP type):
1.49 +front-ends need to accept "pgint" values in float notation.
1.50 +INCOMPATIBILITY.
1.51
1.52 * The IsabelleText font now includes Cyrillic, Hebrew, Arabic from
1.53 DejaVu Sans.
1.54
1.55 +* Discontinued support for Poly/ML 5.0 and 5.1 versions.
1.56 +
1.57
1.58 *** Pure ***
1.59
1.60 @@ -110,17 +112,15 @@
1.61 * Command 'notepad' replaces former 'example_proof' for
1.62 experimentation in Isar without any result. INCOMPATIBILITY.
1.63
1.64 -* Support for real valued preferences (with approximative PGIP type).
1.65 -
1.66 * Locale interpretation commands 'interpret' and 'sublocale' accept
1.67 lists of equations to map definitions in a locale to appropriate
1.68 entities in the context of the interpretation. The 'interpretation'
1.69 command already provided this functionality.
1.70
1.71 -* New diagnostic command 'print_dependencies' prints the locale
1.72 -instances that would be activated if the specified expression was
1.73 -interpreted in the current context. Variant 'print_dependencies!'
1.74 -assumes a context without interpretations.
1.75 +* Diagnostic command 'print_dependencies' prints the locale instances
1.76 +that would be activated if the specified expression was interpreted in
1.77 +the current context. Variant "print_dependencies!" assumes a context
1.78 +without interpretations.
1.79
1.80 * Diagnostic command 'print_interps' prints interpretations in proofs
1.81 in addition to interpretations in theories.
1.82 @@ -135,8 +135,8 @@
1.83
1.84 * The "prems" fact, which refers to the accidental collection of
1.85 foundational premises in the context, is now explicitly marked as
1.86 -legacy feature and will be discontinued eventually. Consider using
1.87 -"assms" of the head statement or reference facts by explicit names.
1.88 +legacy feature and will be discontinued soon. Consider using "assms"
1.89 +of the head statement or reference facts by explicit names.
1.90
1.91 * Document antiquotations @{class} and @{type} print classes and type
1.92 constructors.
1.93 @@ -147,16 +147,10 @@
1.94
1.95 *** HOL ***
1.96
1.97 -* Simproc "list_to_set_comprehension" rewrites list comprehensions
1.98 -applied to List.set to set comprehensions. Occasional
1.99 -INCOMPATIBILITY, may be deactivated like this:
1.100 -
1.101 - declare [[simproc del: list_to_set_comprehension]]
1.102 -
1.103 -* Functions can be declared as coercions and type inference will add
1.104 -them as necessary upon input of a term. Theory Complex_Main declares
1.105 -real :: nat => real and real :: int => real as coercions. A coercion
1.106 -function f is declared like this:
1.107 +* Coercive subtyping: functions can be declared as coercions and type
1.108 +inference will add them as necessary upon input of a term. Theory
1.109 +Complex_Main declares real :: nat => real and real :: int => real as
1.110 +coercions. A coercion function f is declared like this:
1.111
1.112 declare [[coercion f]]
1.113
1.114 @@ -179,25 +173,25 @@
1.115 src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy
1.116 for examples.
1.117
1.118 -* Scala (2.8 or higher) has been added to the target languages of the
1.119 -code generator.
1.120 +* Function package: f.psimps rules are no longer implicitly declared
1.121 +as [simp]. INCOMPATIBILITY.
1.122 +
1.123 +* Datatype package: theorems generated for executable equality (class
1.124 +"eq") carry proper names and are treated as default code equations.
1.125
1.126 * Inductive package: now offers command 'inductive_simps' to
1.127 automatically derive instantiated and simplified equations for
1.128 inductive predicates, similar to 'inductive_cases'.
1.129
1.130 -* Function package: f.psimps rules are no longer implicitly declared
1.131 -as [simp]. INCOMPATIBILITY.
1.132 -
1.133 -* Datatype package: theorems generated for executable equality (class
1.134 -"eq") carry proper names and are treated as default code equations.
1.135 -
1.136 * Command 'enriched_type' allows to register properties of the
1.137 functorial structure of types.
1.138
1.139 * Improved infrastructure for term evaluation using code generator
1.140 techniques, in particular static evaluation conversions.
1.141
1.142 +* Code generator: Scala (2.8 or higher) has been added to the target
1.143 +languages.
1.144 +
1.145 * Code generator: globbing constant expressions "*" and "Theory.*"
1.146 have been replaced by the more idiomatic "_" and "Theory._".
1.147 INCOMPATIBILITY.
1.148 @@ -208,22 +202,22 @@
1.149 * Code generator: do not print function definitions for case
1.150 combinators any longer.
1.151
1.152 -* Simplification with rules determined by code generator with
1.153 +* Code generator: simplification with rules determined with
1.154 src/Tools/Code/code_simp.ML and method "code_simp".
1.155
1.156 +* Code generator for records: more idiomatic representation of record
1.157 +types. Warning: records are not covered by ancient SML code
1.158 +generation any longer. INCOMPATIBILITY. In cases of need, a suitable
1.159 +rep_datatype declaration helps to succeed then:
1.160 +
1.161 + record 'a foo = ...
1.162 + ...
1.163 + rep_datatype foo_ext ...
1.164 +
1.165 * Records: logical foundation type for records does not carry a
1.166 '_type' suffix any longer (obsolete due to authentic syntax).
1.167 INCOMPATIBILITY.
1.168
1.169 -* Code generation for records: more idiomatic representation of record
1.170 -types. Warning: records are not covered by ancient SML code
1.171 -generation any longer. INCOMPATIBILITY. In cases of need, a suitable
1.172 -rep_datatype declaration helps to succeed then:
1.173 -
1.174 - record 'a foo = ...
1.175 - ...
1.176 - rep_datatype foo_ext ...
1.177 -
1.178 * Quickcheck now by default uses exhaustive testing instead of random
1.179 testing. Random testing can be invoked by "quickcheck [random]",
1.180 exhaustive testing by "quickcheck [exhaustive]".
1.181 @@ -314,56 +308,14 @@
1.182 * Boogie output files (.b2i files) need to be declared in the theory
1.183 header.
1.184
1.185 +* Simplification procedure "list_to_set_comprehension" rewrites list
1.186 +comprehensions applied to List.set to set comprehensions. Occasional
1.187 +INCOMPATIBILITY, may be deactivated like this:
1.188 +
1.189 + declare [[simproc del: list_to_set_comprehension]]
1.190 +
1.191 * Removed old version of primrec package. INCOMPATIBILITY.
1.192
1.193 -* Multivariate Analysis: Introduced a type class for euclidean
1.194 -space. Most theorems are now stated in terms of euclidean spaces
1.195 -instead of finite cartesian products.
1.196 -
1.197 - types
1.198 - real ^ 'n ~> 'a::real_vector
1.199 - ~> 'a::euclidean_space
1.200 - ~> 'a::ordered_euclidean_space
1.201 - (depends on your needs)
1.202 -
1.203 - constants
1.204 - _ $ _ ~> _ $$ _
1.205 - \<chi> x. _ ~> \<chi>\<chi> x. _
1.206 - CARD('n) ~> DIM('a)
1.207 -
1.208 -Also note that the indices are now natural numbers and not from some
1.209 -finite type. Finite cartesian products of euclidean spaces, products
1.210 -of euclidean spaces the real and complex numbers are instantiated to
1.211 -be euclidean_spaces. INCOMPATIBILITY.
1.212 -
1.213 -* Session Probability: Introduced pextreal as positive extended real
1.214 -numbers. Use pextreal as value for measures. Introduce the
1.215 -Radon-Nikodym derivative, product spaces and Fubini's theorem for
1.216 -arbitrary sigma finite measures. Introduces Lebesgue measure based on
1.217 -the integral in Multivariate Analysis. INCOMPATIBILITY.
1.218 -
1.219 -* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
1.220 -INCOMPATIBILITY.
1.221 -
1.222 -* Theory Library/Monad_Syntax provides do-syntax for monad types.
1.223 -Syntax in Library/State_Monad has been changed to avoid ambiguities.
1.224 -INCOMPATIBILITY.
1.225 -
1.226 -* Theory SetsAndFunctions has been split into Function_Algebras and
1.227 -Set_Algebras; canonical names for instance definitions for functions;
1.228 -various improvements. INCOMPATIBILITY.
1.229 -
1.230 -* Theory Library/Multiset provides stable quicksort implementation of
1.231 -sort_key.
1.232 -
1.233 -* Former theory Library/Enum is now part of the HOL-Main image.
1.234 -INCOMPATIBILITY: all constants of the Enum theory now have to be
1.235 -referred to by its qualified name.
1.236 -
1.237 - enum ~> Enum.enum
1.238 - nlists ~> Enum.nlists
1.239 - product ~> Enum.product
1.240 -
1.241 * Removed simplifier congruence rule of "prod_case", as has for long
1.242 been the case with "split". INCOMPATIBILITY.
1.243
1.244 @@ -390,9 +342,6 @@
1.245 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
1.246 avoid confusion with finite sets. INCOMPATIBILITY.
1.247
1.248 -* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
1.249 -INCOMPATIBILITY.
1.250 -
1.251 * Abandoned locales equiv, congruent and congruent2 for equivalence
1.252 relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same
1.253 for congruent(2)).
1.254 @@ -488,8 +437,61 @@
1.255 * Removed lemma "Option.is_none_none" which duplicates "is_none_def".
1.256 INCOMPATIBILITY.
1.257
1.258 -* New commands to load and prove verification conditions generated by
1.259 -the SPARK Ada program verifier. See src/HOL/SPARK.
1.260 +* Former theory Library/Enum is now part of the HOL-Main image.
1.261 +INCOMPATIBILITY: all constants of the Enum theory now have to be
1.262 +referred to by its qualified name.
1.263 +
1.264 + enum ~> Enum.enum
1.265 + nlists ~> Enum.nlists
1.266 + product ~> Enum.product
1.267 +
1.268 +* Theory Library/Monad_Syntax provides do-syntax for monad types.
1.269 +Syntax in Library/State_Monad has been changed to avoid ambiguities.
1.270 +INCOMPATIBILITY.
1.271 +
1.272 +* Theory Library/SetsAndFunctions has been split into
1.273 +Library/Function_Algebras and Library/Set_Algebras; canonical names
1.274 +for instance definitions for functions; various improvements.
1.275 +INCOMPATIBILITY.
1.276 +
1.277 +* Theory Library/Multiset provides stable quicksort implementation of
1.278 +sort_key.
1.279 +
1.280 +* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
1.281 +INCOMPATIBILITY.
1.282 +
1.283 +* Session Multivariate_Analysis: introduced a type class for euclidean
1.284 +space. Most theorems are now stated in terms of euclidean spaces
1.285 +instead of finite cartesian products.
1.286 +
1.287 + types
1.288 + real ^ 'n ~> 'a::real_vector
1.289 + ~> 'a::euclidean_space
1.290 + ~> 'a::ordered_euclidean_space
1.291 + (depends on your needs)
1.292 +
1.293 + constants
1.294 + _ $ _ ~> _ $$ _
1.295 + \<chi> x. _ ~> \<chi>\<chi> x. _
1.296 + CARD('n) ~> DIM('a)
1.297 +
1.298 +Also note that the indices are now natural numbers and not from some
1.299 +finite type. Finite cartesian products of euclidean spaces, products
1.300 +of euclidean spaces the real and complex numbers are instantiated to
1.301 +be euclidean_spaces. INCOMPATIBILITY.
1.302 +
1.303 +* Session Probability: introduced pextreal as positive extended real
1.304 +numbers. Use pextreal as value for measures. Introduce the
1.305 +Radon-Nikodym derivative, product spaces and Fubini's theorem for
1.306 +arbitrary sigma finite measures. Introduces Lebesgue measure based on
1.307 +the integral in Multivariate Analysis. INCOMPATIBILITY.
1.308 +
1.309 +* Session Imperative_HOL: revamped, corrected dozens of inadequacies.
1.310 +INCOMPATIBILITY.
1.311 +
1.312 +* Session SPARK (with image HOL-SPARK) provides commands to load and
1.313 +prove verification conditions generated by the SPARK Ada program
1.314 +verifier. See also src/HOL/SPARK and src/HOL/SPARK/Examples.
1.315
1.316
1.317 *** HOL-Algebra ***
1.318 @@ -688,18 +690,30 @@
1.319
1.320 *** ML ***
1.321
1.322 +* Antiquotation @{assert} inlines a function bool -> unit that raises
1.323 +Fail if the argument is false. Due to inlining the source position of
1.324 +failed assertions is included in the error output.
1.325 +
1.326 +* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
1.327 +text is in practice always evaluated with a stable theory checkpoint.
1.328 +Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
1.329 +
1.330 +* Antiquotation @{theory A} refers to theory A from the ancestry of
1.331 +the current context, not any accidental theory loader state as before.
1.332 +Potential INCOMPATIBILITY, subtle change in semantics.
1.333 +
1.334 +* Syntax.pretty_priority (default 0) configures the required priority
1.335 +of pretty-printed output and thus affects insertion of parentheses.
1.336 +
1.337 +* Syntax.default_root (default "any") configures the inner syntax
1.338 +category (nonterminal symbol) for parsing of terms.
1.339 +
1.340 +* Former exception Library.UnequalLengths now coincides with
1.341 +ListPair.UnequalLengths.
1.342 +
1.343 * Renamed structure MetaSimplifier to Raw_Simplifier. Note that the
1.344 main functionality is provided by structure Simplifier.
1.345
1.346 -* Syntax.pretty_priority (default 0) configures the required priority
1.347 -of pretty-printed output and thus affects insertion of parentheses.
1.348 -
1.349 -* Syntax.default_root (default "any") configures the inner syntax
1.350 -category (nonterminal symbol) for parsing of terms.
1.351 -
1.352 -* Former exception Library.UnequalLengths now coincides with
1.353 -ListPair.UnequalLengths.
1.354 -
1.355 * Renamed raw "explode" function to "raw_explode" to emphasize its
1.356 meaning. Note that internally to Isabelle, Symbol.explode is used in
1.357 almost all situations.
1.358 @@ -708,14 +722,6 @@
1.359 See implementation manual for further details on exceptions in
1.360 Isabelle/ML.
1.361
1.362 -* Antiquotation @{assert} inlines a function bool -> unit that raises
1.363 -Fail if the argument is false. Due to inlining the source position of
1.364 -failed assertions is included in the error output.
1.365 -
1.366 -* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
1.367 -text is in practice always evaluated with a stable theory checkpoint.
1.368 -Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
1.369 -
1.370 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
1.371 meaning.
1.372
1.373 @@ -733,17 +739,12 @@
1.374 INCOMPATIBILITY, superseded by static antiquotations @{thm} and
1.375 @{thms} for most purposes.
1.376
1.377 -* ML structure Unsynchronized never opened, not even in Isar
1.378 +* ML structure Unsynchronized is never opened, not even in Isar
1.379 interaction mode as before. Old Unsynchronized.set etc. have been
1.380 discontinued -- use plain := instead. This should be *rare* anyway,
1.381 since modern tools always work via official context data, notably
1.382 configuration options.
1.383
1.384 -* ML antiquotations @{theory} and @{theory_ref} refer to named
1.385 -theories from the ancestry of the current context, not any accidental
1.386 -theory loader state as before. Potential INCOMPATIBILITY, subtle
1.387 -change in semantics.
1.388 -
1.389 * Parallel and asynchronous execution requires special care concerning
1.390 interrupts. Structure Exn provides some convenience functions that
1.391 avoid working directly with raw Interrupt. User code must not absorb