# HG changeset patch # User wenzelm # Date 1404219128 -7200 # Node ID ecad2a53755a8e0e374ee00c5bb48a2e328e9aac # Parent 3b10acac1d5ef45a9f1f0e15e6e759ad2ea1ce28 misc updates for release; diff -r 3b10acac1d5e -r ecad2a53755a ANNOUNCE --- a/ANNOUNCE Tue Jul 01 14:05:05 2014 +0200 +++ b/ANNOUNCE Tue Jul 01 14:52:08 2014 +0200 @@ -1,27 +1,36 @@ -Subject: Announcing Isabelle2013-2 +Subject: Announcing Isabelle2014 To: isabelle-users@cl.cam.ac.uk -Isabelle2013-2 is now available. +Isabelle2014 is now available. + +This version significantly improves upon Isabelle2013-2, see the NEWS +file in the distribution for more details. Some highlights are: -This version supersedes Isabelle2013-1, which in turn consolidated -Isabelle2013 and introduced numerous improvements. See the NEWS file -in the distribution for more details. Some highlights are: +* Improved Isabelle/jEdit Prover IDE: navigation, completion, + spell-checking, Query panel, Simplifier Trace panel. -* Significantly improved Isabelle/jEdit Prover IDE. +* Support for auxiliary files within the Prover IDE. -* Consolidated multi-platform support: Linux, Windows, Mac OS X. +* Support for official Standard ML within the Prover IDE, + independently of Isabelle theory and proof development. -* Added and updated manuals: datatypes, implementation, isar-ref, jedit. +* HOL: BNF datatypes and codatatypes within theory Main, with numerous + add-on tools. -* New Spec_Check tool: Quickcheck for Isabelle/ML. +* HOL tool enhancements: Nitpick, Sledgehammer. + +* HOL: numerous library enhancements: Main, HOL-Multivariate_Analysis, + HOL-Probability. -* HOL library enhancements: Complex_Main, HOL-Library, - HOL-Multivariate_Analysis. +* HOL: internal SAT solver "cdclite" with models and proof traces. + +* HOL: updated SMT module, with support for SMT-LIB 2 and recent + versions of Z3, as well as CVC3, CVC4. -* HOL tool enhancements: Codegenerator, Function, Lifting, Transfer, - Nitpick, Sledgehammer. +* Updated and extended manuals: codegen, datatypes, implementation, + isar-ref, jedit, system. -* HOL-BNF: significantly improved BNF-based (co)datatype package. +* System integration: improved support of LateX on Windows platform. You may get Isabelle2013-2 from the following mirror sites: diff -r 3b10acac1d5e -r ecad2a53755a CONTRIBUTORS --- a/CONTRIBUTORS Tue Jul 01 14:05:05 2014 +0200 +++ b/CONTRIBUTORS Tue Jul 01 14:52:08 2014 +0200 @@ -3,40 +3,48 @@ who is listed as an author in one of the source files of this Isabelle distribution. -Contributions to this Isabelle version --------------------------------------- +Contributions to Isabelle2014 +----------------------------- * June 2014: Florian Haftmann, TUM - Consolidation and generalization of facts concerning products (resp. sums) - on finite sets. + Consolidation and generalization of facts concerning products + (resp. sums) on finite sets. * June 2014: Florian Haftmann, TUM Internal reorganisation of the local theory / named target stack. * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM - Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT, - Waldmeister, etc.). + Work on exotic automatic theorem provers for Sledgehammer (LEO-II, + veriT, Waldmeister, etc.). * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM - Various properties of exponentially, Erlang, and normal distributed random variables. + Various properties of exponentially, Erlang, and normal distributed + random variables. -* May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM +* May 2014: Cezary Kaliszyk, University of Innsbruck, and + Jasmin Blanchette, TUM SML-based engines for MaSh. * March 2014: René Thiemann Improved code generation for multisets. * February 2014: Florian Haftmann, TUM - Permanent interpretation inside theory, locale and class targets with mixin definitions. + Permanent interpretation inside theory, locale and class targets + with mixin definitions. + +* Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI + Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. -* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel, - and Jasmin Blanchette, TUM - Various improvements to the BNF-based (co)datatype package, including - a more polished "primcorec" command, optimizations, and integration in - the "HOL" session. +* Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, + Dmitriy Traytel, and Jasmin Blanchette, TUM + Various improvements to the BNF-based (co)datatype package, + including a more polished "primcorec" command, optimizations, and + integration in the "HOL" session. -* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM - "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3. +* Winter/Spring 2014: Sascha Boehme, QAware GmbH, and + Jasmin Blanchette, TUM + "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and + Z3 4.3. * January 2014: Lars Hupel, TUM An improved, interactive simplifier trace with integration into the diff -r 3b10acac1d5e -r ecad2a53755a NEWS --- a/NEWS Tue Jul 01 14:05:05 2014 +0200 +++ b/NEWS Tue Jul 01 14:52:08 2014 +0200 @@ -1,32 +1,19 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New in this Isabelle version ----------------------------- +New in Isabelle2014 (August 2014) +--------------------------------- *** General *** -* Document antiquotation @{url} produces markup for the given URL, -which results in an active hyperlink within the text. - -* Document antiquotation @{file_unchecked} is like @{file}, but does -not check existence within the file-system. - -* Discontinued legacy_isub_isup, which was a temporary Isabelle/ML -workaround in Isabelle2013-1. The prover process no longer accepts -old identifier syntax with \<^isub> or \<^isup>. - -* Syntax of document antiquotation @{rail} now uses \ instead -of "\\", to avoid the optical illusion of escaped backslash within -string token. Minor INCOMPATIBILITY. - -* Lexical syntax (inner and outer) supports text cartouches with -arbitrary nesting, and without escapes of quotes etc. The Prover IDE -supports input via ` (backquote). - -* The outer syntax categories "text" (for formal comments and document -markup commands) and "altstring" (for literal fact references) allow -cartouches as well, in addition to the traditional mix of quotations. +* Support for official Standard ML within the Isabelle context. +Command 'SML_file' reads and evaluates the given Standard ML file. +Toplevel bindings are stored within the theory context; the initial +environment is restricted to the Standard ML implementation of +Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' +and 'SML_export' allow to exchange toplevel bindings between the two +separate environments. See also ~~/src/Tools/SML/Examples.thy for +some examples. * More static checking of proof methods, which allows the system to form a closure over the concrete syntax. Method arguments should be @@ -37,25 +24,48 @@ exception. Potential INCOMPATIBILITY for non-conformant tactical proof tools. -* Support for official Standard ML within the Isabelle context. -Command 'SML_file' reads and evaluates the given Standard ML file. -Toplevel bindings are stored within the theory context; the initial -environment is restricted to the Standard ML implementation of -Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' -and 'SML_export' allow to exchange toplevel bindings between the two -separate environments. See also ~~/src/Tools/SML/Examples.thy for -some examples. - -* Updated and extended manuals: "codegen", "datatypes", -"implementation", "jedit", "system". +* Lexical syntax (inner and outer) supports text cartouches with +arbitrary nesting, and without escapes of quotes etc. The Prover IDE +supports input via ` (backquote). + +* The outer syntax categories "text" (for formal comments and document +markup commands) and "altstring" (for literal fact references) allow +cartouches as well, in addition to the traditional mix of quotations. + +* Syntax of document antiquotation @{rail} now uses \ instead +of "\\", to avoid the optical illusion of escaped backslash within +string token. General renovation of its syntax using text cartouces. +Minor INCOMPATIBILITY. + +* Discontinued legacy_isub_isup, which was a temporary workaround for +Isabelle/ML in Isabelle2013-1. The prover process no longer accepts +old identifier syntax with \<^isub> or \<^isup>. Potential +INCOMPATIBILITY. + +* Document antiquotation @{url} produces markup for the given URL, +which results in an active hyperlink within the text. + +* Document antiquotation @{file_unchecked} is like @{file}, but does +not check existence within the file-system. + +* Updated and extended manuals: codegen, datatypes, implementation, +isar-ref, jedit, system. *** Prover IDE -- Isabelle/Scala/jEdit *** -* Document panel: simplied interaction where every single mouse click -(re)opens document via desktop environment or as jEdit buffer. - -* Support for Navigator plugin (with toolbar buttons). +* Improved Document panel: simplied interaction where every single +mouse click (re)opens document via desktop environment or as jEdit +buffer. + +* Support for Navigator plugin (with toolbar buttons), with connection +to PIDE hyperlinks. + +* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. +Open text buffers take precedence over copies within the file-system. + +* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for +auxiliary ML files. * Improved syntactic and semantic completion mechanism, with simple templates, completion language context, name-space completion, @@ -72,12 +82,6 @@ * Integrated spell-checker for document text, comments etc. with completion popup and context-menu. -* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. -Open text buffers take precedence over copies within the file-system. - -* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for -auxiliary ML files. - * More general "Query" panel supersedes "Find" panel, with GUI access to commands 'find_theorems' and 'find_consts', as well as print operations for the context. Minor incompatibility in keyboard @@ -91,10 +95,6 @@ process, without requiring old-fashioned command-line invocation of "isabelle jedit -m MODE". -* New Simplifier Trace panel provides an interactive view of the -simplification process, enabled by the "simplifier_trace" attribute -within the context. - * More support for remote files (e.g. http) using standard Java networking operations instead of jEdit virtual file-systems. @@ -105,6 +105,11 @@ and window placement wrt. main editor view; optional menu item to "Detach" a copy where this makes sense. +* New Simplifier Trace panel provides an interactive view of the +simplification process, enabled by the "simplifier_trace" attribute +within the context. + + *** Pure *** @@ -139,12 +144,12 @@ * Low-level type-class commands 'classes', 'classrel', 'arities' have been discontinued to avoid the danger of non-trivial axiomatization that is not immediately visible. INCOMPATIBILITY, use regular -'instance' with proof. The required OFCLASS(...) theorem might be -postulated via 'axiomatization' beforehand, or the proof finished -trivially if the underlying class definition is made vacuous (without -any assumptions). See also Isabelle/ML operations -Axclass.axiomatize_class, Axclass.axiomatize_classrel, -Axclass.axiomatize_arity. +'instance' command with proof. The required OFCLASS(...) theorem +might be postulated via 'axiomatization' beforehand, or the proof +finished trivially if the underlying class definition is made vacuous +(without any assumptions). See also Isabelle/ML operations +Axclass.class_axiomatization, Axclass.classrel_axiomatization, +Axclass.arity_axiomatization. * Attributes "where" and "of" allow an optional context of local variables ('for' declaration): these variables become schematic in the @@ -167,10 +172,10 @@ * Inner syntax token language allows regular quoted strings "..." (only makes sense in practice, if outer syntax is delimited -differently). - -* Code generator preprocessor: explicit control of simp tracing -on a per-constant basis. See attribute "code_preproc". +differently, e.g. via cartouches). + +* Code generator preprocessor: explicit control of simp tracing on a +per-constant basis. See attribute "code_preproc". * Command 'print_term_bindings' supersedes 'print_binds' for clarity, but the latter is retained some time as Proof General legacy. @@ -180,63 +185,68 @@ * Qualified String.implode and String.explode. INCOMPATIBILITY. -* Command and antiquotation ''value'' are hardcoded against nbe and -ML now. Minor INCOMPATIBILITY. - -* Separate command ''approximate'' for approximative computation -in Decision_Procs/Approximation. Minor INCOMPATIBILITY. +* Command and antiquotation "value" are now hardcoded against nbe and +ML. Minor INCOMPATIBILITY. + +* Separate command "approximate" for approximative computation in +src/HOL/Decision_Procs/Approximation. Minor INCOMPATIBILITY. * Adjustion of INF and SUP operations: - * Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. - * Consolidated theorem names containing INFI and SUPR: have INF - and SUP instead uniformly. - * More aggressive normalization of expressions involving INF and Inf - or SUP and Sup. - * INF_image and SUP_image do not unfold composition. - * Dropped facts INF_comp, SUP_comp. - * Default congruence rules strong_INF_cong and strong_SUP_cong, - with simplifier implication in premises. Generalize and replace - former INT_cong, SUP_cong + - Elongated constants INFI and SUPR to INFIMUM and SUPREMUM. + - Consolidated theorem names containing INFI and SUPR: have INF and + SUP instead uniformly. + - More aggressive normalization of expressions involving INF and Inf + or SUP and Sup. + - INF_image and SUP_image do not unfold composition. + - Dropped facts INF_comp, SUP_comp. + - Default congruence rules strong_INF_cong and strong_SUP_cong, with + simplifier implication in premises. Generalize and replace former + INT_cong, SUP_cong + INCOMPATIBILITY. * Swapped orientation of facts image_comp and vimage_comp: + image_compose ~> image_comp [symmetric] image_comp ~> image_comp [symmetric] vimage_compose ~> vimage_comp [symmetric] vimage_comp ~> vimage_comp [symmetric] - INCOMPATIBILITY. - -* Simplifier: Enhanced solver of preconditions of rewrite rules - can now deal with conjunctions. - For help with converting proofs, the old behaviour of the simplifier - can be restored like this: declare/using [[simp_legacy_precond]] - This configuration option will disappear again in the future. + +INCOMPATIBILITY. + +* Simplifier: Enhanced solver of preconditions of rewrite rules can +now deal with conjunctions. For help with converting proofs, the old +behaviour of the simplifier can be restored like this: declare/using +[[simp_legacy_precond]]. This configuration option will disappear +again in the future. INCOMPATIBILITY. * HOL-Word: - * Abandoned fact collection "word_arith_alts", which is a - duplicate of "word_arith_wis". - * Dropped first (duplicated) element in fact collections - "sint_word_ariths", "word_arith_alts", "uint_word_ariths", - "uint_word_arith_bintrs". - -* Code generator: enforce case of identifiers only for strict -target language requirements. INCOMPATIBILITY. + - Abandoned fact collection "word_arith_alts", which is a duplicate + of "word_arith_wis". + - Dropped first (duplicated) element in fact collections + "sint_word_ariths", "word_arith_alts", "uint_word_ariths", + "uint_word_arith_bintrs". + +* Code generator: enforce case of identifiers only for strict target +language requirements. INCOMPATIBILITY. * Code generator: explicit proof contexts in many ML interfaces. INCOMPATIBILITY. -* Code generator: minimize exported identifiers by default. -Minor INCOMPATIBILITY. - -* Code generation for SML and OCaml: dropped arcane "no_signatures" option. -Minor INCOMPATIBILITY. +* Code generator: minimize exported identifiers by default. Minor +INCOMPATIBILITY. + +* Code generation for SML and OCaml: dropped arcane "no_signatures" +option. Minor INCOMPATIBILITY. * Simproc "finite_Collect" is no longer enabled by default, due to spurious crashes and other surprises. Potential INCOMPATIBILITY. -* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". - The "bnf", "wrap_free_constructors", "datatype_new", "codatatype", - "primcorec", and "primcorecursive" commands are now part of "Main". +* Moved new (co)datatype package and its dependencies from session + "HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', + 'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now + part of theory "Main". + Theory renamings: FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) Library/Wfrec.thy ~> Wfrec.thy @@ -260,58 +270,63 @@ BNF/More_BNFs.thy ~> Library/More_BNFs.thy BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy BNF/Examples/* ~> BNF_Examples/* + New theories: Wellorder_Extension.thy (split from Zorn.thy) Library/Cardinal_Notations.thy Library/BNF_Axomatization.thy BNF_Examples/Misc_Primcorec.thy BNF_Examples/Stream_Processor.thy + Discontinued theories: BNF/BNF.thy BNF/Equiv_Relations_More.thy - INCOMPATIBILITY. + +INCOMPATIBILITY. * New (co)datatype package: - * "primcorec" is fully implemented. - * "datatype_new" generates size functions ("size_xxx" and "size") as - required by "fun". - * BNFs are integrated with the Lifting tool and new-style (co)datatypes - with Transfer. - * Renamed commands: + - Command 'primcorec' is fully implemented. + - Command 'datatype_new' generates size functions ("size_xxx" and + "size") as required by 'fun'. + - BNFs are integrated with the Lifting tool and new-style + (co)datatypes with Transfer. + - Renamed commands: datatype_new_compat ~> datatype_compat primrec_new ~> primrec wrap_free_constructors ~> free_constructors INCOMPATIBILITY. - * The generated constants "xxx_case" and "xxx_rec" have been renamed + - The generated constants "xxx_case" and "xxx_rec" have been renamed "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). INCOMPATIBILITY. - * The constant "xxx_(un)fold" and related theorems are no longer generated. - Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec". + - The constant "xxx_(un)fold" and related theorems are no longer + generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually + using "prim(co)rec". INCOMPATIBILITY. - * No discriminators are generated for nullary constructors by default, - eliminating the need for the odd "=:" syntax. + - No discriminators are generated for nullary constructors by + default, eliminating the need for the odd "=:" syntax. INCOMPATIBILITY. - * No discriminators or selectors are generated by default by + - No discriminators or selectors are generated by default by "datatype_new", unless custom names are specified or the new "discs_sels" option is passed. INCOMPATIBILITY. * Old datatype package: - * The generated theorems "xxx.cases" and "xxx.recs" have been renamed - "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case"). - INCOMPATIBILITY. - * The generated constants "xxx_case", "xxx_rec", and "xxx_size" have been - renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., "prod_case" ~> - "case_prod"). - INCOMPATIBILITY. - -* The types "'a list" and "'a option", their set and map functions, their - relators, and their selectors are now produced using the new BNF-based - datatype package. + - The generated theorems "xxx.cases" and "xxx.recs" have been + renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> + "sum.case"). INCOMPATIBILITY. + - The generated constants "xxx_case", "xxx_rec", and "xxx_size" have + been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., + "prod_case" ~> "case_prod"). INCOMPATIBILITY. + +* The types "'a list" and "'a option", their set and map functions, + their relators, and their selectors are now produced using the new + BNF-based datatype package. + Renamed constants: Option.set ~> set_option Option.map ~> map_option option_rel ~> rel_option + Renamed theorems: set_def ~> set_rec[abs_def] map_def ~> map_rec[abs_def] @@ -323,7 +338,8 @@ hd.simps ~> list.sel(1) tl.simps ~> list.sel(2-3) the.simps ~> option.sel - INCOMPATIBILITY. + +INCOMPATIBILITY. * The following map functions and relators have been renamed: sum_map ~> map_sum @@ -333,16 +349,18 @@ fun_rel ~> rel_fun set_rel ~> rel_set filter_rel ~> rel_filter - fset_rel ~> rel_fset (in "Library/FSet.thy") - cset_rel ~> rel_cset (in "Library/Countable_Set_Type.thy") - vset ~> rel_vset (in "Library/Quotient_Set.thy") - -* New theories: - Cardinals/Ordinal_Arithmetic.thy - Library/Tree - -* Theory reorganizations: - * Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy + fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy") + cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy") + vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy") + +INCOMPATIBILITY. + +* New theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. + +* New theory src/HOL/Library/Tree.thy. + +* Theory reorganization: + Big_Operators.thy ~> Groups_Big.thy and Lattices_Big.thy * Consolidated some facts about big group operators: @@ -411,41 +429,41 @@ Dropped setsum_reindex_id, setprod_reindex_id (simple variants of setsum.reindex [symmetric], setprod.reindex [symmetric]). - INCOMPATIBILITY. - -* New internal SAT solver "cdclite" that produces models and proof traces. - This solver replaces the internal SAT solvers "enumerate" and "dpll". - Applications that explicitly used one of these two SAT solvers should - use "cdclite" instead. In addition, "cdclite" is now the default SAT - solver for the "sat" and "satx" proof methods and corresponding tactics; - the old default can be restored using - "declare [[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. - -* SMT module: - * A new version of the SMT module, temporarily called "SMT2", uses SMT-LIB 2 - and supports recent versions of Z3 (e.g., 4.3). The new proof method is - called "smt2". CVC3 and CVC4 are also supported as oracles. Yices is no - longer supported, because no version of the solver can handle both - SMT-LIB 2 and quantifiers. +INCOMPATIBILITY. + +* New internal SAT solver "cdclite" that produces models and proof +traces. This solver replaces the internal SAT solvers "enumerate" and +"dpll". Applications that explicitly used one of these two SAT +solvers should use "cdclite" instead. In addition, "cdclite" is now +the default SAT solver for the "sat" and "satx" proof methods and +corresponding tactics; the old default can be restored using "declare +[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY. + +* SMT module: A new version of the SMT module, temporarily called +"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g., +4.3). The new proof method is called "smt2". CVC3 and CVC4 are also +supported as oracles. Yices is no longer supported, because no version +of the solver can handle both SMT-LIB 2 and quantifiers. * Sledgehammer: - Z3 can now produce Isar proofs. - MaSh overhaul: - - New SML-based learning engines eliminate the dependency on Python - and increase performance and reliability. - - MaSh and MeSh are now used by default together with the traditional - MePo (Meng-Paulson) relevance filter. To disable MaSh, set the "MaSh" - system option in Plugin Options / Isabelle / General to "none". + . New SML-based learning engines eliminate the dependency on + Python and increase performance and reliability. + . MaSh and MeSh are now used by default together with the + traditional MePo (Meng-Paulson) relevance filter. To disable + MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin + Options / Isabelle / General to "none". - New option: smt_proofs - Renamed options: isar_compress ~> compress isar_try0 ~> try0 - INCOMPATIBILITY. - -* Metis: - - Removed legacy proof method 'metisFT'. Use 'metis (full_types)' instead. - INCOMPATIBILITY. + +INCOMPATIBILITY. + +* Metis: Removed legacy proof method 'metisFT'. Use 'metis +(full_types)' instead. INCOMPATIBILITY. * Try0: Added 'algebra' and 'meson' to the set of proof methods. @@ -467,7 +485,7 @@ * Abolished slightly odd global lattice interpretation for min/max. -Fact consolidations: + Fact consolidations: min_max.inf_assoc ~> min.assoc min_max.inf_commute ~> min.commute min_max.inf_left_commute ~> min.left_commute @@ -513,18 +531,18 @@ min.left_commute, min.left_idem, max.commute, max.assoc, max.left_commute, max.left_idem directly. -For min_max.inf_sup_ord, prefer (one of) min.cobounded1, min.cobounded2, -max.cobounded1m max.cobounded2 directly. +For min_max.inf_sup_ord, prefer (one of) min.cobounded1, +min.cobounded2, max.cobounded1m max.cobounded2 directly. For min_ac or max_ac, prefer more general collection ac_simps. INCOMPATBILITY. -* Word library: bit representations prefer type bool over type bit. -INCOMPATIBILITY. - -* Theorem disambiguation Inf_le_Sup (on finite sets) ~> Inf_fin_le_Sup_fin. -INCOMPATIBILITY. +* HOL-Word: bit representations prefer type bool over type bit. +INCOMPATIBILITY. + +* Theorem disambiguation Inf_le_Sup (on finite sets) ~> +Inf_fin_le_Sup_fin. INCOMPATIBILITY. * Code generations are provided for make, fields, extend and truncate operations on records. @@ -534,21 +552,25 @@ * Fact generalization and consolidation: neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 -INCOMPATIBILITY. - -* Purely algebraic definition of even. Fact generalization and consolidation: + +INCOMPATIBILITY. + +* Purely algebraic definition of even. Fact generalization and + consolidation: nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd even_zero_(nat|int) ~> even_zero + INCOMPATIBILITY. * Abolished neg_numeral. - * Canonical representation for minus one is "- 1". - * Canonical representation for other negative numbers is "- (numeral _)". - * When devising rule sets for number calculation, consider the + - Canonical representation for minus one is "- 1". + - Canonical representation for other negative numbers is "- (numeral _)". + - When devising rule sets for number calculation, consider the following canonical cases: 0, 1, numeral _, - 1, - numeral _. - * HOLogic.dest_number also recognizes numerals in non-canonical forms + - HOLogic.dest_number also recognizes numerals in non-canonical forms like "numeral One", "- numeral One", "- 0" and even "- ... - _". - * Syntax for negative numerals is mere input syntax. + - Syntax for negative numerals is mere input syntax. + INCOMPATIBILITY. * Elimination of fact duplicates: @@ -556,6 +578,7 @@ diff_eq_0_iff_eq ~> right_minus_eq nat_infinite ~> infinite_UNIV_nat int_infinite ~> infinite_UNIV_int + INCOMPATIBILITY. * Fact name consolidation: @@ -564,6 +587,7 @@ le_minus_self_iff ~> less_eq_neg_nonpos neg_less_nonneg ~> neg_less_pos less_minus_self_iff ~> less_neg_neg [simp] + INCOMPATIBILITY. * More simplification rules on unary and binary minus: @@ -571,9 +595,9 @@ add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, add_minus_cancel, diff_add_cancel, le_add_same_cancel1, le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, -minus_add_cancel, uminus_add_conv_diff. These correspondingly -have been taken away from fact collections algebra_simps and -field_simps. INCOMPATIBILITY. +minus_add_cancel, uminus_add_conv_diff. These correspondingly have +been taken away from fact collections algebra_simps and field_simps. +INCOMPATIBILITY. To restore proofs, the following patterns are helpful: @@ -588,18 +612,18 @@ or the brute way with "simp add: diff_conv_add_uminus del: add_uminus_conv_diff". -* SUP and INF generalized to conditionally_complete_lattice +* SUP and INF generalized to conditionally_complete_lattice. * Theory Lubs moved HOL image to HOL-Library. It is replaced by -Conditionally_Complete_Lattices. INCOMPATIBILITY. - -* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them -instead of explicitly stating boundedness of sets. - -* ccpo.admissible quantifies only over non-empty chains to allow -more syntax-directed proof rules; the case of the empty chain -shows up as additional case in fixpoint induction proofs. -INCOMPATIBILITY +Conditionally_Complete_Lattices. INCOMPATIBILITY. + +* Introduce bdd_above and bdd_below in theory +Conditionally_Complete_Lattices, use them instead of explicitly +stating boundedness of sets. + +* ccpo.admissible quantifies only over non-empty chains to allow more +syntax-directed proof rules; the case of the empty chain shows up as +additional case in fixpoint induction proofs. INCOMPATIBILITY. * Removed and renamed theorems in Series: summable_le ~> suminf_le @@ -617,10 +641,13 @@ removed series_zero, replaced by sums_finite removed auxiliary lemmas: + sumr_offset, sumr_offset2, sumr_offset3, sumr_offset4, sumr_group, - half, le_Suc_ex_iff, lemma_realpow_diff_sumr, real_setsum_nat_ivl_bounded, - summable_le2, ratio_test_lemma2, sumr_minus_one_realpow_zerom, - sumr_one_lb_realpow_zero, summable_convergent_sumr_iff, sumr_diff_mult_const + half, le_Suc_ex_iff, lemma_realpow_diff_sumr, + real_setsum_nat_ivl_bounded, summable_le2, ratio_test_lemma2, + sumr_minus_one_realpow_zerom, sumr_one_lb_realpow_zero, + summable_convergent_sumr_iff, sumr_diff_mult_const + INCOMPATIBILITY. * Replace (F)DERIV syntax by has_derivative: @@ -632,10 +659,10 @@ - removed constant isDiff - - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as input - syntax. - - - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed + - "DERIV f x : f'" and "FDERIV f x : f'" syntax is only available as + input syntax. + + - "DERIV f x : s : f'" and "FDERIV f x : s : f'" syntax removed. - Renamed FDERIV_... lemmas to has_derivative_... @@ -643,8 +670,9 @@ - removed DERIV_intros, has_derivative_eq_intros - - introduced derivative_intros and deriative_eq_intros which includes now rules for - DERIV, has_derivative and has_vector_derivative. + - introduced derivative_intros and deriative_eq_intros which + includes now rules for DERIV, has_derivative and + has_vector_derivative. - Other renamings: differentiable_def ~> real_differentiable_def @@ -654,24 +682,27 @@ isDiff_der ~> differentiable_def deriv_fderiv ~> has_field_derivative_def deriv_def ~> DERIV_def -INCOMPATIBILITY. - -* Include more theorems in continuous_intros. Remove the continuous_on_intros, - isCont_intros collections, these facts are now in continuous_intros. - -* Theorems about complex numbers are now stated only using Re and Im, the Complex - constructor is not used anymore. It is possible to use primcorec to defined the - behaviour of a complex-valued function. - - Removed theorems about the Complex constructor from the simpset, they are - available as the lemma collection legacy_Complex_simps. This especially - removes + +INCOMPATIBILITY. + +* Include more theorems in continuous_intros. Remove the +continuous_on_intros, isCont_intros collections, these facts are now +in continuous_intros. + +* Theorems about complex numbers are now stated only using Re and Im, +the Complex constructor is not used anymore. It is possible to use +primcorec to defined the behaviour of a complex-valued function. + +Removed theorems about the Complex constructor from the simpset, they +are available as the lemma collection legacy_Complex_simps. This +especially removes + i_complex_of_real: "ii * complex_of_real r = Complex 0 r". - Instead the reverse direction is supported with +Instead the reverse direction is supported with Complex_eq: "Complex a b = a + \ * b" - Moved csqrt from Fundamental_Algebra_Theorem to Complex. +Moved csqrt from Fundamental_Algebra_Theorem to Complex. Renamings: Re/Im ~> complex.sel @@ -701,36 +732,37 @@ complex_inverse_def complex_scaleR_def +INCOMPATIBILITY. + * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. * Nitpick: - - Fixed soundness bug whereby mutually recursive datatypes could take - infinite values. - - Fixed soundness bug with low-level number functions such as "Abs_Integ" and - "Rep_Integ". + - Fixed soundness bug whereby mutually recursive datatypes could + take infinite values. + - Fixed soundness bug with low-level number functions such as + "Abs_Integ" and "Rep_Integ". - Removed "std" option. - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to "hide_types". * HOL-Multivariate_Analysis: - - type class ordered_real_vector for ordered vector spaces - - new theory Complex_Basic_Analysis defining complex derivatives, + - Type class ordered_real_vector for ordered vector spaces. + - New theory Complex_Basic_Analysis defining complex derivatives, holomorphic functions, etc., ported from HOL Light's canal.ml. - - changed order of ordered_euclidean_space to be compatible with + - Changed order of ordered_euclidean_space to be compatible with pointwise ordering on products. Therefore instance of conditionally_complete_lattice and ordered_real_vector. INCOMPATIBILITY: use box instead of greaterThanLessThan or - explicit set-comprehensions with eucl_less for other (half-) open + explicit set-comprehensions with eucl_less for other (half-)open intervals. - - renamed theorems: derivative_linear ~> has_derivative_bounded_linear derivative_is_linear ~> has_derivative_linear bounded_linear_imp_linear ~> bounded_linear.linear * HOL-Probability: - - replaced the Lebesgue integral on real numbers by the more general Bochner - integral for functions into a real-normed vector space. + - replaced the Lebesgue integral on real numbers by the more general + Bochner integral for functions into a real-normed vector space. integral_zero ~> integral_zero / integrable_zero integral_minus ~> integral_minus / integrable_minus @@ -793,15 +825,17 @@ - Renamed positive_integral to nn_integral: - * Renamed all lemmas "*positive_integral*" to *nn_integral*" + . Renamed all lemmas "*positive_integral*" to *nn_integral*" positive_integral_positive ~> nn_integral_nonneg - * Renamed abbreviation integral\<^sup>P to integral\<^sup>N. - - - Formalized properties about exponentially, Erlang, and normal distributed - random variables. - -* Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it. + . Renamed abbreviation integral\<^sup>P to integral\<^sup>N. + + - Formalized properties about exponentially, Erlang, and normal + distributed random variables. + +* Removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by +session Kleene_Algebra in AFP. + *** Scala *** @@ -811,6 +845,9 @@ specific and may override results accumulated so far. The elements guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. +* Substantial reworking of internal PIDE protocol communication +channels. INCOMPATIBILITY. + *** ML *** @@ -818,8 +855,8 @@ structure Runtime. Minor INCOMPATIBILITY. * Discontinued old Toplevel.debug in favour of system option -"ML_exception_trace", which may be also declared within the context via -"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. +"ML_exception_trace", which may be also declared within the context +via "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. * Renamed configuration option "ML_trace" to "ML_source_trace". Minor INCOMPATIBILITY. @@ -878,21 +915,6 @@ the "system" manual for general explanations about add-on components, notably those that are not bundled with the normal release. -* Session ROOT specifications require explicit 'document_files' for -robust dependencies on LaTeX sources. Only these explicitly given -files are copied to the document output directory, before document -processing is started. - -* Simplified "isabelle display" tool. Settings variables DVI_VIEWER -and PDF_VIEWER now refer to the actual programs, not shell -command-lines. Discontinued option -c: invocation may be asynchronous -via desktop environment, without any special precautions. Potential -INCOMPATIBILITY with ambitious private settings. - -* Improved 'display_drafts' concerning desktop integration and -repeated invocation in PIDE front-end: re-use single file -$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. - * The raw Isabelle process executable has been renamed from "isabelle-process" to "isabelle_process", which conforms to common shell naming conventions, and allows to define a shell function within @@ -904,16 +926,31 @@ with implicit build like "isabelle jedit", and without the mostly obsolete Isar TTY loop. +* Simplified "isabelle display" tool. Settings variables DVI_VIEWER +and PDF_VIEWER now refer to the actual programs, not shell +command-lines. Discontinued option -c: invocation may be asynchronous +via desktop environment, without any special precautions. Potential +INCOMPATIBILITY with ambitious private settings. + * Removed obsolete "isabelle unsymbolize". Note that the usual format for email communication is the Unicode rendering of Isabelle symbols, as produced by Isabelle/jEdit, for example. -* Retired the now unused Isabelle tool "wwwfind". Similar -functionality may be integrated into PIDE/jEdit at a later point. +* Removed obsolete tool "wwwfind". Similar functionality may be +integrated into Isabelle/jEdit eventually. + +* Improved 'display_drafts' concerning desktop integration and +repeated invocation in PIDE front-end: re-use single file +$ISABELLE_HOME_USER/tmp/drafts.pdf and corresponding views. * Windows: support for regular TeX installation (e.g. MiKTeX) instead of TeX Live from Cygwin. +* Session ROOT specifications require explicit 'document_files' for +robust dependencies on LaTeX sources. Only these explicitly given +files are copied to the document output directory, before document +processing is started. + New in Isabelle2013-2 (December 2013) diff -r 3b10acac1d5e -r ecad2a53755a README --- a/README Tue Jul 01 14:05:05 2014 +0200 +++ b/README Tue Jul 01 14:52:08 2014 +0200 @@ -17,19 +17,15 @@ Some technical background information may be found in the Isabelle System Manual (directory doc). -User interfaces +User interface Isabelle/jEdit is an advanced Prover IDE based on jEdit and - Isabelle/Scala. It provides a metaphor of continuous proof - checking of a versioned collection of theory sources, with - instantaneous feedback in real-time and rich semantic markup - associated with the formal text. - - The classic Isabelle user interface is Proof General by David - Aspinall and others. It is a generic Emacs interface for proof - assistants, including Isabelle. Its main feature is script - management, with stepwise proof scripting and partial locking of - the editor buffer. + Isabelle/Scala. It is the main example application of the + Isabelle/PIDE framework, and the default user interface of + Isabelle. It provides a metaphor of continuous proof checking of a + versioned collection of theory sources, with instantaneous feedback + in real-time and rich semantic markup associated with the formal + text. Other sources of information