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