1.1 --- a/NEWS Sat Jan 15 12:55:19 2011 +0100
1.2 +++ b/NEWS Sat Jan 15 13:34:10 2011 +0100
1.3 @@ -133,20 +133,20 @@
1.4
1.5 *** HOL ***
1.6
1.7 -* New simproc that rewrites list comprehensions applied to List.set
1.8 -to set comprehensions.
1.9 -To deactivate the simproc for historic proof scripts, use:
1.10 -
1.11 - [[simproc del: list_to_set_comprehension]]
1.12 +* Simproc "list_to_set_comprehension" rewrites list comprehensions
1.13 +applied to List.set to set comprehensions. Occasional
1.14 +INCOMPATIBILITY, may be deactivated like this:
1.15 +
1.16 + declare [[simproc del: list_to_set_comprehension]]
1.17
1.18 * Functions can be declared as coercions and type inference will add
1.19 -them as necessary upon input of a term. In theory Complex_Main,
1.20 -real :: nat => real and real :: int => real are declared as
1.21 -coercions. A new coercion function f is declared like this:
1.22 +them as necessary upon input of a term. Theory Complex_Main declares
1.23 +real :: nat => real and real :: int => real as coercions. A coercion
1.24 +function f is declared like this:
1.25
1.26 declare [[coercion f]]
1.27
1.28 -To lift coercions through type constructors (eg from nat => real to
1.29 +To lift coercions through type constructors (e.g. from nat => real to
1.30 nat list => real list), map functions can be declared, e.g.
1.31
1.32 declare [[coercion_map map]]
1.33 @@ -158,33 +158,28 @@
1.34
1.35 declare [[coercion_enabled]]
1.36
1.37 -* New command 'partial_function' provides basic support for recursive
1.38 -function definitions over complete partial orders. Concrete instances
1.39 +* Command 'partial_function' provides basic support for recursive
1.40 +function definitions over complete partial orders. Concrete instances
1.41 are provided for i) the option type, ii) tail recursion on arbitrary
1.42 -types, and iii) the heap monad of Imperative_HOL. See
1.43 -HOL/ex/Fundefs.thy and HOL/Imperative_HOL/ex/Linked_Lists.thy for
1.44 -examples.
1.45 +types, and iii) the heap monad of Imperative_HOL. See
1.46 +src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy
1.47 +for examples.
1.48
1.49 * Scala (2.8 or higher) has been added to the target languages of the
1.50 code generator.
1.51
1.52 -* Inductive package: offers new command 'inductive_simps' to
1.53 +* Inductive package: now offers command 'inductive_simps' to
1.54 automatically derive instantiated and simplified equations for
1.55 inductive predicates, similar to 'inductive_cases'.
1.56
1.57 -* Function package: .psimps rules are no longer implicitly declared
1.58 -[simp]. INCOMPATIBILITY.
1.59 +* Function package: f.psimps rules are no longer implicitly declared
1.60 +as [simp]. INCOMPATIBILITY.
1.61
1.62 * Datatype package: theorems generated for executable equality (class
1.63 -eq) carry proper names and are treated as default code equations.
1.64 -
1.65 -* New command 'enriched_type' allows to register properties of
1.66 -the functorial structure of types.
1.67 -
1.68 -* Weaker versions of the "meson" and "metis" proof methods are now
1.69 -available in "HOL-Plain", without dependency on "Hilbert_Choice". The
1.70 -proof methods become more powerful after "Hilbert_Choice" is loaded in
1.71 -"HOL-Main".
1.72 +"eq") carry proper names and are treated as default code equations.
1.73 +
1.74 +* Command 'enriched_type' allows to register properties of the
1.75 +functorial structure of types.
1.76
1.77 * Improved infrastructure for term evaluation using code generator
1.78 techniques, in particular static evaluation conversions.
1.79 @@ -199,11 +194,12 @@
1.80 * Code generator: do not print function definitions for case
1.81 combinators any longer.
1.82
1.83 -* Simplification with rules determined by code generator
1.84 -with code_simp.ML and method code_simp.
1.85 -
1.86 -* Records: logical foundation type for records does not carry a '_type'
1.87 -suffix any longer. INCOMPATIBILITY.
1.88 +* Simplification with rules determined by code generator with
1.89 +src/Tools/Code/code_simp.ML and method "code_simp".
1.90 +
1.91 +* Records: logical foundation type for records does not carry a
1.92 +'_type' suffix any longer (obsolete due to authentic syntax).
1.93 +INCOMPATIBILITY.
1.94
1.95 * Code generation for records: more idiomatic representation of record
1.96 types. Warning: records are not covered by ancient SML code
1.97 @@ -215,15 +211,15 @@
1.98 rep_datatype foo_ext ...
1.99
1.100 * Quickcheck now by default uses exhaustive testing instead of random
1.101 -testing. Random testing can be invoked by quickcheck[random],
1.102 -exhaustive testing by quickcheck[exhaustive].
1.103 +testing. Random testing can be invoked by "quickcheck [random]",
1.104 +exhaustive testing by "quickcheck [exhaustive]".
1.105
1.106 * Quickcheck instantiates polymorphic types with small finite
1.107 datatypes by default. This enables a simple execution mechanism to
1.108 handle quantifiers and function equality over the finite datatypes.
1.109
1.110 -* Quickcheck's generator for random generation is renamed from "code"
1.111 -to "random". INCOMPATIBILITY.
1.112 +* Quickcheck random generator has been renamed from "code" to
1.113 +"random". INCOMPATIBILITY.
1.114
1.115 * Quickcheck now has a configurable time limit which is set to 30
1.116 seconds by default. This can be changed by adding [timeout = n] to the
1.117 @@ -234,20 +230,9 @@
1.118 counter example search.
1.119
1.120 * Sledgehammer:
1.121 - - Added "smt" and "remote_smt" provers based on the "smt" proof method. See
1.122 - the Sledgehammer manual for details ("isabelle doc sledgehammer").
1.123 - - Renamed lemmas:
1.124 - COMBI_def ~> Meson.COMBI_def
1.125 - COMBK_def ~> Meson.COMBK_def
1.126 - COMBB_def ~> Meson.COMBB_def
1.127 - COMBC_def ~> Meson.COMBC_def
1.128 - COMBS_def ~> Meson.COMBS_def
1.129 - abs_I ~> Meson.abs_I
1.130 - abs_K ~> Meson.abs_K
1.131 - abs_B ~> Meson.abs_B
1.132 - abs_C ~> Meson.abs_C
1.133 - abs_S ~> Meson.abs_S
1.134 - INCOMPATIBILITY.
1.135 + - Added "smt" and "remote_smt" provers based on the "smt" proof
1.136 + method. See the Sledgehammer manual for details ("isabelle doc
1.137 + sledgehammer").
1.138 - Renamed commands:
1.139 sledgehammer atp_info ~> sledgehammer running_provers
1.140 sledgehammer atp_kill ~> sledgehammer kill_provers
1.141 @@ -260,18 +245,11 @@
1.142 (and "ms" and "min" are no longer supported)
1.143 INCOMPATIBILITY.
1.144
1.145 -* Metis and Meson now have configuration options "meson_trace",
1.146 -"metis_trace", and "metis_verbose" that can be enabled to diagnose
1.147 -these tools. E.g.
1.148 -
1.149 - using [[metis_trace = true]]
1.150 -
1.151 * Nitpick:
1.152 - Renamed options:
1.153 nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
1.154 nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
1.155 INCOMPATIBILITY.
1.156 - - Now requires Kodkodi 1.2.9. INCOMPATIBILITY.
1.157 - Added support for partial quotient types.
1.158 - Added local versions of the "Nitpick.register_xxx" functions.
1.159 - Added "whack" option.
1.160 @@ -282,19 +260,26 @@
1.161 higher cardinalities.
1.162 - Prevent the expansion of too large definitions.
1.163
1.164 +* Proof methods "metis" and "meson" now have configuration options
1.165 +"meson_trace", "metis_trace", and "metis_verbose" that can be enabled
1.166 +to diagnose these tools. E.g.
1.167 +
1.168 + using [[metis_trace = true]]
1.169 +
1.170 * Auto Solve: Renamed "Auto Solve Direct". The tool is now available
1.171 manually as command 'solve_direct'.
1.172
1.173 -* The default SMT solver is now CVC3. Z3 must be enabled explicitly,
1.174 -due to licensing issues.
1.175 +* The default SMT solver is now CVC3. Z3 must be enabled explicitly
1.176 +(due to licensing issues) via Z3_NON_COMMERCIAL in etc/settings of the
1.177 +component, for example.
1.178
1.179 * Remote SMT solvers need to be referred to by the "remote_" prefix,
1.180 -i.e., "remote_cvc3" and "remote_z3".
1.181 -
1.182 -* Added basic SMT support for datatypes, records, and typedefs
1.183 -using the oracle mode (no proofs). Direct support of pairs has been
1.184 -dropped in exchange (pass theorems fst_conv snd_conv pair_collapse to
1.185 -the SMT support for a similar behaviour). MINOR INCOMPATIBILITY.
1.186 +i.e. "remote_cvc3" and "remote_z3".
1.187 +
1.188 +* Added basic SMT support for datatypes, records, and typedefs using
1.189 +the oracle mode (no proofs). Direct support of pairs has been dropped
1.190 +in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT
1.191 +support for a similar behavior). Minor INCOMPATIBILITY.
1.192
1.193 * Changed SMT configuration options:
1.194 - Renamed:
1.195 @@ -315,7 +300,7 @@
1.196 * Boogie output files (.b2i files) need to be declared in the theory
1.197 header.
1.198
1.199 -* Dropped syntax for old primrec package. INCOMPATIBILITY.
1.200 +* Dropped syntax for old version of primrec package. INCOMPATIBILITY.
1.201
1.202 * Multivariate Analysis: Introduced a type class for euclidean
1.203 space. Most theorems are now stated in terms of euclidean spaces
1.204 @@ -337,11 +322,11 @@
1.205 of euclidean spaces the real and complex numbers are instantiated to
1.206 be euclidean_spaces. INCOMPATIBILITY.
1.207
1.208 -* Probability: Introduced pextreal as positive extended real numbers.
1.209 -Use pextreal as value for measures. Introduce the Radon-Nikodym
1.210 -derivative, product spaces and Fubini's theorem for arbitrary sigma
1.211 -finite measures. Introduces Lebesgue measure based on the integral in
1.212 -Multivariate Analysis. INCOMPATIBILITY.
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 @@ -354,12 +339,12 @@
1.222 Set_Algebras; canonical names for instance definitions for functions;
1.223 various improvements. INCOMPATIBILITY.
1.224
1.225 -* Theory Multiset provides stable quicksort implementation of
1.226 +* Theory Library/Multiset provides stable quicksort implementation of
1.227 sort_key.
1.228
1.229 -* Theory Enum (for explicit enumerations of finite types) is now part
1.230 -of the HOL-Main image. INCOMPATIBILITY: all constants of the Enum
1.231 -theory now have to be referred to by its qualified name.
1.232 +* Former theory Library/Enum is now part of the HOL-Main image.
1.233 +INCOMPATIBILITY: all constants of the Enum theory now have to be
1.234 +referred to by its qualified name.
1.235
1.236 enum ~> Enum.enum
1.237 nlists ~> Enum.nlists
1.238 @@ -373,9 +358,8 @@
1.239 * Removed [split_format ... and ... and ...] version of
1.240 [split_format]. Potential INCOMPATIBILITY.
1.241
1.242 -* Predicate "sorted" now defined inductively, with
1.243 -nice induction rules. INCOMPATIBILITY: former sorted.simps now
1.244 -named sorted_simps.
1.245 +* Predicate "sorted" now defined inductively, with nice induction
1.246 +rules. INCOMPATIBILITY: former sorted.simps now named sorted_simps.
1.247
1.248 * Constant "contents" renamed to "the_elem", to free the generic name
1.249 contents for other uses. INCOMPATIBILITY.
1.250 @@ -386,12 +370,14 @@
1.251
1.252 * Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY.
1.253
1.254 -* Removed output syntax "'a ~=> 'b" for "'a => 'b option". INCOMPATIBILITY.
1.255 +* Removed output syntax "'a ~=> 'b" for "'a => 'b option".
1.256 +INCOMPATIBILITY.
1.257
1.258 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
1.259 avoid confusion with finite sets. INCOMPATIBILITY.
1.260
1.261 -* Multiset.thy: renamed empty_idemp ~> empty_neutral. INCOMPATIBILITY.
1.262 +* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral.
1.263 +INCOMPATIBILITY.
1.264
1.265 * Abandoned locales equiv, congruent and congruent2 for equivalence
1.266 relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same
1.267 @@ -452,7 +438,7 @@
1.268
1.269 INCOMPATIBILITY.
1.270
1.271 -* Refactoring of code-generation specific operations in List.thy
1.272 +* Refactoring of code-generation specific operations in theory List:
1.273
1.274 constants
1.275 null ~> List.null
1.276 @@ -468,37 +454,15 @@
1.277 Various operations from the Haskell prelude are used for generating
1.278 Haskell code.
1.279
1.280 -* MESON: Renamed lemmas:
1.281 - meson_not_conjD ~> Meson.not_conjD
1.282 - meson_not_disjD ~> Meson.not_disjD
1.283 - meson_not_notD ~> Meson.not_notD
1.284 - meson_not_allD ~> Meson.not_allD
1.285 - meson_not_exD ~> Meson.not_exD
1.286 - meson_imp_to_disjD ~> Meson.imp_to_disjD
1.287 - meson_not_impD ~> Meson.not_impD
1.288 - meson_iff_to_disjD ~> Meson.iff_to_disjD
1.289 - meson_not_iffD ~> Meson.not_iffD
1.290 - meson_not_refl_disj_D ~> Meson.not_refl_disj_D
1.291 - meson_conj_exD1 ~> Meson.conj_exD1
1.292 - meson_conj_exD2 ~> Meson.conj_exD2
1.293 - meson_disj_exD ~> Meson.disj_exD
1.294 - meson_disj_exD1 ~> Meson.disj_exD1
1.295 - meson_disj_exD2 ~> Meson.disj_exD2
1.296 - meson_disj_assoc ~> Meson.disj_assoc
1.297 - meson_disj_comm ~> Meson.disj_comm
1.298 - meson_disj_FalseD1 ~> Meson.disj_FalseD1
1.299 - meson_disj_FalseD2 ~> Meson.disj_FalseD2
1.300 -INCOMPATIBILITY.
1.301 -
1.302 -* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f"
1.303 -is now an abbreviation of "range f = UNIV". The theorems bij_def and
1.304 -surj_def are unchanged. INCOMPATIBILITY.
1.305 +* Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". Term
1.306 +"surj f" is now an abbreviation of "range f = UNIV". The theorems
1.307 +bij_def and surj_def are unchanged. INCOMPATIBILITY.
1.308
1.309 * Abolished some non-alphabetic type names: "prod" and "sum" replace
1.310 "*" and "+" respectively. INCOMPATIBILITY.
1.311
1.312 * Name "Plus" of disjoint sum operator "<+>" is now hidden. Write
1.313 -Sum_Type.Plus.
1.314 +"Sum_Type.Plus" instead.
1.315
1.316 * Constant "split" has been merged with constant "prod_case"; names of
1.317 ML functions, facts etc. involving split have been retained so far,
1.318 @@ -507,7 +471,7 @@
1.319 * Dropped old infix syntax "_ mem _" for List.member; use "_ : set _"
1.320 instead. INCOMPATIBILITY.
1.321
1.322 -* Removed lemma Option.is_none_none (Duplicate of is_none_def).
1.323 +* Removed lemma "Option.is_none_none" which duplicates "is_none_def".
1.324 INCOMPATIBILITY.
1.325
1.326
1.327 @@ -519,79 +483,80 @@
1.328 qualifier 'add'. Previous theorem names are redeclared for
1.329 compatibility.
1.330
1.331 -* Structure 'int_ring' is now an abbreviation (previously a
1.332 +* Structure "int_ring" is now an abbreviation (previously a
1.333 definition). This fits more natural with advanced interpretations.
1.334
1.335
1.336 *** HOLCF ***
1.337
1.338 * The domain package now runs in definitional mode by default: The
1.339 -former command 'new_domain' is now called 'domain'. To use the domain
1.340 +former command 'new_domain' is now called 'domain'. To use the domain
1.341 package in its original axiomatic mode, use 'domain (unsafe)'.
1.342 INCOMPATIBILITY.
1.343
1.344 -* The new class 'domain' is now the default sort. Class 'predomain' is
1.345 -an unpointed version of 'domain'. Theories can be updated by replacing
1.346 -sort annotations as shown below. INCOMPATIBILITY.
1.347 +* The new class "domain" is now the default sort. Class "predomain"
1.348 +is an unpointed version of "domain". Theories can be updated by
1.349 +replacing sort annotations as shown below. INCOMPATIBILITY.
1.350
1.351 'a::type ~> 'a::countable
1.352 'a::cpo ~> 'a::predomain
1.353 'a::pcpo ~> 'a::domain
1.354
1.355 -* The old type class 'rep' has been superseded by class 'domain'.
1.356 +* The old type class "rep" has been superseded by class "domain".
1.357 Accordingly, users of the definitional package must remove any
1.358 -'default_sort rep' declarations. INCOMPATIBILITY.
1.359 +"default_sort rep" declarations. INCOMPATIBILITY.
1.360
1.361 * The domain package (definitional mode) now supports unpointed
1.362 predomain argument types, as long as they are marked 'lazy'. (Strict
1.363 -arguments must be in class 'domain'.) For example, the following
1.364 +arguments must be in class "domain".) For example, the following
1.365 domain definition now works:
1.366
1.367 domain natlist = nil | cons (lazy "nat discr") (lazy "natlist")
1.368
1.369 * Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class
1.370 -instances for types from Isabelle/HOL: bool, nat, int, char, 'a + 'b,
1.371 -'a option, and 'a list. Additionally, it configures fixrec and the
1.372 -domain package to work with these types. For example:
1.373 +instances for types from main HOL: bool, nat, int, char, 'a + 'b,
1.374 +'a option, and 'a list. Additionally, it configures fixrec and the
1.375 +domain package to work with these types. For example:
1.376
1.377 fixrec isInl :: "('a + 'b) u -> tr"
1.378 where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF"
1.379
1.380 domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list")
1.381
1.382 -* The '(permissive)' option of fixrec has been replaced with a
1.383 -per-equation '(unchecked)' option. See HOLCF/Tutorial/Fixrec_ex.thy
1.384 -for examples. INCOMPATIBILITY.
1.385 -
1.386 -* The 'bifinite' class no longer fixes a constant 'approx'; the class
1.387 -now just asserts that such a function exists. INCOMPATIBILITY.
1.388 -
1.389 -* The type 'alg_defl' has been renamed to 'defl'. HOLCF no longer
1.390 +* The "(permissive)" option of fixrec has been replaced with a
1.391 +per-equation "(unchecked)" option. See
1.392 +src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY.
1.393 +
1.394 +* The "bifinite" class no longer fixes a constant "approx"; the class
1.395 +now just asserts that such a function exists. INCOMPATIBILITY.
1.396 +
1.397 +* Former type "alg_defl" has been renamed to "defl". HOLCF no longer
1.398 defines an embedding of type 'a defl into udom by default; instances
1.399 -of 'bifinite' and 'domain' classes are available in
1.400 -HOLCF/Library/Defl_Bifinite.thy.
1.401 -
1.402 -* The syntax 'REP('a)' has been replaced with 'DEFL('a)'.
1.403 -
1.404 -* The predicate 'directed' has been removed. INCOMPATIBILITY.
1.405 -
1.406 -* The type class 'finite_po' has been removed. INCOMPATIBILITY.
1.407 -
1.408 -* The function 'cprod_map' has been renamed to 'prod_map'.
1.409 +of "bifinite" and "domain" classes are available in
1.410 +src/HOL/HOLCF/Library/Defl_Bifinite.thy.
1.411 +
1.412 +* The syntax "REP('a)" has been replaced with "DEFL('a)".
1.413 +
1.414 +* The predicate "directed" has been removed. INCOMPATIBILITY.
1.415 +
1.416 +* The type class "finite_po" has been removed. INCOMPATIBILITY.
1.417 +
1.418 +* The function "cprod_map" has been renamed to "prod_map".
1.419 INCOMPATIBILITY.
1.420
1.421 * The monadic bind operator on each powerdomain has new binder syntax
1.422 -similar to sets, e.g. '\<Union>\<sharp>x\<in>xs. t' represents
1.423 -'upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)'.
1.424 +similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents
1.425 +"upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)".
1.426
1.427 * The infix syntax for binary union on each powerdomain has changed
1.428 -from e.g. '+\<sharp>' to '\<union>\<sharp>', for consistency with set
1.429 -syntax. INCOMPATIBILITY.
1.430 -
1.431 -* The constant 'UU' has been renamed to 'bottom'. The syntax 'UU' is
1.432 +from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set
1.433 +syntax. INCOMPATIBILITY.
1.434 +
1.435 +* The constant "UU" has been renamed to "bottom". The syntax "UU" is
1.436 still supported as an input translation.
1.437
1.438 * Renamed some theorems (the original names are also still available).
1.439 +
1.440 expand_fun_below ~> fun_below_iff
1.441 below_fun_ext ~> fun_belowI
1.442 expand_cfun_eq ~> cfun_eq_iff
1.443 @@ -602,6 +567,7 @@
1.444
1.445 * The Abs and Rep functions for various types have changed names.
1.446 Related theorem names have also changed to match. INCOMPATIBILITY.
1.447 +
1.448 Rep_CFun ~> Rep_cfun
1.449 Abs_CFun ~> Abs_cfun
1.450 Rep_Sprod ~> Rep_sprod
1.451 @@ -610,20 +576,23 @@
1.452 Abs_Ssum ~> Abs_ssum
1.453
1.454 * Lemmas with names of the form *_defined_iff or *_strict_iff have
1.455 -been renamed to *_bottom_iff. INCOMPATIBILITY.
1.456 +been renamed to *_bottom_iff. INCOMPATIBILITY.
1.457
1.458 * Various changes to bisimulation/coinduction with domain package:
1.459 - - Definitions of 'bisim' constants no longer mention definedness.
1.460 - - With mutual recursion, 'bisim' predicate is now curried.
1.461 +
1.462 + - Definitions of "bisim" constants no longer mention definedness.
1.463 + - With mutual recursion, "bisim" predicate is now curried.
1.464 - With mutual recursion, each type gets a separate coind theorem.
1.465 - Variable names in bisim_def and coinduct rules have changed.
1.466 +
1.467 INCOMPATIBILITY.
1.468
1.469 -* Case combinators generated by the domain package for type 'foo' are
1.470 -now named 'foo_case' instead of 'foo_when'. INCOMPATIBILITY.
1.471 +* Case combinators generated by the domain package for type "foo" are
1.472 +now named "foo_case" instead of "foo_when". INCOMPATIBILITY.
1.473
1.474 * Several theorems have been renamed to more accurately reflect the
1.475 -names of constants and types involved. INCOMPATIBILITY.
1.476 +names of constants and types involved. INCOMPATIBILITY.
1.477 +
1.478 thelub_const ~> lub_const
1.479 lub_const ~> is_lub_const
1.480 thelubI ~> lub_eqI
1.481 @@ -645,7 +614,8 @@
1.482 deflation_UU ~> deflation_bottom
1.483 finite_deflation_UU ~> finite_deflation_bottom
1.484
1.485 -* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
1.486 +* Many legacy theorem names have been discontinued. INCOMPATIBILITY.
1.487 +
1.488 sq_ord_less_eq_trans ~> below_eq_trans
1.489 sq_ord_eq_less_trans ~> eq_below_trans
1.490 refl_less ~> below_refl
1.491 @@ -699,7 +669,6 @@
1.492 identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY.
1.493
1.494
1.495 -
1.496 *** ML ***
1.497
1.498 * Renamed structure MetaSimplifier to Raw_Simplifier. Note that the