NEWS
changeset 57452 ecad2a53755a
parent 57443 577f029fde39
child 57474 250decee4ac5
     1.1 --- a/NEWS	Tue Jul 01 14:05:05 2014 +0200
     1.2 +++ b/NEWS	Tue Jul 01 14:52:08 2014 +0200
     1.3 @@ -1,32 +1,19 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle version
     1.8 -----------------------------
     1.9 +New in Isabelle2014 (August 2014)
    1.10 +---------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14 -* Document antiquotation @{url} produces markup for the given URL,
    1.15 -which results in an active hyperlink within the text.
    1.16 -
    1.17 -* Document antiquotation @{file_unchecked} is like @{file}, but does
    1.18 -not check existence within the file-system.
    1.19 -
    1.20 -* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML
    1.21 -workaround in Isabelle2013-1.  The prover process no longer accepts
    1.22 -old identifier syntax with \<^isub> or \<^isup>.
    1.23 -
    1.24 -* Syntax of document antiquotation @{rail} now uses \<newline> instead
    1.25 -of "\\", to avoid the optical illusion of escaped backslash within
    1.26 -string token.  Minor INCOMPATIBILITY.
    1.27 -
    1.28 -* Lexical syntax (inner and outer) supports text cartouches with
    1.29 -arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    1.30 -supports input via ` (backquote).
    1.31 -
    1.32 -* The outer syntax categories "text" (for formal comments and document
    1.33 -markup commands) and "altstring" (for literal fact references) allow
    1.34 -cartouches as well, in addition to the traditional mix of quotations.
    1.35 +* Support for official Standard ML within the Isabelle context.
    1.36 +Command 'SML_file' reads and evaluates the given Standard ML file.
    1.37 +Toplevel bindings are stored within the theory context; the initial
    1.38 +environment is restricted to the Standard ML implementation of
    1.39 +Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    1.40 +and 'SML_export' allow to exchange toplevel bindings between the two
    1.41 +separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    1.42 +some examples.
    1.43  
    1.44  * More static checking of proof methods, which allows the system to
    1.45  form a closure over the concrete syntax.  Method arguments should be
    1.46 @@ -37,25 +24,48 @@
    1.47  exception.  Potential INCOMPATIBILITY for non-conformant tactical
    1.48  proof tools.
    1.49  
    1.50 -* Support for official Standard ML within the Isabelle context.
    1.51 -Command 'SML_file' reads and evaluates the given Standard ML file.
    1.52 -Toplevel bindings are stored within the theory context; the initial
    1.53 -environment is restricted to the Standard ML implementation of
    1.54 -Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    1.55 -and 'SML_export' allow to exchange toplevel bindings between the two
    1.56 -separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    1.57 -some examples.
    1.58 -
    1.59 -* Updated and extended manuals: "codegen", "datatypes",
    1.60 -"implementation", "jedit", "system".
    1.61 +* Lexical syntax (inner and outer) supports text cartouches with
    1.62 +arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    1.63 +supports input via ` (backquote).
    1.64 +
    1.65 +* The outer syntax categories "text" (for formal comments and document
    1.66 +markup commands) and "altstring" (for literal fact references) allow
    1.67 +cartouches as well, in addition to the traditional mix of quotations.
    1.68 +
    1.69 +* Syntax of document antiquotation @{rail} now uses \<newline> instead
    1.70 +of "\\", to avoid the optical illusion of escaped backslash within
    1.71 +string token.  General renovation of its syntax using text cartouces.
    1.72 +Minor INCOMPATIBILITY.
    1.73 +
    1.74 +* Discontinued legacy_isub_isup, which was a temporary workaround for
    1.75 +Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts
    1.76 +old identifier syntax with \<^isub> or \<^isup>.  Potential
    1.77 +INCOMPATIBILITY.
    1.78 +
    1.79 +* Document antiquotation @{url} produces markup for the given URL,
    1.80 +which results in an active hyperlink within the text.
    1.81 +
    1.82 +* Document antiquotation @{file_unchecked} is like @{file}, but does
    1.83 +not check existence within the file-system.
    1.84 +
    1.85 +* Updated and extended manuals: codegen, datatypes, implementation,
    1.86 +isar-ref, jedit, system.
    1.87  
    1.88  
    1.89  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.90  
    1.91 -* Document panel: simplied interaction where every single mouse click
    1.92 -(re)opens document via desktop environment or as jEdit buffer.
    1.93 -
    1.94 -* Support for Navigator plugin (with toolbar buttons).
    1.95 +* Improved Document panel: simplied interaction where every single
    1.96 +mouse click (re)opens document via desktop environment or as jEdit
    1.97 +buffer.
    1.98 +
    1.99 +* Support for Navigator plugin (with toolbar buttons), with connection
   1.100 +to PIDE hyperlinks.
   1.101 +
   1.102 +* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
   1.103 +Open text buffers take precedence over copies within the file-system.
   1.104 +
   1.105 +* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
   1.106 +auxiliary ML files.
   1.107  
   1.108  * Improved syntactic and semantic completion mechanism, with simple
   1.109  templates, completion language context, name-space completion,
   1.110 @@ -72,12 +82,6 @@
   1.111  * Integrated spell-checker for document text, comments etc. with
   1.112  completion popup and context-menu.
   1.113  
   1.114 -* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
   1.115 -Open text buffers take precedence over copies within the file-system.
   1.116 -
   1.117 -* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
   1.118 -auxiliary ML files.
   1.119 -
   1.120  * More general "Query" panel supersedes "Find" panel, with GUI access
   1.121  to commands 'find_theorems' and 'find_consts', as well as print
   1.122  operations for the context.  Minor incompatibility in keyboard
   1.123 @@ -91,10 +95,6 @@
   1.124  process, without requiring old-fashioned command-line invocation of
   1.125  "isabelle jedit -m MODE".
   1.126  
   1.127 -* New Simplifier Trace panel provides an interactive view of the
   1.128 -simplification process, enabled by the "simplifier_trace" attribute
   1.129 -within the context.
   1.130 -
   1.131  * More support for remote files (e.g. http) using standard Java
   1.132  networking operations instead of jEdit virtual file-systems.
   1.133  
   1.134 @@ -105,6 +105,11 @@
   1.135  and window placement wrt. main editor view; optional menu item to
   1.136  "Detach" a copy where this makes sense.
   1.137  
   1.138 +* New Simplifier Trace panel provides an interactive view of the
   1.139 +simplification process, enabled by the "simplifier_trace" attribute
   1.140 +within the context.
   1.141 +
   1.142 +
   1.143  
   1.144  *** Pure ***
   1.145  
   1.146 @@ -139,12 +144,12 @@
   1.147  * Low-level type-class commands 'classes', 'classrel', 'arities' have
   1.148  been discontinued to avoid the danger of non-trivial axiomatization
   1.149  that is not immediately visible.  INCOMPATIBILITY, use regular
   1.150 -'instance' with proof.  The required OFCLASS(...) theorem might be
   1.151 -postulated via 'axiomatization' beforehand, or the proof finished
   1.152 -trivially if the underlying class definition is made vacuous (without
   1.153 -any assumptions).  See also Isabelle/ML operations
   1.154 -Axclass.axiomatize_class, Axclass.axiomatize_classrel,
   1.155 -Axclass.axiomatize_arity.
   1.156 +'instance' command with proof.  The required OFCLASS(...) theorem
   1.157 +might be postulated via 'axiomatization' beforehand, or the proof
   1.158 +finished trivially if the underlying class definition is made vacuous
   1.159 +(without any assumptions).  See also Isabelle/ML operations
   1.160 +Axclass.class_axiomatization, Axclass.classrel_axiomatization,
   1.161 +Axclass.arity_axiomatization.
   1.162  
   1.163  * Attributes "where" and "of" allow an optional context of local
   1.164  variables ('for' declaration): these variables become schematic in the
   1.165 @@ -167,10 +172,10 @@
   1.166  
   1.167  * Inner syntax token language allows regular quoted strings "..."
   1.168  (only makes sense in practice, if outer syntax is delimited
   1.169 -differently).
   1.170 -
   1.171 -* Code generator preprocessor: explicit control of simp tracing
   1.172 -on a per-constant basis.  See attribute "code_preproc".
   1.173 +differently, e.g. via cartouches).
   1.174 +
   1.175 +* Code generator preprocessor: explicit control of simp tracing on a
   1.176 +per-constant basis.  See attribute "code_preproc".
   1.177  
   1.178  * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
   1.179  but the latter is retained some time as Proof General legacy.
   1.180 @@ -180,63 +185,68 @@
   1.181  
   1.182  * Qualified String.implode and String.explode.  INCOMPATIBILITY.
   1.183  
   1.184 -* Command and antiquotation ''value'' are hardcoded against nbe and
   1.185 -ML now.  Minor INCOMPATIBILITY.
   1.186 -
   1.187 -* Separate command ''approximate'' for approximative computation
   1.188 -in Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   1.189 +* Command and antiquotation "value" are now hardcoded against nbe and
   1.190 +ML.  Minor INCOMPATIBILITY.
   1.191 +
   1.192 +* Separate command "approximate" for approximative computation in
   1.193 +src/HOL/Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   1.194  
   1.195  * Adjustion of INF and SUP operations:
   1.196 -  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   1.197 -  * Consolidated theorem names containing INFI and SUPR: have INF
   1.198 -  and SUP instead uniformly.
   1.199 -  * More aggressive normalization of expressions involving INF and Inf
   1.200 -  or SUP and Sup.
   1.201 -  * INF_image and SUP_image do not unfold composition.
   1.202 -  * Dropped facts INF_comp, SUP_comp.
   1.203 -  * Default congruence rules strong_INF_cong and strong_SUP_cong,
   1.204 -  with simplifier implication in premises.  Generalize and replace
   1.205 -  former INT_cong, SUP_cong
   1.206 +  - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   1.207 +  - Consolidated theorem names containing INFI and SUPR: have INF and
   1.208 +    SUP instead uniformly.
   1.209 +  - More aggressive normalization of expressions involving INF and Inf
   1.210 +    or SUP and Sup.
   1.211 +  - INF_image and SUP_image do not unfold composition.
   1.212 +  - Dropped facts INF_comp, SUP_comp.
   1.213 +  - Default congruence rules strong_INF_cong and strong_SUP_cong, with
   1.214 +    simplifier implication in premises.  Generalize and replace former
   1.215 +    INT_cong, SUP_cong
   1.216 +
   1.217  INCOMPATIBILITY.
   1.218  
   1.219  * Swapped orientation of facts image_comp and vimage_comp:
   1.220 +
   1.221    image_compose ~> image_comp [symmetric]
   1.222    image_comp ~> image_comp [symmetric]
   1.223    vimage_compose ~> vimage_comp [symmetric]
   1.224    vimage_comp ~> vimage_comp [symmetric]
   1.225 -  INCOMPATIBILITY.
   1.226 -
   1.227 -* Simplifier: Enhanced solver of preconditions of rewrite rules
   1.228 -  can now deal with conjunctions.
   1.229 -  For help with converting proofs, the old behaviour of the simplifier
   1.230 -  can be restored like this:  declare/using [[simp_legacy_precond]]
   1.231 -  This configuration option will disappear again in the future.
   1.232 +
   1.233 +INCOMPATIBILITY.
   1.234 +
   1.235 +* Simplifier: Enhanced solver of preconditions of rewrite rules can
   1.236 +now deal with conjunctions.  For help with converting proofs, the old
   1.237 +behaviour of the simplifier can be restored like this: declare/using
   1.238 +[[simp_legacy_precond]].  This configuration option will disappear
   1.239 +again in the future.  INCOMPATIBILITY.
   1.240  
   1.241  * HOL-Word:
   1.242 -  * Abandoned fact collection "word_arith_alts", which is a
   1.243 -  duplicate of "word_arith_wis".
   1.244 -  * Dropped first (duplicated) element in fact collections
   1.245 -  "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   1.246 -  "uint_word_arith_bintrs".
   1.247 -
   1.248 -* Code generator: enforce case of identifiers only for strict
   1.249 -target language requirements.  INCOMPATIBILITY.
   1.250 +  - Abandoned fact collection "word_arith_alts", which is a duplicate
   1.251 +    of "word_arith_wis".
   1.252 +  - Dropped first (duplicated) element in fact collections
   1.253 +    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   1.254 +    "uint_word_arith_bintrs".
   1.255 +
   1.256 +* Code generator: enforce case of identifiers only for strict target
   1.257 +language requirements.  INCOMPATIBILITY.
   1.258  
   1.259  * Code generator: explicit proof contexts in many ML interfaces.
   1.260  INCOMPATIBILITY.
   1.261  
   1.262 -* Code generator: minimize exported identifiers by default.
   1.263 -Minor INCOMPATIBILITY.
   1.264 -
   1.265 -* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
   1.266 -Minor INCOMPATIBILITY.
   1.267 +* Code generator: minimize exported identifiers by default.  Minor
   1.268 +INCOMPATIBILITY.
   1.269 +
   1.270 +* Code generation for SML and OCaml: dropped arcane "no_signatures"
   1.271 +option.  Minor INCOMPATIBILITY.
   1.272  
   1.273  * Simproc "finite_Collect" is no longer enabled by default, due to
   1.274  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
   1.275  
   1.276 -* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   1.277 -  The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
   1.278 -  "primcorec", and "primcorecursive" commands are now part of "Main".
   1.279 +* Moved new (co)datatype package and its dependencies from session
   1.280 +  "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',
   1.281 +  'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
   1.282 +  part of theory "Main".
   1.283 +
   1.284    Theory renamings:
   1.285      FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
   1.286      Library/Wfrec.thy ~> Wfrec.thy
   1.287 @@ -260,58 +270,63 @@
   1.288      BNF/More_BNFs.thy ~> Library/More_BNFs.thy
   1.289      BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
   1.290      BNF/Examples/* ~> BNF_Examples/*
   1.291 +
   1.292    New theories:
   1.293      Wellorder_Extension.thy (split from Zorn.thy)
   1.294      Library/Cardinal_Notations.thy
   1.295      Library/BNF_Axomatization.thy
   1.296      BNF_Examples/Misc_Primcorec.thy
   1.297      BNF_Examples/Stream_Processor.thy
   1.298 +
   1.299    Discontinued theories:
   1.300      BNF/BNF.thy
   1.301      BNF/Equiv_Relations_More.thy
   1.302 -  INCOMPATIBILITY.
   1.303 +
   1.304 +INCOMPATIBILITY.
   1.305  
   1.306  * New (co)datatype package:
   1.307 -  * "primcorec" is fully implemented.
   1.308 -  * "datatype_new" generates size functions ("size_xxx" and "size") as
   1.309 -    required by "fun".
   1.310 -  * BNFs are integrated with the Lifting tool and new-style (co)datatypes
   1.311 -    with Transfer.
   1.312 -  * Renamed commands:
   1.313 +  - Command 'primcorec' is fully implemented.
   1.314 +  - Command 'datatype_new' generates size functions ("size_xxx" and
   1.315 +    "size") as required by 'fun'.
   1.316 +  - BNFs are integrated with the Lifting tool and new-style
   1.317 +    (co)datatypes with Transfer.
   1.318 +  - Renamed commands:
   1.319        datatype_new_compat ~> datatype_compat
   1.320        primrec_new ~> primrec
   1.321        wrap_free_constructors ~> free_constructors
   1.322      INCOMPATIBILITY.
   1.323 -  * The generated constants "xxx_case" and "xxx_rec" have been renamed
   1.324 +  - The generated constants "xxx_case" and "xxx_rec" have been renamed
   1.325      "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
   1.326      INCOMPATIBILITY.
   1.327 -  * The constant "xxx_(un)fold" and related theorems are no longer generated.
   1.328 -    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
   1.329 +  - The constant "xxx_(un)fold" and related theorems are no longer
   1.330 +    generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually
   1.331 +    using "prim(co)rec".
   1.332      INCOMPATIBILITY.
   1.333 -  * No discriminators are generated for nullary constructors by default,
   1.334 -    eliminating the need for the odd "=:" syntax.
   1.335 +  - No discriminators are generated for nullary constructors by
   1.336 +    default, eliminating the need for the odd "=:" syntax.
   1.337      INCOMPATIBILITY.
   1.338 -  * No discriminators or selectors are generated by default by
   1.339 +  - No discriminators or selectors are generated by default by
   1.340      "datatype_new", unless custom names are specified or the new
   1.341      "discs_sels" option is passed.
   1.342      INCOMPATIBILITY.
   1.343  
   1.344  * Old datatype package:
   1.345 -  * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
   1.346 -    "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
   1.347 -    INCOMPATIBILITY.
   1.348 -  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
   1.349 -    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
   1.350 -    "case_prod").
   1.351 -    INCOMPATIBILITY.
   1.352 -
   1.353 -* The types "'a list" and "'a option", their set and map functions, their
   1.354 -  relators, and their selectors are now produced using the new BNF-based
   1.355 -  datatype package.
   1.356 +  - The generated theorems "xxx.cases" and "xxx.recs" have been
   1.357 +    renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
   1.358 +    "sum.case").  INCOMPATIBILITY.
   1.359 +  - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
   1.360 +    been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
   1.361 +    "prod_case" ~> "case_prod").  INCOMPATIBILITY.
   1.362 +
   1.363 +* The types "'a list" and "'a option", their set and map functions,
   1.364 +  their relators, and their selectors are now produced using the new
   1.365 +  BNF-based datatype package.
   1.366 +
   1.367    Renamed constants:
   1.368      Option.set ~> set_option
   1.369      Option.map ~> map_option
   1.370      option_rel ~> rel_option
   1.371 +
   1.372    Renamed theorems:
   1.373      set_def ~> set_rec[abs_def]
   1.374      map_def ~> map_rec[abs_def]
   1.375 @@ -323,7 +338,8 @@
   1.376      hd.simps ~> list.sel(1)
   1.377      tl.simps ~> list.sel(2-3)
   1.378      the.simps ~> option.sel
   1.379 -  INCOMPATIBILITY.
   1.380 +
   1.381 +INCOMPATIBILITY.
   1.382  
   1.383  * The following map functions and relators have been renamed:
   1.384      sum_map ~> map_sum
   1.385 @@ -333,16 +349,18 @@
   1.386      fun_rel ~> rel_fun
   1.387      set_rel ~> rel_set
   1.388      filter_rel ~> rel_filter
   1.389 -    fset_rel ~> rel_fset (in "Library/FSet.thy")
   1.390 -    cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
   1.391 -    vset ~> rel_vset (in "Library/Quotient_Set.thy")
   1.392 -
   1.393 -* New theories:
   1.394 -    Cardinals/Ordinal_Arithmetic.thy
   1.395 -    Library/Tree
   1.396 -
   1.397 -* Theory reorganizations:
   1.398 -  * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   1.399 +    fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
   1.400 +    cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
   1.401 +    vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
   1.402 +
   1.403 +INCOMPATIBILITY.
   1.404 +
   1.405 +* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   1.406 +
   1.407 +* New theory src/HOL/Library/Tree.thy.
   1.408 +
   1.409 +* Theory reorganization:
   1.410 +  Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   1.411  
   1.412  * Consolidated some facts about big group operators:
   1.413  
   1.414 @@ -411,41 +429,41 @@
   1.415    Dropped setsum_reindex_id, setprod_reindex_id
   1.416      (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
   1.417  
   1.418 -  INCOMPATIBILITY.
   1.419 -
   1.420 -* New internal SAT solver "cdclite" that produces models and proof traces.
   1.421 -  This solver replaces the internal SAT solvers "enumerate" and "dpll".
   1.422 -  Applications that explicitly used one of these two SAT solvers should
   1.423 -  use "cdclite" instead. In addition, "cdclite" is now the default SAT
   1.424 -  solver for the "sat" and "satx" proof methods and corresponding tactics;
   1.425 -  the old default can be restored using
   1.426 -  "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
   1.427 -
   1.428 -* SMT module:
   1.429 -  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
   1.430 -    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
   1.431 -    called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no
   1.432 -    longer supported, because no version of the solver can handle both
   1.433 -    SMT-LIB 2 and quantifiers.
   1.434 +INCOMPATIBILITY.
   1.435 +
   1.436 +* New internal SAT solver "cdclite" that produces models and proof
   1.437 +traces.  This solver replaces the internal SAT solvers "enumerate" and
   1.438 +"dpll".  Applications that explicitly used one of these two SAT
   1.439 +solvers should use "cdclite" instead. In addition, "cdclite" is now
   1.440 +the default SAT solver for the "sat" and "satx" proof methods and
   1.441 +corresponding tactics; the old default can be restored using "declare
   1.442 +[[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.
   1.443 +
   1.444 +* SMT module: A new version of the SMT module, temporarily called
   1.445 +"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
   1.446 +4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
   1.447 +supported as oracles. Yices is no longer supported, because no version
   1.448 +of the solver can handle both SMT-LIB 2 and quantifiers.
   1.449  
   1.450  * Sledgehammer:
   1.451    - Z3 can now produce Isar proofs.
   1.452    - MaSh overhaul:
   1.453 -      - New SML-based learning engines eliminate the dependency on Python
   1.454 -        and increase performance and reliability.
   1.455 -      - MaSh and MeSh are now used by default together with the traditional
   1.456 -        MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
   1.457 -        system option in Plugin Options / Isabelle / General to "none".
   1.458 +    . New SML-based learning engines eliminate the dependency on
   1.459 +      Python and increase performance and reliability.
   1.460 +    . MaSh and MeSh are now used by default together with the
   1.461 +      traditional MePo (Meng-Paulson) relevance filter. To disable
   1.462 +      MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
   1.463 +      Options / Isabelle / General to "none".
   1.464    - New option:
   1.465        smt_proofs
   1.466    - Renamed options:
   1.467        isar_compress ~> compress
   1.468        isar_try0 ~> try0
   1.469 -    INCOMPATIBILITY.
   1.470 -
   1.471 -* Metis:
   1.472 -  - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead.
   1.473 -    INCOMPATIBILITY.
   1.474 +
   1.475 +INCOMPATIBILITY.
   1.476 +
   1.477 +* Metis: Removed legacy proof method 'metisFT'. Use 'metis
   1.478 +(full_types)' instead. INCOMPATIBILITY.
   1.479  
   1.480  * Try0: Added 'algebra' and 'meson' to the set of proof methods.
   1.481  
   1.482 @@ -467,7 +485,7 @@
   1.483  
   1.484  * Abolished slightly odd global lattice interpretation for min/max.
   1.485  
   1.486 -Fact consolidations:
   1.487 +  Fact consolidations:
   1.488      min_max.inf_assoc ~> min.assoc
   1.489      min_max.inf_commute ~> min.commute
   1.490      min_max.inf_left_commute ~> min.left_commute
   1.491 @@ -513,18 +531,18 @@
   1.492  min.left_commute, min.left_idem, max.commute, max.assoc,
   1.493  max.left_commute, max.left_idem directly.
   1.494  
   1.495 -For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
   1.496 -max.cobounded1m max.cobounded2 directly.
   1.497 +For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
   1.498 +min.cobounded2, max.cobounded1m max.cobounded2 directly.
   1.499  
   1.500  For min_ac or max_ac, prefer more general collection ac_simps.
   1.501  
   1.502  INCOMPATBILITY.
   1.503  
   1.504 -* Word library: bit representations prefer type bool over type bit.
   1.505 -INCOMPATIBILITY.
   1.506 -
   1.507 -* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
   1.508 -INCOMPATIBILITY.
   1.509 +* HOL-Word: bit representations prefer type bool over type bit.
   1.510 +INCOMPATIBILITY.
   1.511 +
   1.512 +* Theorem disambiguation Inf_le_Sup (on finite sets) ~>
   1.513 +Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
   1.514  
   1.515  * Code generations are provided for make, fields, extend and truncate
   1.516  operations on records.
   1.517 @@ -534,21 +552,25 @@
   1.518  
   1.519  * Fact generalization and consolidation:
   1.520      neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
   1.521 -INCOMPATIBILITY.
   1.522 -
   1.523 -* Purely algebraic definition of even.  Fact generalization and consolidation:
   1.524 +
   1.525 +INCOMPATIBILITY.
   1.526 +
   1.527 +* Purely algebraic definition of even.  Fact generalization and
   1.528 +  consolidation:
   1.529      nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
   1.530      even_zero_(nat|int) ~> even_zero
   1.531 +
   1.532  INCOMPATIBILITY.
   1.533  
   1.534  * Abolished neg_numeral.
   1.535 -  * Canonical representation for minus one is "- 1".
   1.536 -  * Canonical representation for other negative numbers is "- (numeral _)".
   1.537 -  * When devising rule sets for number calculation, consider the
   1.538 +  - Canonical representation for minus one is "- 1".
   1.539 +  - Canonical representation for other negative numbers is "- (numeral _)".
   1.540 +  - When devising rule sets for number calculation, consider the
   1.541      following canonical cases: 0, 1, numeral _, - 1, - numeral _.
   1.542 -  * HOLogic.dest_number also recognizes numerals in non-canonical forms
   1.543 +  - HOLogic.dest_number also recognizes numerals in non-canonical forms
   1.544      like "numeral One", "- numeral One", "- 0" and even "- ... - _".
   1.545 -  * Syntax for negative numerals is mere input syntax.
   1.546 +  - Syntax for negative numerals is mere input syntax.
   1.547 +
   1.548  INCOMPATIBILITY.
   1.549  
   1.550  * Elimination of fact duplicates:
   1.551 @@ -556,6 +578,7 @@
   1.552      diff_eq_0_iff_eq ~> right_minus_eq
   1.553      nat_infinite ~> infinite_UNIV_nat
   1.554      int_infinite ~> infinite_UNIV_int
   1.555 +
   1.556  INCOMPATIBILITY.
   1.557  
   1.558  * Fact name consolidation:
   1.559 @@ -564,6 +587,7 @@
   1.560      le_minus_self_iff ~> less_eq_neg_nonpos
   1.561      neg_less_nonneg ~> neg_less_pos
   1.562      less_minus_self_iff ~> less_neg_neg [simp]
   1.563 +
   1.564  INCOMPATIBILITY.
   1.565  
   1.566  * More simplification rules on unary and binary minus:
   1.567 @@ -571,9 +595,9 @@
   1.568  add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
   1.569  add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
   1.570  le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
   1.571 -minus_add_cancel, uminus_add_conv_diff.  These correspondingly
   1.572 -have been taken away from fact collections algebra_simps and
   1.573 -field_simps.  INCOMPATIBILITY.
   1.574 +minus_add_cancel, uminus_add_conv_diff.  These correspondingly have
   1.575 +been taken away from fact collections algebra_simps and field_simps.
   1.576 +INCOMPATIBILITY.
   1.577  
   1.578  To restore proofs, the following patterns are helpful:
   1.579  
   1.580 @@ -588,18 +612,18 @@
   1.581  or the brute way with
   1.582  "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
   1.583  
   1.584 -* SUP and INF generalized to conditionally_complete_lattice
   1.585 +* SUP and INF generalized to conditionally_complete_lattice.
   1.586  
   1.587  * Theory Lubs moved HOL image to HOL-Library. It is replaced by
   1.588 -Conditionally_Complete_Lattices.   INCOMPATIBILITY.
   1.589 -
   1.590 -* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
   1.591 -instead of explicitly stating boundedness of sets.
   1.592 -
   1.593 -* ccpo.admissible quantifies only over non-empty chains to allow
   1.594 -more syntax-directed proof rules; the case of the empty chain
   1.595 -shows up as additional case in fixpoint induction proofs.
   1.596 -INCOMPATIBILITY
   1.597 +Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   1.598 +
   1.599 +* Introduce bdd_above and bdd_below in theory
   1.600 +Conditionally_Complete_Lattices, use them instead of explicitly
   1.601 +stating boundedness of sets.
   1.602 +
   1.603 +* ccpo.admissible quantifies only over non-empty chains to allow more
   1.604 +syntax-directed proof rules; the case of the empty chain shows up as
   1.605 +additional case in fixpoint induction proofs.  INCOMPATIBILITY.
   1.606  
   1.607  * Removed and renamed theorems in Series:
   1.608    summable_le         ~>  suminf_le
   1.609 @@ -617,10 +641,13 @@
   1.610    removed series_zero, replaced by sums_finite
   1.611  
   1.612    removed auxiliary lemmas:
   1.613 +
   1.614      sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
   1.615 -    half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded,
   1.616 -    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
   1.617 -    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const
   1.618 +    half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
   1.619 +    real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
   1.620 +    sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
   1.621 +    summable_convergent_sumr_iff, sumr_diff_mult_const
   1.622 +
   1.623  INCOMPATIBILITY.
   1.624  
   1.625  * Replace (F)DERIV syntax by has_derivative:
   1.626 @@ -632,10 +659,10 @@
   1.627  
   1.628    - removed constant isDiff
   1.629  
   1.630 -  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input
   1.631 -    syntax.
   1.632 -
   1.633 -  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed
   1.634 +  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
   1.635 +    input syntax.
   1.636 +
   1.637 +  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.
   1.638  
   1.639    - Renamed FDERIV_... lemmas to has_derivative_...
   1.640  
   1.641 @@ -643,8 +670,9 @@
   1.642  
   1.643    - removed DERIV_intros, has_derivative_eq_intros
   1.644  
   1.645 -  - introduced derivative_intros and deriative_eq_intros which includes now rules for
   1.646 -    DERIV, has_derivative and has_vector_derivative.
   1.647 +  - introduced derivative_intros and deriative_eq_intros which
   1.648 +    includes now rules for DERIV, has_derivative and
   1.649 +    has_vector_derivative.
   1.650  
   1.651    - Other renamings:
   1.652      differentiable_def        ~>  real_differentiable_def
   1.653 @@ -654,24 +682,27 @@
   1.654      isDiff_der                ~>  differentiable_def
   1.655      deriv_fderiv              ~>  has_field_derivative_def
   1.656      deriv_def                 ~>  DERIV_def
   1.657 -INCOMPATIBILITY.
   1.658 -
   1.659 -* Include more theorems in continuous_intros. Remove the continuous_on_intros,
   1.660 -  isCont_intros collections, these facts are now in continuous_intros.
   1.661 -
   1.662 -* Theorems about complex numbers are now stated only using Re and Im, the Complex
   1.663 -  constructor is not used anymore. It is possible to use primcorec to defined the
   1.664 -  behaviour of a complex-valued function.
   1.665 -
   1.666 -  Removed theorems about the Complex constructor from the simpset, they are
   1.667 -  available as the lemma collection legacy_Complex_simps. This especially
   1.668 -  removes
   1.669 +
   1.670 +INCOMPATIBILITY.
   1.671 +
   1.672 +* Include more theorems in continuous_intros. Remove the
   1.673 +continuous_on_intros, isCont_intros collections, these facts are now
   1.674 +in continuous_intros.
   1.675 +
   1.676 +* Theorems about complex numbers are now stated only using Re and Im,
   1.677 +the Complex constructor is not used anymore. It is possible to use
   1.678 +primcorec to defined the behaviour of a complex-valued function.
   1.679 +
   1.680 +Removed theorems about the Complex constructor from the simpset, they
   1.681 +are available as the lemma collection legacy_Complex_simps. This
   1.682 +especially removes
   1.683 +
   1.684      i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
   1.685  
   1.686 -  Instead the reverse direction is supported with
   1.687 +Instead the reverse direction is supported with
   1.688      Complex_eq: "Complex a b = a + \<i> * b"
   1.689  
   1.690 -  Moved csqrt from Fundamental_Algebra_Theorem to Complex.
   1.691 +Moved csqrt from Fundamental_Algebra_Theorem to Complex.
   1.692  
   1.693    Renamings:
   1.694      Re/Im                  ~>  complex.sel
   1.695 @@ -701,36 +732,37 @@
   1.696      complex_inverse_def
   1.697      complex_scaleR_def
   1.698  
   1.699 +INCOMPATIBILITY.
   1.700 +
   1.701  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
   1.702  
   1.703  * Nitpick:
   1.704 -  - Fixed soundness bug whereby mutually recursive datatypes could take
   1.705 -    infinite values.
   1.706 -  - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
   1.707 -    "Rep_Integ".
   1.708 +  - Fixed soundness bug whereby mutually recursive datatypes could
   1.709 +    take infinite values.
   1.710 +  - Fixed soundness bug with low-level number functions such as
   1.711 +    "Abs_Integ" and "Rep_Integ".
   1.712    - Removed "std" option.
   1.713    - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
   1.714      "hide_types".
   1.715  
   1.716  * HOL-Multivariate_Analysis:
   1.717 -  - type class ordered_real_vector for ordered vector spaces
   1.718 -  - new theory Complex_Basic_Analysis defining complex derivatives,
   1.719 +  - Type class ordered_real_vector for ordered vector spaces.
   1.720 +  - New theory Complex_Basic_Analysis defining complex derivatives,
   1.721      holomorphic functions, etc., ported from HOL Light's canal.ml.
   1.722 -  - changed order of ordered_euclidean_space to be compatible with
   1.723 +  - Changed order of ordered_euclidean_space to be compatible with
   1.724      pointwise ordering on products. Therefore instance of
   1.725      conditionally_complete_lattice and ordered_real_vector.
   1.726      INCOMPATIBILITY: use box instead of greaterThanLessThan or
   1.727 -    explicit set-comprehensions with eucl_less for other (half-) open
   1.728 +    explicit set-comprehensions with eucl_less for other (half-)open
   1.729      intervals.
   1.730 -
   1.731    - renamed theorems:
   1.732      derivative_linear         ~>  has_derivative_bounded_linear
   1.733      derivative_is_linear      ~>  has_derivative_linear
   1.734      bounded_linear_imp_linear ~>  bounded_linear.linear
   1.735  
   1.736  * HOL-Probability:
   1.737 -  - replaced the Lebesgue integral on real numbers by the more general Bochner
   1.738 -    integral for functions into a real-normed vector space.
   1.739 +  - replaced the Lebesgue integral on real numbers by the more general
   1.740 +    Bochner integral for functions into a real-normed vector space.
   1.741  
   1.742      integral_zero               ~>  integral_zero / integrable_zero
   1.743      integral_minus              ~>  integral_minus / integrable_minus
   1.744 @@ -793,15 +825,17 @@
   1.745  
   1.746    - Renamed positive_integral to nn_integral:
   1.747  
   1.748 -    * Renamed all lemmas "*positive_integral*" to *nn_integral*"
   1.749 +    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
   1.750        positive_integral_positive ~> nn_integral_nonneg
   1.751  
   1.752 -    * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   1.753 -
   1.754 -  - Formalized properties about exponentially, Erlang, and normal distributed
   1.755 -    random variables.
   1.756 -
   1.757 -* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it.
   1.758 +    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   1.759 +
   1.760 +  - Formalized properties about exponentially, Erlang, and normal
   1.761 +    distributed random variables.
   1.762 +
   1.763 +* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by
   1.764 +session Kleene_Algebra in AFP.
   1.765 +
   1.766  
   1.767  *** Scala ***
   1.768  
   1.769 @@ -811,6 +845,9 @@
   1.770  specific and may override results accumulated so far.  The elements
   1.771  guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
   1.772  
   1.773 +* Substantial reworking of internal PIDE protocol communication
   1.774 +channels.  INCOMPATIBILITY.
   1.775 +
   1.776  
   1.777  *** ML ***
   1.778  
   1.779 @@ -818,8 +855,8 @@
   1.780  structure Runtime.  Minor INCOMPATIBILITY.
   1.781  
   1.782  * Discontinued old Toplevel.debug in favour of system option
   1.783 -"ML_exception_trace", which may be also declared within the context via
   1.784 -"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   1.785 +"ML_exception_trace", which may be also declared within the context
   1.786 +via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   1.787  
   1.788  * Renamed configuration option "ML_trace" to "ML_source_trace". Minor
   1.789  INCOMPATIBILITY.
   1.790 @@ -878,21 +915,6 @@
   1.791  the "system" manual for general explanations about add-on components,
   1.792  notably those that are not bundled with the normal release.
   1.793  
   1.794 -* Session ROOT specifications require explicit 'document_files' for
   1.795 -robust dependencies on LaTeX sources.  Only these explicitly given
   1.796 -files are copied to the document output directory, before document
   1.797 -processing is started.
   1.798 -
   1.799 -* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
   1.800 -and PDF_VIEWER now refer to the actual programs, not shell
   1.801 -command-lines.  Discontinued option -c: invocation may be asynchronous
   1.802 -via desktop environment, without any special precautions.  Potential
   1.803 -INCOMPATIBILITY with ambitious private settings.
   1.804 -
   1.805 -* Improved 'display_drafts' concerning desktop integration and
   1.806 -repeated invocation in PIDE front-end: re-use single file
   1.807 -$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   1.808 -
   1.809  * The raw Isabelle process executable has been renamed from
   1.810  "isabelle-process" to "isabelle_process", which conforms to common
   1.811  shell naming conventions, and allows to define a shell function within
   1.812 @@ -904,16 +926,31 @@
   1.813  with implicit build like "isabelle jedit", and without the mostly
   1.814  obsolete Isar TTY loop.
   1.815  
   1.816 +* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
   1.817 +and PDF_VIEWER now refer to the actual programs, not shell
   1.818 +command-lines.  Discontinued option -c: invocation may be asynchronous
   1.819 +via desktop environment, without any special precautions.  Potential
   1.820 +INCOMPATIBILITY with ambitious private settings.
   1.821 +
   1.822  * Removed obsolete "isabelle unsymbolize".  Note that the usual format
   1.823  for email communication is the Unicode rendering of Isabelle symbols,
   1.824  as produced by Isabelle/jEdit, for example.
   1.825  
   1.826 -* Retired the now unused Isabelle tool "wwwfind". Similar
   1.827 -functionality may be integrated into PIDE/jEdit at a later point.
   1.828 +* Removed obsolete tool "wwwfind". Similar functionality may be
   1.829 +integrated into Isabelle/jEdit eventually.
   1.830 +
   1.831 +* Improved 'display_drafts' concerning desktop integration and
   1.832 +repeated invocation in PIDE front-end: re-use single file
   1.833 +$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   1.834  
   1.835  * Windows: support for regular TeX installation (e.g. MiKTeX) instead
   1.836  of TeX Live from Cygwin.
   1.837  
   1.838 +* Session ROOT specifications require explicit 'document_files' for
   1.839 +robust dependencies on LaTeX sources.  Only these explicitly given
   1.840 +files are copied to the document output directory, before document
   1.841 +processing is started.
   1.842 +
   1.843  
   1.844  
   1.845  New in Isabelle2013-2 (December 2013)