author | wenzelm |

Tue Jul 01 14:52:08 2014 +0200 (2014-07-01) | |

changeset 57452 | ecad2a53755a |

parent 57451 | 3b10acac1d5e |

child 57453 | 77d13a98f1c8 |

misc updates for release;

ANNOUNCE | file | annotate | diff | revisions | |

CONTRIBUTORS | file | annotate | diff | revisions | |

NEWS | file | annotate | diff | revisions | |

README | file | annotate | diff | revisions |

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