misc updates for release;
authorwenzelm
Tue Jul 01 14:52:08 2014 +0200 (2014-07-01)
changeset 57452ecad2a53755a
parent 57451 3b10acac1d5e
child 57453 77d13a98f1c8
misc updates for release;
ANNOUNCE
CONTRIBUTORS
NEWS
README
     1.1 --- a/ANNOUNCE	Tue Jul 01 14:05:05 2014 +0200
     1.2 +++ b/ANNOUNCE	Tue Jul 01 14:52:08 2014 +0200
     1.3 @@ -1,27 +1,36 @@
     1.4 -Subject: Announcing Isabelle2013-2
     1.5 +Subject: Announcing Isabelle2014
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2013-2 is now available.
     1.9 +Isabelle2014 is now available.
    1.10 +
    1.11 +This version significantly improves upon Isabelle2013-2, see the NEWS
    1.12 +file in the distribution for more details.  Some highlights are:
    1.13  
    1.14 -This version supersedes Isabelle2013-1, which in turn consolidated
    1.15 -Isabelle2013 and introduced numerous improvements.  See the NEWS file
    1.16 -in the distribution for more details.  Some highlights are:
    1.17 +* Improved Isabelle/jEdit Prover IDE: navigation, completion,
    1.18 +  spell-checking, Query panel, Simplifier Trace panel.
    1.19  
    1.20 -* Significantly improved Isabelle/jEdit Prover IDE.
    1.21 +* Support for auxiliary files within the Prover IDE.
    1.22  
    1.23 -* Consolidated multi-platform support: Linux, Windows, Mac OS X.
    1.24 +* Support for official Standard ML within the Prover IDE,
    1.25 +  independently of Isabelle theory and proof development.
    1.26  
    1.27 -* Added and updated manuals: datatypes, implementation, isar-ref, jedit.
    1.28 +* HOL: BNF datatypes and codatatypes within theory Main, with numerous
    1.29 +  add-on tools.
    1.30  
    1.31 -* New Spec_Check tool: Quickcheck for Isabelle/ML.
    1.32 +* HOL tool enhancements: Nitpick, Sledgehammer.
    1.33 +
    1.34 +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis,
    1.35 +  HOL-Probability.
    1.36  
    1.37 -* HOL library enhancements: Complex_Main, HOL-Library,
    1.38 -  HOL-Multivariate_Analysis.
    1.39 +* HOL: internal SAT solver "cdclite" with models and proof traces.
    1.40 +
    1.41 +* HOL: updated SMT module, with support for SMT-LIB 2 and recent
    1.42 +  versions of Z3, as well as CVC3, CVC4.
    1.43  
    1.44 -* HOL tool enhancements: Codegenerator, Function, Lifting, Transfer,
    1.45 -  Nitpick, Sledgehammer.
    1.46 +* Updated and extended manuals: codegen, datatypes, implementation,
    1.47 +  isar-ref, jedit, system.
    1.48  
    1.49 -* HOL-BNF: significantly improved BNF-based (co)datatype package.
    1.50 +* System integration: improved support of LateX on Windows platform.
    1.51  
    1.52  
    1.53  You may get Isabelle2013-2 from the following mirror sites:
     2.1 --- a/CONTRIBUTORS	Tue Jul 01 14:05:05 2014 +0200
     2.2 +++ b/CONTRIBUTORS	Tue Jul 01 14:52:08 2014 +0200
     2.3 @@ -3,40 +3,48 @@
     2.4  who is listed as an author in one of the source files of this Isabelle
     2.5  distribution.
     2.6  
     2.7 -Contributions to this Isabelle version
     2.8 ---------------------------------------
     2.9 +Contributions to Isabelle2014
    2.10 +-----------------------------
    2.11  
    2.12  * June 2014: Florian Haftmann, TUM
    2.13 -  Consolidation and generalization of facts concerning products (resp. sums)
    2.14 -  on finite sets.
    2.15 +  Consolidation and generalization of facts concerning products
    2.16 +  (resp. sums) on finite sets.
    2.17  
    2.18  * June 2014: Florian Haftmann, TUM
    2.19    Internal reorganisation of the local theory / named target stack.
    2.20  
    2.21  * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM
    2.22 -  Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT,
    2.23 -  Waldmeister, etc.).
    2.24 +  Work on exotic automatic theorem provers for Sledgehammer (LEO-II,
    2.25 +  veriT, Waldmeister, etc.).
    2.26  
    2.27  * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM
    2.28 -  Various properties of exponentially, Erlang, and normal distributed random variables.
    2.29 +  Various properties of exponentially, Erlang, and normal distributed
    2.30 +  random variables.
    2.31  
    2.32 -* May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
    2.33 +* May 2014: Cezary Kaliszyk, University of Innsbruck, and
    2.34 +  Jasmin Blanchette, TUM
    2.35    SML-based engines for MaSh.
    2.36  
    2.37  * March 2014: René Thiemann
    2.38    Improved code generation for multisets.
    2.39  
    2.40  * February 2014: Florian Haftmann, TUM
    2.41 -  Permanent interpretation inside theory, locale and class targets with mixin definitions.
    2.42 +  Permanent interpretation inside theory, locale and class targets
    2.43 +  with mixin definitions.
    2.44 +
    2.45 +* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI
    2.46 +  Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE.
    2.47  
    2.48 -* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel,
    2.49 -  and Jasmin Blanchette, TUM
    2.50 -  Various improvements to the BNF-based (co)datatype package, including
    2.51 -  a more polished "primcorec" command, optimizations, and integration in
    2.52 -  the "HOL" session.
    2.53 +* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny,
    2.54 +  Dmitriy Traytel, and Jasmin Blanchette, TUM
    2.55 +  Various improvements to the BNF-based (co)datatype package,
    2.56 +  including a more polished "primcorec" command, optimizations, and
    2.57 +  integration in the "HOL" session.
    2.58  
    2.59 -* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM
    2.60 -  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3.
    2.61 +* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and
    2.62 +  Jasmin Blanchette, TUM
    2.63 +  "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and
    2.64 +  Z3 4.3.
    2.65  
    2.66  * January 2014: Lars Hupel, TUM
    2.67    An improved, interactive simplifier trace with integration into the
     3.1 --- a/NEWS	Tue Jul 01 14:05:05 2014 +0200
     3.2 +++ b/NEWS	Tue Jul 01 14:52:08 2014 +0200
     3.3 @@ -1,32 +1,19 @@
     3.4  Isabelle NEWS -- history user-relevant changes
     3.5  ==============================================
     3.6  
     3.7 -New in this Isabelle version
     3.8 -----------------------------
     3.9 +New in Isabelle2014 (August 2014)
    3.10 +---------------------------------
    3.11  
    3.12  *** General ***
    3.13  
    3.14 -* Document antiquotation @{url} produces markup for the given URL,
    3.15 -which results in an active hyperlink within the text.
    3.16 -
    3.17 -* Document antiquotation @{file_unchecked} is like @{file}, but does
    3.18 -not check existence within the file-system.
    3.19 -
    3.20 -* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML
    3.21 -workaround in Isabelle2013-1.  The prover process no longer accepts
    3.22 -old identifier syntax with \<^isub> or \<^isup>.
    3.23 -
    3.24 -* Syntax of document antiquotation @{rail} now uses \<newline> instead
    3.25 -of "\\", to avoid the optical illusion of escaped backslash within
    3.26 -string token.  Minor INCOMPATIBILITY.
    3.27 -
    3.28 -* Lexical syntax (inner and outer) supports text cartouches with
    3.29 -arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    3.30 -supports input via ` (backquote).
    3.31 -
    3.32 -* The outer syntax categories "text" (for formal comments and document
    3.33 -markup commands) and "altstring" (for literal fact references) allow
    3.34 -cartouches as well, in addition to the traditional mix of quotations.
    3.35 +* Support for official Standard ML within the Isabelle context.
    3.36 +Command 'SML_file' reads and evaluates the given Standard ML file.
    3.37 +Toplevel bindings are stored within the theory context; the initial
    3.38 +environment is restricted to the Standard ML implementation of
    3.39 +Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    3.40 +and 'SML_export' allow to exchange toplevel bindings between the two
    3.41 +separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    3.42 +some examples.
    3.43  
    3.44  * More static checking of proof methods, which allows the system to
    3.45  form a closure over the concrete syntax.  Method arguments should be
    3.46 @@ -37,25 +24,48 @@
    3.47  exception.  Potential INCOMPATIBILITY for non-conformant tactical
    3.48  proof tools.
    3.49  
    3.50 -* Support for official Standard ML within the Isabelle context.
    3.51 -Command 'SML_file' reads and evaluates the given Standard ML file.
    3.52 -Toplevel bindings are stored within the theory context; the initial
    3.53 -environment is restricted to the Standard ML implementation of
    3.54 -Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
    3.55 -and 'SML_export' allow to exchange toplevel bindings between the two
    3.56 -separate environments.  See also ~~/src/Tools/SML/Examples.thy for
    3.57 -some examples.
    3.58 -
    3.59 -* Updated and extended manuals: "codegen", "datatypes",
    3.60 -"implementation", "jedit", "system".
    3.61 +* Lexical syntax (inner and outer) supports text cartouches with
    3.62 +arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    3.63 +supports input via ` (backquote).
    3.64 +
    3.65 +* The outer syntax categories "text" (for formal comments and document
    3.66 +markup commands) and "altstring" (for literal fact references) allow
    3.67 +cartouches as well, in addition to the traditional mix of quotations.
    3.68 +
    3.69 +* Syntax of document antiquotation @{rail} now uses \<newline> instead
    3.70 +of "\\", to avoid the optical illusion of escaped backslash within
    3.71 +string token.  General renovation of its syntax using text cartouces.
    3.72 +Minor INCOMPATIBILITY.
    3.73 +
    3.74 +* Discontinued legacy_isub_isup, which was a temporary workaround for
    3.75 +Isabelle/ML in Isabelle2013-1.  The prover process no longer accepts
    3.76 +old identifier syntax with \<^isub> or \<^isup>.  Potential
    3.77 +INCOMPATIBILITY.
    3.78 +
    3.79 +* Document antiquotation @{url} produces markup for the given URL,
    3.80 +which results in an active hyperlink within the text.
    3.81 +
    3.82 +* Document antiquotation @{file_unchecked} is like @{file}, but does
    3.83 +not check existence within the file-system.
    3.84 +
    3.85 +* Updated and extended manuals: codegen, datatypes, implementation,
    3.86 +isar-ref, jedit, system.
    3.87  
    3.88  
    3.89  *** Prover IDE -- Isabelle/Scala/jEdit ***
    3.90  
    3.91 -* Document panel: simplied interaction where every single mouse click
    3.92 -(re)opens document via desktop environment or as jEdit buffer.
    3.93 -
    3.94 -* Support for Navigator plugin (with toolbar buttons).
    3.95 +* Improved Document panel: simplied interaction where every single
    3.96 +mouse click (re)opens document via desktop environment or as jEdit
    3.97 +buffer.
    3.98 +
    3.99 +* Support for Navigator plugin (with toolbar buttons), with connection
   3.100 +to PIDE hyperlinks.
   3.101 +
   3.102 +* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
   3.103 +Open text buffers take precedence over copies within the file-system.
   3.104 +
   3.105 +* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
   3.106 +auxiliary ML files.
   3.107  
   3.108  * Improved syntactic and semantic completion mechanism, with simple
   3.109  templates, completion language context, name-space completion,
   3.110 @@ -72,12 +82,6 @@
   3.111  * Integrated spell-checker for document text, comments etc. with
   3.112  completion popup and context-menu.
   3.113  
   3.114 -* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
   3.115 -Open text buffers take precedence over copies within the file-system.
   3.116 -
   3.117 -* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
   3.118 -auxiliary ML files.
   3.119 -
   3.120  * More general "Query" panel supersedes "Find" panel, with GUI access
   3.121  to commands 'find_theorems' and 'find_consts', as well as print
   3.122  operations for the context.  Minor incompatibility in keyboard
   3.123 @@ -91,10 +95,6 @@
   3.124  process, without requiring old-fashioned command-line invocation of
   3.125  "isabelle jedit -m MODE".
   3.126  
   3.127 -* New Simplifier Trace panel provides an interactive view of the
   3.128 -simplification process, enabled by the "simplifier_trace" attribute
   3.129 -within the context.
   3.130 -
   3.131  * More support for remote files (e.g. http) using standard Java
   3.132  networking operations instead of jEdit virtual file-systems.
   3.133  
   3.134 @@ -105,6 +105,11 @@
   3.135  and window placement wrt. main editor view; optional menu item to
   3.136  "Detach" a copy where this makes sense.
   3.137  
   3.138 +* New Simplifier Trace panel provides an interactive view of the
   3.139 +simplification process, enabled by the "simplifier_trace" attribute
   3.140 +within the context.
   3.141 +
   3.142 +
   3.143  
   3.144  *** Pure ***
   3.145  
   3.146 @@ -139,12 +144,12 @@
   3.147  * Low-level type-class commands 'classes', 'classrel', 'arities' have
   3.148  been discontinued to avoid the danger of non-trivial axiomatization
   3.149  that is not immediately visible.  INCOMPATIBILITY, use regular
   3.150 -'instance' with proof.  The required OFCLASS(...) theorem might be
   3.151 -postulated via 'axiomatization' beforehand, or the proof finished
   3.152 -trivially if the underlying class definition is made vacuous (without
   3.153 -any assumptions).  See also Isabelle/ML operations
   3.154 -Axclass.axiomatize_class, Axclass.axiomatize_classrel,
   3.155 -Axclass.axiomatize_arity.
   3.156 +'instance' command with proof.  The required OFCLASS(...) theorem
   3.157 +might be postulated via 'axiomatization' beforehand, or the proof
   3.158 +finished trivially if the underlying class definition is made vacuous
   3.159 +(without any assumptions).  See also Isabelle/ML operations
   3.160 +Axclass.class_axiomatization, Axclass.classrel_axiomatization,
   3.161 +Axclass.arity_axiomatization.
   3.162  
   3.163  * Attributes "where" and "of" allow an optional context of local
   3.164  variables ('for' declaration): these variables become schematic in the
   3.165 @@ -167,10 +172,10 @@
   3.166  
   3.167  * Inner syntax token language allows regular quoted strings "..."
   3.168  (only makes sense in practice, if outer syntax is delimited
   3.169 -differently).
   3.170 -
   3.171 -* Code generator preprocessor: explicit control of simp tracing
   3.172 -on a per-constant basis.  See attribute "code_preproc".
   3.173 +differently, e.g. via cartouches).
   3.174 +
   3.175 +* Code generator preprocessor: explicit control of simp tracing on a
   3.176 +per-constant basis.  See attribute "code_preproc".
   3.177  
   3.178  * Command 'print_term_bindings' supersedes 'print_binds' for clarity,
   3.179  but the latter is retained some time as Proof General legacy.
   3.180 @@ -180,63 +185,68 @@
   3.181  
   3.182  * Qualified String.implode and String.explode.  INCOMPATIBILITY.
   3.183  
   3.184 -* Command and antiquotation ''value'' are hardcoded against nbe and
   3.185 -ML now.  Minor INCOMPATIBILITY.
   3.186 -
   3.187 -* Separate command ''approximate'' for approximative computation
   3.188 -in Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   3.189 +* Command and antiquotation "value" are now hardcoded against nbe and
   3.190 +ML.  Minor INCOMPATIBILITY.
   3.191 +
   3.192 +* Separate command "approximate" for approximative computation in
   3.193 +src/HOL/Decision_Procs/Approximation.  Minor INCOMPATIBILITY.
   3.194  
   3.195  * Adjustion of INF and SUP operations:
   3.196 -  * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   3.197 -  * Consolidated theorem names containing INFI and SUPR: have INF
   3.198 -  and SUP instead uniformly.
   3.199 -  * More aggressive normalization of expressions involving INF and Inf
   3.200 -  or SUP and Sup.
   3.201 -  * INF_image and SUP_image do not unfold composition.
   3.202 -  * Dropped facts INF_comp, SUP_comp.
   3.203 -  * Default congruence rules strong_INF_cong and strong_SUP_cong,
   3.204 -  with simplifier implication in premises.  Generalize and replace
   3.205 -  former INT_cong, SUP_cong
   3.206 +  - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
   3.207 +  - Consolidated theorem names containing INFI and SUPR: have INF and
   3.208 +    SUP instead uniformly.
   3.209 +  - More aggressive normalization of expressions involving INF and Inf
   3.210 +    or SUP and Sup.
   3.211 +  - INF_image and SUP_image do not unfold composition.
   3.212 +  - Dropped facts INF_comp, SUP_comp.
   3.213 +  - Default congruence rules strong_INF_cong and strong_SUP_cong, with
   3.214 +    simplifier implication in premises.  Generalize and replace former
   3.215 +    INT_cong, SUP_cong
   3.216 +
   3.217  INCOMPATIBILITY.
   3.218  
   3.219  * Swapped orientation of facts image_comp and vimage_comp:
   3.220 +
   3.221    image_compose ~> image_comp [symmetric]
   3.222    image_comp ~> image_comp [symmetric]
   3.223    vimage_compose ~> vimage_comp [symmetric]
   3.224    vimage_comp ~> vimage_comp [symmetric]
   3.225 -  INCOMPATIBILITY.
   3.226 -
   3.227 -* Simplifier: Enhanced solver of preconditions of rewrite rules
   3.228 -  can now deal with conjunctions.
   3.229 -  For help with converting proofs, the old behaviour of the simplifier
   3.230 -  can be restored like this:  declare/using [[simp_legacy_precond]]
   3.231 -  This configuration option will disappear again in the future.
   3.232 +
   3.233 +INCOMPATIBILITY.
   3.234 +
   3.235 +* Simplifier: Enhanced solver of preconditions of rewrite rules can
   3.236 +now deal with conjunctions.  For help with converting proofs, the old
   3.237 +behaviour of the simplifier can be restored like this: declare/using
   3.238 +[[simp_legacy_precond]].  This configuration option will disappear
   3.239 +again in the future.  INCOMPATIBILITY.
   3.240  
   3.241  * HOL-Word:
   3.242 -  * Abandoned fact collection "word_arith_alts", which is a
   3.243 -  duplicate of "word_arith_wis".
   3.244 -  * Dropped first (duplicated) element in fact collections
   3.245 -  "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   3.246 -  "uint_word_arith_bintrs".
   3.247 -
   3.248 -* Code generator: enforce case of identifiers only for strict
   3.249 -target language requirements.  INCOMPATIBILITY.
   3.250 +  - Abandoned fact collection "word_arith_alts", which is a duplicate
   3.251 +    of "word_arith_wis".
   3.252 +  - Dropped first (duplicated) element in fact collections
   3.253 +    "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
   3.254 +    "uint_word_arith_bintrs".
   3.255 +
   3.256 +* Code generator: enforce case of identifiers only for strict target
   3.257 +language requirements.  INCOMPATIBILITY.
   3.258  
   3.259  * Code generator: explicit proof contexts in many ML interfaces.
   3.260  INCOMPATIBILITY.
   3.261  
   3.262 -* Code generator: minimize exported identifiers by default.
   3.263 -Minor INCOMPATIBILITY.
   3.264 -
   3.265 -* Code generation for SML and OCaml: dropped arcane "no_signatures" option.
   3.266 -Minor INCOMPATIBILITY.
   3.267 +* Code generator: minimize exported identifiers by default.  Minor
   3.268 +INCOMPATIBILITY.
   3.269 +
   3.270 +* Code generation for SML and OCaml: dropped arcane "no_signatures"
   3.271 +option.  Minor INCOMPATIBILITY.
   3.272  
   3.273  * Simproc "finite_Collect" is no longer enabled by default, due to
   3.274  spurious crashes and other surprises.  Potential INCOMPATIBILITY.
   3.275  
   3.276 -* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   3.277 -  The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
   3.278 -  "primcorec", and "primcorecursive" commands are now part of "Main".
   3.279 +* Moved new (co)datatype package and its dependencies from session
   3.280 +  "HOL-BNF" to "HOL".  The commands 'bnf', 'wrap_free_constructors',
   3.281 +  'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
   3.282 +  part of theory "Main".
   3.283 +
   3.284    Theory renamings:
   3.285      FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
   3.286      Library/Wfrec.thy ~> Wfrec.thy
   3.287 @@ -260,58 +270,63 @@
   3.288      BNF/More_BNFs.thy ~> Library/More_BNFs.thy
   3.289      BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
   3.290      BNF/Examples/* ~> BNF_Examples/*
   3.291 +
   3.292    New theories:
   3.293      Wellorder_Extension.thy (split from Zorn.thy)
   3.294      Library/Cardinal_Notations.thy
   3.295      Library/BNF_Axomatization.thy
   3.296      BNF_Examples/Misc_Primcorec.thy
   3.297      BNF_Examples/Stream_Processor.thy
   3.298 +
   3.299    Discontinued theories:
   3.300      BNF/BNF.thy
   3.301      BNF/Equiv_Relations_More.thy
   3.302 -  INCOMPATIBILITY.
   3.303 +
   3.304 +INCOMPATIBILITY.
   3.305  
   3.306  * New (co)datatype package:
   3.307 -  * "primcorec" is fully implemented.
   3.308 -  * "datatype_new" generates size functions ("size_xxx" and "size") as
   3.309 -    required by "fun".
   3.310 -  * BNFs are integrated with the Lifting tool and new-style (co)datatypes
   3.311 -    with Transfer.
   3.312 -  * Renamed commands:
   3.313 +  - Command 'primcorec' is fully implemented.
   3.314 +  - Command 'datatype_new' generates size functions ("size_xxx" and
   3.315 +    "size") as required by 'fun'.
   3.316 +  - BNFs are integrated with the Lifting tool and new-style
   3.317 +    (co)datatypes with Transfer.
   3.318 +  - Renamed commands:
   3.319        datatype_new_compat ~> datatype_compat
   3.320        primrec_new ~> primrec
   3.321        wrap_free_constructors ~> free_constructors
   3.322      INCOMPATIBILITY.
   3.323 -  * The generated constants "xxx_case" and "xxx_rec" have been renamed
   3.324 +  - The generated constants "xxx_case" and "xxx_rec" have been renamed
   3.325      "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
   3.326      INCOMPATIBILITY.
   3.327 -  * The constant "xxx_(un)fold" and related theorems are no longer generated.
   3.328 -    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
   3.329 +  - The constant "xxx_(un)fold" and related theorems are no longer
   3.330 +    generated.  Use "xxx_(co)rec" or define "xxx_(un)fold" manually
   3.331 +    using "prim(co)rec".
   3.332      INCOMPATIBILITY.
   3.333 -  * No discriminators are generated for nullary constructors by default,
   3.334 -    eliminating the need for the odd "=:" syntax.
   3.335 +  - No discriminators are generated for nullary constructors by
   3.336 +    default, eliminating the need for the odd "=:" syntax.
   3.337      INCOMPATIBILITY.
   3.338 -  * No discriminators or selectors are generated by default by
   3.339 +  - No discriminators or selectors are generated by default by
   3.340      "datatype_new", unless custom names are specified or the new
   3.341      "discs_sels" option is passed.
   3.342      INCOMPATIBILITY.
   3.343  
   3.344  * Old datatype package:
   3.345 -  * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
   3.346 -    "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
   3.347 -    INCOMPATIBILITY.
   3.348 -  * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been
   3.349 -    renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~>
   3.350 -    "case_prod").
   3.351 -    INCOMPATIBILITY.
   3.352 -
   3.353 -* The types "'a list" and "'a option", their set and map functions, their
   3.354 -  relators, and their selectors are now produced using the new BNF-based
   3.355 -  datatype package.
   3.356 +  - The generated theorems "xxx.cases" and "xxx.recs" have been
   3.357 +    renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
   3.358 +    "sum.case").  INCOMPATIBILITY.
   3.359 +  - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
   3.360 +    been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
   3.361 +    "prod_case" ~> "case_prod").  INCOMPATIBILITY.
   3.362 +
   3.363 +* The types "'a list" and "'a option", their set and map functions,
   3.364 +  their relators, and their selectors are now produced using the new
   3.365 +  BNF-based datatype package.
   3.366 +
   3.367    Renamed constants:
   3.368      Option.set ~> set_option
   3.369      Option.map ~> map_option
   3.370      option_rel ~> rel_option
   3.371 +
   3.372    Renamed theorems:
   3.373      set_def ~> set_rec[abs_def]
   3.374      map_def ~> map_rec[abs_def]
   3.375 @@ -323,7 +338,8 @@
   3.376      hd.simps ~> list.sel(1)
   3.377      tl.simps ~> list.sel(2-3)
   3.378      the.simps ~> option.sel
   3.379 -  INCOMPATIBILITY.
   3.380 +
   3.381 +INCOMPATIBILITY.
   3.382  
   3.383  * The following map functions and relators have been renamed:
   3.384      sum_map ~> map_sum
   3.385 @@ -333,16 +349,18 @@
   3.386      fun_rel ~> rel_fun
   3.387      set_rel ~> rel_set
   3.388      filter_rel ~> rel_filter
   3.389 -    fset_rel ~> rel_fset (in "Library/FSet.thy")
   3.390 -    cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy")
   3.391 -    vset ~> rel_vset (in "Library/Quotient_Set.thy")
   3.392 -
   3.393 -* New theories:
   3.394 -    Cardinals/Ordinal_Arithmetic.thy
   3.395 -    Library/Tree
   3.396 -
   3.397 -* Theory reorganizations:
   3.398 -  * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   3.399 +    fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
   3.400 +    cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
   3.401 +    vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
   3.402 +
   3.403 +INCOMPATIBILITY.
   3.404 +
   3.405 +* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.
   3.406 +
   3.407 +* New theory src/HOL/Library/Tree.thy.
   3.408 +
   3.409 +* Theory reorganization:
   3.410 +  Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy
   3.411  
   3.412  * Consolidated some facts about big group operators:
   3.413  
   3.414 @@ -411,41 +429,41 @@
   3.415    Dropped setsum_reindex_id, setprod_reindex_id
   3.416      (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]).
   3.417  
   3.418 -  INCOMPATIBILITY.
   3.419 -
   3.420 -* New internal SAT solver "cdclite" that produces models and proof traces.
   3.421 -  This solver replaces the internal SAT solvers "enumerate" and "dpll".
   3.422 -  Applications that explicitly used one of these two SAT solvers should
   3.423 -  use "cdclite" instead. In addition, "cdclite" is now the default SAT
   3.424 -  solver for the "sat" and "satx" proof methods and corresponding tactics;
   3.425 -  the old default can be restored using
   3.426 -  "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
   3.427 -
   3.428 -* SMT module:
   3.429 -  * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2
   3.430 -    and supports recent versions of Z3 (e.g., 4.3). The new proof method is
   3.431 -    called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no
   3.432 -    longer supported, because no version of the solver can handle both
   3.433 -    SMT-LIB 2 and quantifiers.
   3.434 +INCOMPATIBILITY.
   3.435 +
   3.436 +* New internal SAT solver "cdclite" that produces models and proof
   3.437 +traces.  This solver replaces the internal SAT solvers "enumerate" and
   3.438 +"dpll".  Applications that explicitly used one of these two SAT
   3.439 +solvers should use "cdclite" instead. In addition, "cdclite" is now
   3.440 +the default SAT solver for the "sat" and "satx" proof methods and
   3.441 +corresponding tactics; the old default can be restored using "declare
   3.442 +[[sat_solver = zchaff_with_proofs]]".  Minor INCOMPATIBILITY.
   3.443 +
   3.444 +* SMT module: A new version of the SMT module, temporarily called
   3.445 +"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
   3.446 +4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
   3.447 +supported as oracles. Yices is no longer supported, because no version
   3.448 +of the solver can handle both SMT-LIB 2 and quantifiers.
   3.449  
   3.450  * Sledgehammer:
   3.451    - Z3 can now produce Isar proofs.
   3.452    - MaSh overhaul:
   3.453 -      - New SML-based learning engines eliminate the dependency on Python
   3.454 -        and increase performance and reliability.
   3.455 -      - MaSh and MeSh are now used by default together with the traditional
   3.456 -        MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh"
   3.457 -        system option in Plugin Options / Isabelle / General to "none".
   3.458 +    . New SML-based learning engines eliminate the dependency on
   3.459 +      Python and increase performance and reliability.
   3.460 +    . MaSh and MeSh are now used by default together with the
   3.461 +      traditional MePo (Meng-Paulson) relevance filter. To disable
   3.462 +      MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
   3.463 +      Options / Isabelle / General to "none".
   3.464    - New option:
   3.465        smt_proofs
   3.466    - Renamed options:
   3.467        isar_compress ~> compress
   3.468        isar_try0 ~> try0
   3.469 -    INCOMPATIBILITY.
   3.470 -
   3.471 -* Metis:
   3.472 -  - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead.
   3.473 -    INCOMPATIBILITY.
   3.474 +
   3.475 +INCOMPATIBILITY.
   3.476 +
   3.477 +* Metis: Removed legacy proof method 'metisFT'. Use 'metis
   3.478 +(full_types)' instead. INCOMPATIBILITY.
   3.479  
   3.480  * Try0: Added 'algebra' and 'meson' to the set of proof methods.
   3.481  
   3.482 @@ -467,7 +485,7 @@
   3.483  
   3.484  * Abolished slightly odd global lattice interpretation for min/max.
   3.485  
   3.486 -Fact consolidations:
   3.487 +  Fact consolidations:
   3.488      min_max.inf_assoc ~> min.assoc
   3.489      min_max.inf_commute ~> min.commute
   3.490      min_max.inf_left_commute ~> min.left_commute
   3.491 @@ -513,18 +531,18 @@
   3.492  min.left_commute, min.left_idem, max.commute, max.assoc,
   3.493  max.left_commute, max.left_idem directly.
   3.494  
   3.495 -For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2,
   3.496 -max.cobounded1m max.cobounded2 directly.
   3.497 +For min_max.inf_sup_ord, prefer (one of) min.cobounded1,
   3.498 +min.cobounded2, max.cobounded1m max.cobounded2 directly.
   3.499  
   3.500  For min_ac or max_ac, prefer more general collection ac_simps.
   3.501  
   3.502  INCOMPATBILITY.
   3.503  
   3.504 -* Word library: bit representations prefer type bool over type bit.
   3.505 -INCOMPATIBILITY.
   3.506 -
   3.507 -* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin.
   3.508 -INCOMPATIBILITY.
   3.509 +* HOL-Word: bit representations prefer type bool over type bit.
   3.510 +INCOMPATIBILITY.
   3.511 +
   3.512 +* Theorem disambiguation Inf_le_Sup (on finite sets) ~>
   3.513 +Inf_fin_le_Sup_fin.  INCOMPATIBILITY.
   3.514  
   3.515  * Code generations are provided for make, fields, extend and truncate
   3.516  operations on records.
   3.517 @@ -534,21 +552,25 @@
   3.518  
   3.519  * Fact generalization and consolidation:
   3.520      neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
   3.521 -INCOMPATIBILITY.
   3.522 -
   3.523 -* Purely algebraic definition of even.  Fact generalization and consolidation:
   3.524 +
   3.525 +INCOMPATIBILITY.
   3.526 +
   3.527 +* Purely algebraic definition of even.  Fact generalization and
   3.528 +  consolidation:
   3.529      nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd
   3.530      even_zero_(nat|int) ~> even_zero
   3.531 +
   3.532  INCOMPATIBILITY.
   3.533  
   3.534  * Abolished neg_numeral.
   3.535 -  * Canonical representation for minus one is "- 1".
   3.536 -  * Canonical representation for other negative numbers is "- (numeral _)".
   3.537 -  * When devising rule sets for number calculation, consider the
   3.538 +  - Canonical representation for minus one is "- 1".
   3.539 +  - Canonical representation for other negative numbers is "- (numeral _)".
   3.540 +  - When devising rule sets for number calculation, consider the
   3.541      following canonical cases: 0, 1, numeral _, - 1, - numeral _.
   3.542 -  * HOLogic.dest_number also recognizes numerals in non-canonical forms
   3.543 +  - HOLogic.dest_number also recognizes numerals in non-canonical forms
   3.544      like "numeral One", "- numeral One", "- 0" and even "- ... - _".
   3.545 -  * Syntax for negative numerals is mere input syntax.
   3.546 +  - Syntax for negative numerals is mere input syntax.
   3.547 +
   3.548  INCOMPATIBILITY.
   3.549  
   3.550  * Elimination of fact duplicates:
   3.551 @@ -556,6 +578,7 @@
   3.552      diff_eq_0_iff_eq ~> right_minus_eq
   3.553      nat_infinite ~> infinite_UNIV_nat
   3.554      int_infinite ~> infinite_UNIV_int
   3.555 +
   3.556  INCOMPATIBILITY.
   3.557  
   3.558  * Fact name consolidation:
   3.559 @@ -564,6 +587,7 @@
   3.560      le_minus_self_iff ~> less_eq_neg_nonpos
   3.561      neg_less_nonneg ~> neg_less_pos
   3.562      less_minus_self_iff ~> less_neg_neg [simp]
   3.563 +
   3.564  INCOMPATIBILITY.
   3.565  
   3.566  * More simplification rules on unary and binary minus:
   3.567 @@ -571,9 +595,9 @@
   3.568  add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2,
   3.569  add_minus_cancel, diff_add_cancel, le_add_same_cancel1,
   3.570  le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2,
   3.571 -minus_add_cancel, uminus_add_conv_diff.  These correspondingly
   3.572 -have been taken away from fact collections algebra_simps and
   3.573 -field_simps.  INCOMPATIBILITY.
   3.574 +minus_add_cancel, uminus_add_conv_diff.  These correspondingly have
   3.575 +been taken away from fact collections algebra_simps and field_simps.
   3.576 +INCOMPATIBILITY.
   3.577  
   3.578  To restore proofs, the following patterns are helpful:
   3.579  
   3.580 @@ -588,18 +612,18 @@
   3.581  or the brute way with
   3.582  "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
   3.583  
   3.584 -* SUP and INF generalized to conditionally_complete_lattice
   3.585 +* SUP and INF generalized to conditionally_complete_lattice.
   3.586  
   3.587  * Theory Lubs moved HOL image to HOL-Library. It is replaced by
   3.588 -Conditionally_Complete_Lattices.   INCOMPATIBILITY.
   3.589 -
   3.590 -* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them
   3.591 -instead of explicitly stating boundedness of sets.
   3.592 -
   3.593 -* ccpo.admissible quantifies only over non-empty chains to allow
   3.594 -more syntax-directed proof rules; the case of the empty chain
   3.595 -shows up as additional case in fixpoint induction proofs.
   3.596 -INCOMPATIBILITY
   3.597 +Conditionally_Complete_Lattices.  INCOMPATIBILITY.
   3.598 +
   3.599 +* Introduce bdd_above and bdd_below in theory
   3.600 +Conditionally_Complete_Lattices, use them instead of explicitly
   3.601 +stating boundedness of sets.
   3.602 +
   3.603 +* ccpo.admissible quantifies only over non-empty chains to allow more
   3.604 +syntax-directed proof rules; the case of the empty chain shows up as
   3.605 +additional case in fixpoint induction proofs.  INCOMPATIBILITY.
   3.606  
   3.607  * Removed and renamed theorems in Series:
   3.608    summable_le         ~>  suminf_le
   3.609 @@ -617,10 +641,13 @@
   3.610    removed series_zero, replaced by sums_finite
   3.611  
   3.612    removed auxiliary lemmas:
   3.613 +
   3.614      sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group,
   3.615 -    half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded,
   3.616 -    summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom,
   3.617 -    sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const
   3.618 +    half, le_Suc_ex_iff, lemma_realpow_diff_sumr,
   3.619 +    real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2,
   3.620 +    sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero,
   3.621 +    summable_convergent_sumr_iff, sumr_diff_mult_const
   3.622 +
   3.623  INCOMPATIBILITY.
   3.624  
   3.625  * Replace (F)DERIV syntax by has_derivative:
   3.626 @@ -632,10 +659,10 @@
   3.627  
   3.628    - removed constant isDiff
   3.629  
   3.630 -  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input
   3.631 -    syntax.
   3.632 -
   3.633 -  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed
   3.634 +  - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as
   3.635 +    input syntax.
   3.636 +
   3.637 +  - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed.
   3.638  
   3.639    - Renamed FDERIV_... lemmas to has_derivative_...
   3.640  
   3.641 @@ -643,8 +670,9 @@
   3.642  
   3.643    - removed DERIV_intros, has_derivative_eq_intros
   3.644  
   3.645 -  - introduced derivative_intros and deriative_eq_intros which includes now rules for
   3.646 -    DERIV, has_derivative and has_vector_derivative.
   3.647 +  - introduced derivative_intros and deriative_eq_intros which
   3.648 +    includes now rules for DERIV, has_derivative and
   3.649 +    has_vector_derivative.
   3.650  
   3.651    - Other renamings:
   3.652      differentiable_def        ~>  real_differentiable_def
   3.653 @@ -654,24 +682,27 @@
   3.654      isDiff_der                ~>  differentiable_def
   3.655      deriv_fderiv              ~>  has_field_derivative_def
   3.656      deriv_def                 ~>  DERIV_def
   3.657 -INCOMPATIBILITY.
   3.658 -
   3.659 -* Include more theorems in continuous_intros. Remove the continuous_on_intros,
   3.660 -  isCont_intros collections, these facts are now in continuous_intros.
   3.661 -
   3.662 -* Theorems about complex numbers are now stated only using Re and Im, the Complex
   3.663 -  constructor is not used anymore. It is possible to use primcorec to defined the
   3.664 -  behaviour of a complex-valued function.
   3.665 -
   3.666 -  Removed theorems about the Complex constructor from the simpset, they are
   3.667 -  available as the lemma collection legacy_Complex_simps. This especially
   3.668 -  removes
   3.669 +
   3.670 +INCOMPATIBILITY.
   3.671 +
   3.672 +* Include more theorems in continuous_intros. Remove the
   3.673 +continuous_on_intros, isCont_intros collections, these facts are now
   3.674 +in continuous_intros.
   3.675 +
   3.676 +* Theorems about complex numbers are now stated only using Re and Im,
   3.677 +the Complex constructor is not used anymore. It is possible to use
   3.678 +primcorec to defined the behaviour of a complex-valued function.
   3.679 +
   3.680 +Removed theorems about the Complex constructor from the simpset, they
   3.681 +are available as the lemma collection legacy_Complex_simps. This
   3.682 +especially removes
   3.683 +
   3.684      i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
   3.685  
   3.686 -  Instead the reverse direction is supported with
   3.687 +Instead the reverse direction is supported with
   3.688      Complex_eq: "Complex a b = a + \<i> * b"
   3.689  
   3.690 -  Moved csqrt from Fundamental_Algebra_Theorem to Complex.
   3.691 +Moved csqrt from Fundamental_Algebra_Theorem to Complex.
   3.692  
   3.693    Renamings:
   3.694      Re/Im                  ~>  complex.sel
   3.695 @@ -701,36 +732,37 @@
   3.696      complex_inverse_def
   3.697      complex_scaleR_def
   3.698  
   3.699 +INCOMPATIBILITY.
   3.700 +
   3.701  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
   3.702  
   3.703  * Nitpick:
   3.704 -  - Fixed soundness bug whereby mutually recursive datatypes could take
   3.705 -    infinite values.
   3.706 -  - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
   3.707 -    "Rep_Integ".
   3.708 +  - Fixed soundness bug whereby mutually recursive datatypes could
   3.709 +    take infinite values.
   3.710 +  - Fixed soundness bug with low-level number functions such as
   3.711 +    "Abs_Integ" and "Rep_Integ".
   3.712    - Removed "std" option.
   3.713    - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
   3.714      "hide_types".
   3.715  
   3.716  * HOL-Multivariate_Analysis:
   3.717 -  - type class ordered_real_vector for ordered vector spaces
   3.718 -  - new theory Complex_Basic_Analysis defining complex derivatives,
   3.719 +  - Type class ordered_real_vector for ordered vector spaces.
   3.720 +  - New theory Complex_Basic_Analysis defining complex derivatives,
   3.721      holomorphic functions, etc., ported from HOL Light's canal.ml.
   3.722 -  - changed order of ordered_euclidean_space to be compatible with
   3.723 +  - Changed order of ordered_euclidean_space to be compatible with
   3.724      pointwise ordering on products. Therefore instance of
   3.725      conditionally_complete_lattice and ordered_real_vector.
   3.726      INCOMPATIBILITY: use box instead of greaterThanLessThan or
   3.727 -    explicit set-comprehensions with eucl_less for other (half-) open
   3.728 +    explicit set-comprehensions with eucl_less for other (half-)open
   3.729      intervals.
   3.730 -
   3.731    - renamed theorems:
   3.732      derivative_linear         ~>  has_derivative_bounded_linear
   3.733      derivative_is_linear      ~>  has_derivative_linear
   3.734      bounded_linear_imp_linear ~>  bounded_linear.linear
   3.735  
   3.736  * HOL-Probability:
   3.737 -  - replaced the Lebesgue integral on real numbers by the more general Bochner
   3.738 -    integral for functions into a real-normed vector space.
   3.739 +  - replaced the Lebesgue integral on real numbers by the more general
   3.740 +    Bochner integral for functions into a real-normed vector space.
   3.741  
   3.742      integral_zero               ~>  integral_zero / integrable_zero
   3.743      integral_minus              ~>  integral_minus / integrable_minus
   3.744 @@ -793,15 +825,17 @@
   3.745  
   3.746    - Renamed positive_integral to nn_integral:
   3.747  
   3.748 -    * Renamed all lemmas "*positive_integral*" to *nn_integral*"
   3.749 +    . Renamed all lemmas "*positive_integral*" to *nn_integral*"
   3.750        positive_integral_positive ~> nn_integral_nonneg
   3.751  
   3.752 -    * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   3.753 -
   3.754 -  - Formalized properties about exponentially, Erlang, and normal distributed
   3.755 -    random variables.
   3.756 -
   3.757 -* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it.
   3.758 +    . Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
   3.759 +
   3.760 +  - Formalized properties about exponentially, Erlang, and normal
   3.761 +    distributed random variables.
   3.762 +
   3.763 +* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by
   3.764 +session Kleene_Algebra in AFP.
   3.765 +
   3.766  
   3.767  *** Scala ***
   3.768  
   3.769 @@ -811,6 +845,9 @@
   3.770  specific and may override results accumulated so far.  The elements
   3.771  guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
   3.772  
   3.773 +* Substantial reworking of internal PIDE protocol communication
   3.774 +channels.  INCOMPATIBILITY.
   3.775 +
   3.776  
   3.777  *** ML ***
   3.778  
   3.779 @@ -818,8 +855,8 @@
   3.780  structure Runtime.  Minor INCOMPATIBILITY.
   3.781  
   3.782  * Discontinued old Toplevel.debug in favour of system option
   3.783 -"ML_exception_trace", which may be also declared within the context via
   3.784 -"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   3.785 +"ML_exception_trace", which may be also declared within the context
   3.786 +via "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
   3.787  
   3.788  * Renamed configuration option "ML_trace" to "ML_source_trace". Minor
   3.789  INCOMPATIBILITY.
   3.790 @@ -878,21 +915,6 @@
   3.791  the "system" manual for general explanations about add-on components,
   3.792  notably those that are not bundled with the normal release.
   3.793  
   3.794 -* Session ROOT specifications require explicit 'document_files' for
   3.795 -robust dependencies on LaTeX sources.  Only these explicitly given
   3.796 -files are copied to the document output directory, before document
   3.797 -processing is started.
   3.798 -
   3.799 -* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
   3.800 -and PDF_VIEWER now refer to the actual programs, not shell
   3.801 -command-lines.  Discontinued option -c: invocation may be asynchronous
   3.802 -via desktop environment, without any special precautions.  Potential
   3.803 -INCOMPATIBILITY with ambitious private settings.
   3.804 -
   3.805 -* Improved 'display_drafts' concerning desktop integration and
   3.806 -repeated invocation in PIDE front-end: re-use single file
   3.807 -$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   3.808 -
   3.809  * The raw Isabelle process executable has been renamed from
   3.810  "isabelle-process" to "isabelle_process", which conforms to common
   3.811  shell naming conventions, and allows to define a shell function within
   3.812 @@ -904,16 +926,31 @@
   3.813  with implicit build like "isabelle jedit", and without the mostly
   3.814  obsolete Isar TTY loop.
   3.815  
   3.816 +* Simplified "isabelle display" tool.  Settings variables DVI_VIEWER
   3.817 +and PDF_VIEWER now refer to the actual programs, not shell
   3.818 +command-lines.  Discontinued option -c: invocation may be asynchronous
   3.819 +via desktop environment, without any special precautions.  Potential
   3.820 +INCOMPATIBILITY with ambitious private settings.
   3.821 +
   3.822  * Removed obsolete "isabelle unsymbolize".  Note that the usual format
   3.823  for email communication is the Unicode rendering of Isabelle symbols,
   3.824  as produced by Isabelle/jEdit, for example.
   3.825  
   3.826 -* Retired the now unused Isabelle tool "wwwfind". Similar
   3.827 -functionality may be integrated into PIDE/jEdit at a later point.
   3.828 +* Removed obsolete tool "wwwfind". Similar functionality may be
   3.829 +integrated into Isabelle/jEdit eventually.
   3.830 +
   3.831 +* Improved 'display_drafts' concerning desktop integration and
   3.832 +repeated invocation in PIDE front-end: re-use single file
   3.833 +$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views.
   3.834  
   3.835  * Windows: support for regular TeX installation (e.g. MiKTeX) instead
   3.836  of TeX Live from Cygwin.
   3.837  
   3.838 +* Session ROOT specifications require explicit 'document_files' for
   3.839 +robust dependencies on LaTeX sources.  Only these explicitly given
   3.840 +files are copied to the document output directory, before document
   3.841 +processing is started.
   3.842 +
   3.843  
   3.844  
   3.845  New in Isabelle2013-2 (December 2013)
     4.1 --- a/README	Tue Jul 01 14:05:05 2014 +0200
     4.2 +++ b/README	Tue Jul 01 14:52:08 2014 +0200
     4.3 @@ -17,19 +17,15 @@
     4.4     Some technical background information may be found in the Isabelle
     4.5     System Manual (directory doc).
     4.6  
     4.7 -User interfaces
     4.8 +User interface
     4.9  
    4.10     Isabelle/jEdit is an advanced Prover IDE based on jEdit and
    4.11 -   Isabelle/Scala.  It provides a metaphor of continuous proof
    4.12 -   checking of a versioned collection of theory sources, with
    4.13 -   instantaneous feedback in real-time and rich semantic markup
    4.14 -   associated with the formal text.
    4.15 -
    4.16 -   The classic Isabelle user interface is Proof General by David
    4.17 -   Aspinall and others.  It is a generic Emacs interface for proof
    4.18 -   assistants, including Isabelle.  Its main feature is script
    4.19 -   management, with stepwise proof scripting and partial locking of
    4.20 -   the editor buffer.
    4.21 +   Isabelle/Scala.  It is the main example application of the
    4.22 +   Isabelle/PIDE framework, and the default user interface of
    4.23 +   Isabelle.  It provides a metaphor of continuous proof checking of a
    4.24 +   versioned collection of theory sources, with instantaneous feedback
    4.25 +   in real-time and rich semantic markup associated with the formal
    4.26 +   text.
    4.27  
    4.28  Other sources of information
    4.29