1.1 --- a/NEWS Fri Dec 03 21:34:54 2010 +0100
1.2 +++ b/NEWS Fri Dec 03 22:08:14 2010 +0100
1.3 @@ -6,22 +6,15 @@
1.4
1.5 *** General ***
1.6
1.7 +* Significantly improved Isabelle/Isar implementation manual.
1.8 +
1.9 * Source files are always encoded as UTF-8, instead of old-fashioned
1.10 ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require
1.11 -the following packages declarations:
1.12 +the following package declarations:
1.13
1.14 \usepackage[utf8]{inputenc}
1.15 \usepackage{textcomp}
1.16
1.17 -* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
1.18 -(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
1.19 -while the default heap location within that directory lacks that extra
1.20 -suffix. This isolates multiple Isabelle installations from each
1.21 -other, avoiding problems with old settings in new versions.
1.22 -INCOMPATIBILITY, need to copy/upgrade old user settings manually.
1.23 -
1.24 -* Significantly improved Isabelle/Isar implementation manual.
1.25 -
1.26 * Explicit treatment of UTF8 sequences as Isabelle symbols, such that
1.27 a Unicode character is treated as a single symbol, not a sequence of
1.28 non-ASCII bytes as before. Since Isabelle/ML string literals may
1.29 @@ -30,6 +23,13 @@
1.30 consistent view on symbols, while raw explode (or String.explode)
1.31 merely give a byte-oriented representation.
1.32
1.33 +* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
1.34 +(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
1.35 +while the default heap location within that directory lacks that extra
1.36 +suffix. This isolates multiple Isabelle installations from each
1.37 +other, avoiding problems with old settings in new versions.
1.38 +INCOMPATIBILITY, need to copy/upgrade old user settings manually.
1.39 +
1.40 * Theory loading: only the master source file is looked-up in the
1.41 implicit load path, all other files are addressed relatively to its
1.42 directory. Minor INCOMPATIBILITY, subtle change in semantics.
1.43 @@ -71,18 +71,18 @@
1.44 "no_abbrevs" with inverted meaning.
1.45
1.46 * More systematic naming of some configuration options.
1.47 - INCOMPATIBILTY.
1.48 +INCOMPATIBILTY.
1.49
1.50 trace_simp ~> simp_trace
1.51 debug_simp ~> simp_debug
1.52
1.53 -
1.54 -*** Pure ***
1.55 -
1.56 * Support for real valued configuration options, using simplistic
1.57 floating-point notation that coincides with the inner syntax for
1.58 float_token.
1.59
1.60 +
1.61 +*** Pure ***
1.62 +
1.63 * Support for real valued preferences (with approximative PGIP type).
1.64
1.65 * Interpretation command 'interpret' accepts a list of equations like
1.66 @@ -96,7 +96,7 @@
1.67 Sign.root_path and Sign.local_path may be applied directly where this
1.68 feature is still required for historical reasons.
1.69
1.70 -* Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use
1.71 +* Discontinued obsolete 'constdefs' command. INCOMPATIBILITY, use
1.72 'definition' instead.
1.73
1.74 * Document antiquotations @{class} and @{type} print classes and type
1.75 @@ -135,31 +135,35 @@
1.76
1.77 declare [[coercion_enabled]]
1.78
1.79 -* Abandoned locales equiv, congruent and congruent2 for equivalence relations.
1.80 -INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).
1.81 -
1.82 -* Code generator: globbing constant expressions "*" and "Theory.*" have been
1.83 -replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.
1.84 -
1.85 -* Theory Enum (for explicit enumerations of finite types) is now part of
1.86 -the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now
1.87 -have to be referred to by its qualified name.
1.88 - constants
1.89 - enum -> Enum.enum
1.90 - nlists -> Enum.nlists
1.91 - product -> Enum.product
1.92 +* Abandoned locales equiv, congruent and congruent2 for equivalence
1.93 +relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same
1.94 +for congruent(2)).
1.95 +
1.96 +* Code generator: globbing constant expressions "*" and "Theory.*"
1.97 +have been replaced by the more idiomatic "_" and "Theory._".
1.98 +INCOMPATIBILITY.
1.99 +
1.100 +* Theory Enum (for explicit enumerations of finite types) is now part
1.101 +of the HOL-Main image. INCOMPATIBILITY: all constants of the Enum
1.102 +theory now have to be referred to by its qualified name.
1.103 +
1.104 + enum ~> Enum.enum
1.105 + nlists ~> Enum.nlists
1.106 + product ~> Enum.product
1.107
1.108 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
1.109 avoid confusion with finite sets. INCOMPATIBILITY.
1.110
1.111 -* Quickcheck's generator for random generation is renamed from "code" to
1.112 -"random". INCOMPATIBILITY.
1.113 -
1.114 -* Theory Multiset provides stable quicksort implementation of sort_key.
1.115 -
1.116 -* Quickcheck now has a configurable time limit which is set to 30 seconds
1.117 -by default. This can be changed by adding [timeout = n] to the quickcheck
1.118 -command. The time limit for Auto Quickcheck is still set independently.
1.119 +* Quickcheck's generator for random generation is renamed from "code"
1.120 +to "random". INCOMPATIBILITY.
1.121 +
1.122 +* Quickcheck now has a configurable time limit which is set to 30
1.123 +seconds by default. This can be changed by adding [timeout = n] to the
1.124 +quickcheck command. The time limit for Auto Quickcheck is still set
1.125 +independently.
1.126 +
1.127 +* Theory Multiset provides stable quicksort implementation of
1.128 +sort_key.
1.129
1.130 * New command 'partial_function' provides basic support for recursive
1.131 function definitions over complete partial orders. Concrete instances
1.132 @@ -168,11 +172,11 @@
1.133 HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
1.134 examples.
1.135
1.136 -* Predicates `distinct` and `sorted` now defined inductively, with nice
1.137 -induction rules. INCOMPATIBILITY: former distinct.simps and sorted.simps
1.138 -now named distinct_simps and sorted_simps.
1.139 -
1.140 -* Constant `contents` renamed to `the_elem`, to free the generic name
1.141 +* Predicates "distinct" and "sorted" now defined inductively, with
1.142 +nice induction rules. INCOMPATIBILITY: former distinct.simps and
1.143 +sorted.simps now named distinct_simps and sorted_simps.
1.144 +
1.145 +* Constant "contents" renamed to "the_elem", to free the generic name
1.146 contents for other uses. INCOMPATIBILITY.
1.147
1.148 * Dropped syntax for old primrec package. INCOMPATIBILITY.
1.149 @@ -182,36 +186,34 @@
1.150
1.151 * String.literal is a type, but not a datatype. INCOMPATIBILITY.
1.152
1.153 -* Renamed lemmas:
1.154 - expand_fun_eq -> fun_eq_iff
1.155 - expand_set_eq -> set_eq_iff
1.156 - set_ext -> set_eqI
1.157 - INCOMPATIBILITY.
1.158 -
1.159 -* Renamed lemma list: nat_number -> eval_nat_numeral
1.160 -
1.161 -* Renamed class eq and constant eq (for code generation) to class equal
1.162 -and constant equal, plus renaming of related facts and various tuning.
1.163 -INCOMPATIBILITY.
1.164 -
1.165 -* Scala (2.8 or higher) has been added to the target languages of
1.166 -the code generator.
1.167 +* Renamed facts:
1.168 + expand_fun_eq ~> fun_eq_iff
1.169 + expand_set_eq ~> set_eq_iff
1.170 + set_ext ~> set_eqI
1.171 + nat_number ~> eval_nat_numeral
1.172 +
1.173 +* Renamed class eq and constant eq (for code generation) to class
1.174 +equal and constant equal, plus renaming of related facts and various
1.175 +tuning. INCOMPATIBILITY.
1.176 +
1.177 +* Scala (2.8 or higher) has been added to the target languages of the
1.178 +code generator.
1.179
1.180 * Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
1.181
1.182 -* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
1.183 -
1.184 -* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
1.185 -canonical names for instance definitions for functions; various improvements.
1.186 -INCOMPATIBILITY.
1.187 -
1.188 -* Records: logical foundation type for records do not carry a '_type' suffix
1.189 -any longer. INCOMPATIBILITY.
1.190 -
1.191 -* Code generation for records: more idiomatic representation of record types.
1.192 -Warning: records are not covered by ancient SML code generation any longer.
1.193 -INCOMPATIBILITY. In cases of need, a suitable rep_datatype declaration
1.194 -helps to succeed then:
1.195 +* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
1.196 +
1.197 +* Theory SetsAndFunctions has been split into Function_Algebras and
1.198 +Set_Algebras; canonical names for instance definitions for functions;
1.199 +various improvements. INCOMPATIBILITY.
1.200 +
1.201 +* Records: logical foundation type for records do not carry a '_type'
1.202 +suffix any longer. INCOMPATIBILITY.
1.203 +
1.204 +* Code generation for records: more idiomatic representation of record
1.205 +types. Warning: records are not covered by ancient SML code
1.206 +generation any longer. INCOMPATIBILITY. In cases of need, a suitable
1.207 +rep_datatype declaration helps to succeed then:
1.208
1.209 record 'a foo = ...
1.210 ...
1.211 @@ -223,24 +225,24 @@
1.212 * Quickcheck in locales considers interpretations of that locale for
1.213 counter example search.
1.214
1.215 -* Theory Library/Monad_Syntax provides do-syntax for monad types. Syntax
1.216 -in Library/State_Monad has been changed to avoid ambiguities.
1.217 +* Theory Library/Monad_Syntax provides do-syntax for monad types.
1.218 +Syntax in Library/State_Monad has been changed to avoid ambiguities.
1.219 INCOMPATIBILITY.
1.220
1.221 * Code generator: export_code without explicit file declaration prints
1.222 to standard output. INCOMPATIBILITY.
1.223
1.224 -* Abolished symbol type names: "prod" and "sum" replace "*" and "+"
1.225 -respectively. INCOMPATIBILITY.
1.226 -
1.227 -* Name "Plus" of disjoint sum operator "<+>" is now hidden.
1.228 - Write Sum_Type.Plus.
1.229 -
1.230 -* Constant "split" has been merged with constant "prod_case"; names
1.231 -of ML functions, facts etc. involving split have been retained so far,
1.232 +* Abolished some non-alphabetic type names: "prod" and "sum" replace
1.233 +"*" and "+" respectively. INCOMPATIBILITY.
1.234 +
1.235 +* Name "Plus" of disjoint sum operator "<+>" is now hidden. Write
1.236 +Sum_Type.Plus.
1.237 +
1.238 +* Constant "split" has been merged with constant "prod_case"; names of
1.239 +ML functions, facts etc. involving split have been retained so far,
1.240 though. INCOMPATIBILITY.
1.241
1.242 -* Dropped old infix syntax "mem" for List.member; use "in set"
1.243 +* Dropped old infix syntax "mem" for List.member; use "in set"
1.244 instead. INCOMPATIBILITY.
1.245
1.246 * Refactoring of code-generation specific operations in List.thy
1.247 @@ -253,7 +255,7 @@
1.248 null_empty ~> null_def
1.249
1.250 INCOMPATIBILITY. Note that these were not suppossed to be used
1.251 -regularly unless for striking reasons; their main purpose was code
1.252 +regularly unless for striking reasons; their main purpose was code
1.253 generation.
1.254
1.255 * Some previously unqualified names have been qualified:
1.256 @@ -292,9 +294,8 @@
1.257 * Removed simplifier congruence rule of "prod_case", as has for long
1.258 been the case with "split". INCOMPATIBILITY.
1.259
1.260 -* Datatype package: theorems generated for executable equality
1.261 -(class eq) carry proper names and are treated as default code
1.262 -equations.
1.263 +* Datatype package: theorems generated for executable equality (class
1.264 +eq) carry proper names and are treated as default code equations.
1.265
1.266 * Removed lemma Option.is_none_none (Duplicate of is_none_def).
1.267 INCOMPATIBILITY.
1.268 @@ -304,15 +305,15 @@
1.269
1.270 * Multiset.thy: renamed empty_idemp -> empty_neutral
1.271
1.272 -* code_simp.ML and method code_simp: simplification with rules determined
1.273 -by code generator.
1.274 +* code_simp.ML and method code_simp: simplification with rules
1.275 +determined by code generator.
1.276
1.277 * code generator: do not print function definitions for case
1.278 combinators any longer.
1.279
1.280 -* Multivariate Analysis: Introduced a type class for euclidean space. Most
1.281 -theorems are now stated in terms of euclidean spaces instead of finite
1.282 -cartesian products.
1.283 +* 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 @@ -325,31 +326,32 @@
1.290 \<chi> x. _ ~> \<chi>\<chi> x. _
1.291 CARD('n) ~> DIM('a)
1.292
1.293 -Also note that the indices are now natural numbers and not from some finite
1.294 -type. Finite cartesian products of euclidean spaces, products of euclidean
1.295 -spaces the real and complex numbers are instantiated to be euclidean_spaces.
1.296 -INCOMPATIBILITY.
1.297 -
1.298 -* Probability: Introduced pinfreal as real numbers with infinity. Use pinfreal
1.299 -as value for measures. Introduce the Radon-Nikodym derivative, product spaces
1.300 -and Fubini's theorem for arbitrary sigma finite measures. Introduces Lebesgue
1.301 -measure based on the integral in Multivariate Analysis.
1.302 -INCOMPATIBILITY.
1.303 -
1.304 -* Inductive package: offers new command "inductive_simps" to automatically
1.305 -derive instantiated and simplified equations for inductive predicates,
1.306 -similar to inductive_cases.
1.307 +Also note that the indices are now natural numbers and not from some
1.308 +finite type. Finite cartesian products of euclidean spaces, products
1.309 +of euclidean spaces the real and complex numbers are instantiated to
1.310 +be euclidean_spaces. INCOMPATIBILITY.
1.311 +
1.312 +* Probability: Introduced pinfreal as real numbers with infinity. Use
1.313 +pinfreal as value for measures. Introduce the Radon-Nikodym
1.314 +derivative, product spaces and Fubini's theorem for arbitrary sigma
1.315 +finite measures. Introduces Lebesgue measure based on the integral in
1.316 +Multivariate Analysis. INCOMPATIBILITY.
1.317 +
1.318 +* Inductive package: offers new command 'inductive_simps' to
1.319 +automatically derive instantiated and simplified equations for
1.320 +inductive predicates, similar to 'inductive_cases'.
1.321
1.322 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f"
1.323 is now an abbreviation of "range f = UNIV". The theorems bij_def and
1.324 surj_def are unchanged. INCOMPATIBILITY.
1.325
1.326 -* Function package: .psimps rules are no longer implicitly declared [simp].
1.327 -INCOMPATIBILITY.
1.328 -
1.329 -* Weaker versions of the "meson" and "metis" proof methods are now available in
1.330 - "HOL-Plain", without dependency on "Hilbert_Choice". The proof methods become
1.331 - more powerful after "Hilbert_Choice" is loaded in "HOL-Main".
1.332 +* Function package: .psimps rules are no longer implicitly declared
1.333 +[simp]. INCOMPATIBILITY.
1.334 +
1.335 +* Weaker versions of the "meson" and "metis" proof methods are now
1.336 +available in "HOL-Plain", without dependency on "Hilbert_Choice". The
1.337 +proof methods become more powerful after "Hilbert_Choice" is loaded in
1.338 +"HOL-Main".
1.339
1.340 * MESON: Renamed lemmas:
1.341 meson_not_conjD ~> Meson.not_conjD
1.342 @@ -373,8 +375,8 @@
1.343 meson_disj_FalseD2 ~> Meson.disj_FalseD2
1.344 INCOMPATIBILITY.
1.345
1.346 -* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as
1.347 - "solve_direct".
1.348 +* Auto Solve: Renamed "Auto Solve Direct". The tool is now available
1.349 +manually as command 'solve_direct'.
1.350
1.351 * Sledgehammer:
1.352 - Added "smt" and "remote_smt" provers based on the "smt" proof method. See
1.353 @@ -403,8 +405,9 @@
1.354 (and "ms" and "min" are no longer supported)
1.355 INCOMPATIBILITY.
1.356
1.357 -* Metis and Meson now have configuration options "meson_trace", "metis_trace",
1.358 - and "metis_verbose" that can be enabled to diagnose these tools. E.g.
1.359 +* Metis and Meson now have configuration options "meson_trace",
1.360 +"metis_trace", and "metis_verbose" that can be enabled to diagnose
1.361 +these tools. E.g.
1.362
1.363 using [[metis_trace = true]]
1.364
1.365 @@ -435,8 +438,8 @@
1.366 cvc3_options
1.367 yices_options
1.368
1.369 -* Boogie output files (.b2i files) need to be declared in the
1.370 -theory header.
1.371 +* Boogie output files (.b2i files) need to be declared in the theory
1.372 +header.
1.373
1.374 * Removed [split_format ... and ... and ...] version of
1.375 [split_format]. Potential INCOMPATIBILITY.
1.376 @@ -487,7 +490,7 @@
1.377 cont2cont_Rep_CFun ~> cont2cont_APP
1.378
1.379 * The Abs and Rep functions for various types have changed names.
1.380 -Related theorem names have also changed to match. INCOMPATIBILITY.
1.381 +Related theorem names have also changed to match. INCOMPATIBILITY.
1.382 Rep_CFun ~> Rep_cfun
1.383 Abs_CFun ~> Abs_cfun
1.384 Rep_Sprod ~> Rep_sprod
1.385 @@ -505,8 +508,8 @@
1.386 - Variable names in bisim_def and coinduct rules have changed.
1.387 INCOMPATIBILITY.
1.388
1.389 -* Case combinators generated by the domain package for type 'foo'
1.390 -are now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
1.391 +* Case combinators generated by the domain package for type 'foo' are
1.392 +now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
1.393
1.394 * Several theorems have been renamed to more accurately reflect the
1.395 names of constants and types involved. INCOMPATIBILITY.
1.396 @@ -572,12 +575,7 @@
1.397 less_sinrD ~> below_sinrD
1.398
1.399
1.400 -*** FOL ***
1.401 -
1.402 -* All constant names are now qualified. INCOMPATIBILITY.
1.403 -
1.404 -
1.405 -*** ZF ***
1.406 +*** FOL and ZF ***
1.407
1.408 * All constant names are now qualified. INCOMPATIBILITY.
1.409