summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 31 Dec 2015 21:24:58 +0100 | |

changeset 62017 | 038ee85c95e4 |

parent 62016 | 740c70a21523 |

child 62018 | 01823b93ddaf |

misc tuning for release;

--- a/NEWS Thu Dec 31 21:06:09 2015 +0100 +++ b/NEWS Thu Dec 31 21:24:58 2015 +0100 @@ -9,6 +9,18 @@ *** General *** +* Former "xsymbols" syntax with Isabelle symbols is used by default, +without any special print mode. Important ASCII replacement syntax +remains available under print mode "ASCII", but less important syntax +has been removed (see below). + +* Support for more arrow symbols, with rendering in LaTeX and +Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow> + +* Syntax for formal comments "-- text" now also supports the symbolic +form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps +to update old sources. + * Toplevel theorem statements have been simplified as follows: theorems ~> lemmas @@ -22,31 +34,9 @@ * Toplevel theorem statement 'proposition' is another alias for 'theorem'. -* Syntax for formal comments "-- text" now also supports the symbolic -form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps -to update old sources. - -* Former "xsymbols" syntax with Isabelle symbols is used by default, -without any special print mode. Important ASCII replacement syntax -remains available under print mode "ASCII", but less important syntax -has been removed (see below). - -* Support for more arrow symbols, with rendering in LaTeX and -Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow> - *** Prover IDE -- Isabelle/Scala/jEdit *** -* Completion of symbols via prefix of \<name> or \<^name> or \name is -always possible, independently of the language context. It is never -implicit: a popup will show up unconditionally. - -* Additional abbreviations for syntactic completion may be specified in -$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. - -* Improved scheduling for urgent print tasks (e.g. command state output, -interactive queries) wrt. long-running background tasks. - * IDE support for the source-level debugger of Poly/ML, to work with Isabelle/ML and official Standard ML. Configuration option "ML_debugger" and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', @@ -56,9 +46,6 @@ At least one Debugger view needs to be active to have any effect on the running ML program. -* The main Isabelle executable is managed as single-instance Desktop -application uniformly on all platforms: Linux, Windows, Mac OS X. - * The State panel manages explicit proof state output, with dynamic auto-update according to cursor movement. Alternatively, the jEdit action "isabelle.update-state" (shortcut S+ENTER) triggers manual @@ -80,6 +67,17 @@ due to ad-hoc updates by auxiliary GUI components, such as the State panel. +* Improved scheduling for urgent print tasks (e.g. command state output, +interactive queries) wrt. long-running background tasks. + +* Completion of symbols via prefix of \<name> or \<^name> or \name is +always possible, independently of the language context. It is never +implicit: a popup will show up unconditionally. + +* Additional abbreviations for syntactic completion may be specified in +$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with +support for simple templates using ASCII 007 (bell) as placeholder. + * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls emphasized text style; the effect is visible in document output, not in the editor. @@ -87,15 +85,18 @@ * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, instead of former C+e LEFT. -* New command-line tool "isabelle jedit_client" allows to connect to an -already running Isabelle/jEdit process. This achieves the effect of -single-instance applications seen on common GUI desktops. - * The command-line tool "isabelle jedit" and the isabelle.Main application wrapper threat the default $USER_HOME/Scratch.thy more uniformly, and allow the dummy file argument ":" to open an empty buffer instead. +* New command-line tool "isabelle jedit_client" allows to connect to an +already running Isabelle/jEdit process. This achieves the effect of +single-instance applications seen on common GUI desktops. + +* The main Isabelle executable is managed as single-instance Desktop +application uniformly on all platforms: Linux, Windows, Mac OS X. + * The default look-and-feel for Linux is the traditional "Metal", which works better with GUI scaling for very high-resolution displays (e.g. 4K). Moreover, it is generally more robust than "Nimbus". @@ -103,6 +104,21 @@ *** Document preparation *** +* Commands 'paragraph' and 'subparagraph' provide additional section +headings. Thus there are 6 levels of standard headings, as in HTML. + +* Command 'text_raw' has been clarified: input text is processed as in +'text' (with antiquotations and control symbols). The key difference is +the lack of the surrounding isabelle markup environment in output. + +* Text is structured in paragraphs and nested lists, using notation that +is similar to Markdown. The control symbols for list items are as +follows: + + \<^item> itemize + \<^enum> enumerate + \<^descr> description + * There is a new short form for antiquotations with a single argument that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. @@ -110,18 +126,6 @@ standard Isabelle fonts provide glyphs to render important control symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". -* Antiquotation @{theory_text} prints uninterpreted theory source text -(outer syntax with command keywords etc.). This may be used in the short -form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". - -* @{verbatim [display]} supports option "indent". - -* Antiquotation @{doc ENTRY} provides a reference to the given -documentation, with a hyperlink in the Prover IDE. - -* Antiquotations @{command}, @{method}, @{attribute} print checked -entities of the Isar language. - * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using standard LaTeX macros of the same names. @@ -138,44 +142,32 @@ argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial or terminal spaces are ignored. +* Antiquotations @{emph} and @{bold} output LaTeX source recursively, +adding appropriate text style markup. These may be used in the short +form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. + +* Document antiquotation @{footnote} outputs LaTeX source recursively, +marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. + +* Antiquotation @{verbatim [display]} supports option "indent". + +* Antiquotation @{theory_text} prints uninterpreted theory source text +(outer syntax with command keywords etc.). This may be used in the short +form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". + +* Antiquotation @{doc ENTRY} provides a reference to the given +documentation, with a hyperlink in the Prover IDE. + +* Antiquotations @{command}, @{method}, @{attribute} print checked +entities of the Isar language. + * HTML presentation uses the standard IsabelleText font and Unicode rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former print mode "HTML" loses its special meaning. -* Commands 'paragraph' and 'subparagraph' provide additional section -headings. Thus there are 6 levels of standard headings, as in HTML. - -* Text is structured in paragraphs and nested lists, using notation that -is similar to Markdown. The control symbols for list items are as -follows: - - \<^item> itemize - \<^enum> enumerate - \<^descr> description - -* Command 'text_raw' has been clarified: input text is processed as in -'text' (with antiquotations and control symbols). The key difference is -the lack of the surrounding isabelle markup environment in output. - -* Document antiquotations @{emph} and @{bold} output LaTeX source -recursively, adding appropriate text style markup. These may be used in -the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. - -* Document antiquotation @{footnote} outputs LaTeX source recursively, -marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. - *** Isar *** -* Command 'obtain' binds term abbreviations (via 'is' patterns) in the -proof body as well, abstracted over relevant parameters. - -* Improved type-inference for theorem statement 'obtains': separate -parameter scope for of each clause. - -* Term abbreviations via 'is' patterns also work for schematic -statements: result is abstracted over unknowns. - * Local goals ('have', 'show', 'hence', 'thus') allow structured rule statements like fixes/assumes/shows in theorem specifications, but the notation is postfix with keywords 'if' (or 'when') and 'for'. For @@ -234,9 +226,6 @@ show "C x" when "A x" "B x" for x -* New command 'supply' supports fact definitions during goal refinement -('apply' scripts). - * New command 'consider' states rules for generalized elimination and case splitting. This is like a toplevel statement "theorem obtains" used within a proof body; or like a multi-branch 'obtain' without activation @@ -274,11 +263,36 @@ is still available as legacy for some time. Documentation now explains '..' more accurately as "by standard" instead of "by rule". +* Nesting of Isar goal structure has been clarified: the context after +the initial backwards refinement is retained for the whole proof, within +all its context sections (as indicated via 'next'). This is e.g. +relevant for 'using', 'including', 'supply': + + have "A \<and> A" if a: A for A + supply [simp] = a + proof + show A by simp + next + show A by simp + qed + +* Command 'obtain' binds term abbreviations (via 'is' patterns) in the +proof body as well, abstracted over relevant parameters. + +* Improved type-inference for theorem statement 'obtains': separate +parameter scope for of each clause. + +* Term abbreviations via 'is' patterns also work for schematic +statements: result is abstracted over unknowns. + * Command 'subgoal' allows to impose some structure on backward refinements, to avoid proof scripts degenerating into long of 'apply' sequences. Further explanations and examples are given in the isar-ref manual. +* Command 'supply' supports fact definitions during goal refinement +('apply' scripts). + * Proof method "goal_cases" turns the current subgoals into cases within the context; the conclusion is bound to variable ?case in each case. For example: @@ -308,18 +322,8 @@ "goals" achieves a similar effect within regular Isar; often it can be done more adequately by other means (e.g. 'consider'). -* Nesting of Isar goal structure has been clarified: the context after -the initial backwards refinement is retained for the whole proof, within -all its context sections (as indicated via 'next'). This is e.g. -relevant for 'using', 'including', 'supply': - - have "A \<and> A" if a: A for A - supply [simp] = a - proof - show A by simp - next - show A by simp - qed +* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` +as well, not just "by this" or "." as before. * Method "sleep" succeeds after a real-time delay (in seconds). This is occasionally useful for demonstration and testing purposes. @@ -333,17 +337,16 @@ INCOMPATIBILITY, remove '!' and add '?' as required. * Keyword 'rewrites' identifies rewrite morphisms in interpretation -commands. Previously, the keyword was 'where'. INCOMPATIBILITY. +commands. Previously, the keyword was 'where'. INCOMPATIBILITY. * More gentle suppression of syntax along locale morphisms while -printing terms. Previously 'abbreviation' and 'notation' declarations -would be suppressed for morphisms except term identity. Now +printing terms. Previously 'abbreviation' and 'notation' declarations +would be suppressed for morphisms except term identity. Now 'abbreviation' is also kept for morphims that only change the involved -parameters, and only 'notation' is suppressed. This can be of great -help when working with complex locale hierarchies, because proof -states are displayed much more succinctly. It also means that only -notation needs to be redeclared if desired, as illustrated by this -example: +parameters, and only 'notation' is suppressed. This can be of great help +when working with complex locale hierarchies, because proof states are +displayed much more succinctly. It also means that only notation needs +to be redeclared if desired, as illustrated by this example: locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65) begin @@ -369,11 +372,8 @@ * Command 'print_definitions' prints dependencies of definitional specifications. This functionality used to be part of 'print_theory'. -* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` -as well, not just "by this" or "." as before. - * Configuration option rule_insts_schematic has been discontinued -(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. +(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. * Abbreviations in type classes now carry proper sort constraint. Rare INCOMPATIBILITY in situations where the previous misbehaviour @@ -386,9 +386,71 @@ *** HOL *** -* Combinator to represent case distinction on products is named "case_prod", -uniformly, discontinuing any input aliasses. Very popular theorem aliasses -have been retained. +* The 'typedef' command has been upgraded from a partially checked +"axiomatization", to a full definitional specification that takes the +global collection of overloaded constant / type definitions into +account. Type definitions with open dependencies on overloaded +definitions need to be specified as "typedef (overloaded)". This +provides extra robustness in theory construction. Rare INCOMPATIBILITY. + +* Qualification of various formal entities in the libraries is done more +uniformly via "context begin qualified definition ... end" instead of +old-style "hide_const (open) ...". Consequently, both the defined +constant and its defining fact become qualified, e.g. Option.is_none and +Option.is_none_def. Occasional INCOMPATIBILITY in applications. + +* Some old and rarely used ASCII replacement syntax has been removed. +INCOMPATIBILITY, standard syntax with symbols should be used instead. +The subsequent commands help to reproduce the old forms, e.g. to +simplify porting old theories: + + notation iff (infixr "<->" 25) + + notation Times (infixr "<*>" 80) + + type_notation Map.map (infixr "~=>" 0) + notation Map.map_comp (infixl "o'_m" 55) + + type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) + + notation FuncSet.funcset (infixr "->" 60) + notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) + + notation Omega_Words_Fun.conc (infixr "conc" 65) + + notation Preorder.equiv ("op ~~") + and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) + + notation (in topological_space) tendsto (infixr "--->" 55) + notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) + notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) + + notation NSA.approx (infixl "@=" 50) + notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) + notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) + +* The alternative notation "\<Colon>" for type and sort constraints has been +removed: in LaTeX document output it looks the same as "::". +INCOMPATIBILITY, use plain "::" instead. + +* Commands 'inductive' and 'inductive_set' work better when names for +intro rules are omitted: the "cases" and "induct" rules no longer +declare empty case_names, but no case_names at all. This allows to use +numbered cases in proofs, without requiring method "goal_cases". + +* Inductive definitions ('inductive', 'coinductive', etc.) expose +low-level facts of the internal construction only if the option +"inductive_defs" is enabled. This refers to the internal predicate +definition and its monotonicity result. Rare INCOMPATIBILITY. + +* Recursive function definitions ('fun', 'function', 'partial_function') +expose low-level facts of the internal construction only if the option +"function_defs" is enabled. Rare INCOMPATIBILITY. + +* Combinator to represent case distinction on products is named +"case_prod", uniformly, discontinuing any input aliasses. Very popular +theorem aliasses have been retained. + Consolidated facts: PairE ~> prod.exhaust Pair_eq ~> prod.inject @@ -425,36 +487,21 @@ split_rsp ~> case_prod_rsp curry_split ~> curry_case_prod split_curry ~> case_prod_curry + Changes in structure HOLogic: split_const ~> case_prod_const mk_split ~> mk_case_prod mk_psplits ~> mk_ptupleabs strip_psplits ~> strip_ptupleabs -INCOMPATIBILITY. - -* Commands 'inductive' and 'inductive_set' work better when names for -intro rules are omitted: the "cases" and "induct" rules no longer -declare empty case_names, but no case_names at all. This allows to use -numbered cases in proofs, without requiring method "goal_cases". - -* The 'typedef' command has been upgraded from a partially checked -"axiomatization", to a full definitional specification that takes the -global collection of overloaded constant / type definitions into -account. Type definitions with open dependencies on overloaded -definitions need to be specified as "typedef (overloaded)". This -provides extra robustness in theory construction. Rare INCOMPATIBILITY. - -* Qualification of various formal entities in the libraries is done more -uniformly via "context begin qualified definition ... end" instead of -old-style "hide_const (open) ...". Consequently, both the defined -constant and its defining fact become qualified, e.g. Option.is_none and -Option.is_none_def. Occasional INCOMPATIBILITY in applications. - -* The coercions to type 'real' have been reorganised. The function 'real' -is no longer overloaded, but has type 'nat => real' and abbreviates -of_nat for that type. Also 'real_of_int :: int => real' abbreviates -of_int for that type. Other overloaded instances of 'real' have been -replaced by 'real_of_ereal' and 'real_of_float'. + +INCOMPATIBILITY. + +* The coercions to type 'real' have been reorganised. The function +'real' is no longer overloaded, but has type 'nat => real' and +abbreviates of_nat for that type. Also 'real_of_int :: int => real' +abbreviates of_int for that type. Other overloaded instances of 'real' +have been replaced by 'real_of_ereal' and 'real_of_float'. + Consolidated facts (among others): real_of_nat_le_iff -> of_nat_le_iff real_of_nat_numeral of_nat_numeral @@ -478,41 +525,8 @@ floor_divide_eq_div floor_divide_of_int_eq real_of_int_zero_cancel of_nat_eq_0_iff ceiling_real_of_int ceiling_of_int -INCOMPATIBILITY. - -* Some old and rarely used ASCII replacement syntax has been removed. -INCOMPATIBILITY, standard syntax with symbols should be used instead. -The subsequent commands help to reproduce the old forms, e.g. to -simplify porting old theories: - - notation iff (infixr "<->" 25) - - notation Times (infixr "<*>" 80) - - type_notation Map.map (infixr "~=>" 0) - notation Map.map_comp (infixl "o'_m" 55) - - type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) - - notation FuncSet.funcset (infixr "->" 60) - notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) - - notation Omega_Words_Fun.conc (infixr "conc" 65) - - notation Preorder.equiv ("op ~~") - and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) - - notation (in topological_space) tendsto (infixr "--->" 55) - notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) - notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) - - notation NSA.approx (infixl "@=" 50) - notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) - notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) - -* The alternative notation "\<Colon>" for type and sort constraints has been -removed: in LaTeX document output it looks the same as "::". -INCOMPATIBILITY, use plain "::" instead. + +INCOMPATIBILITY. * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has been removed. INCOMPATIBILITY. @@ -551,38 +565,38 @@ 'transfer_prover_start' and 'transfer_prover_end'. * Division on integers is bootstrapped directly from division on -naturals and uses generic numeral algorithm for computations. -Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes -former simprocs binary_int_div and binary_int_mod - -* Tightened specification of class semiring_no_zero_divisors. Slight +naturals and uses generic numeral algorithm for computations. Slight +INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former +simprocs binary_int_div and binary_int_mod + +* Tightened specification of class semiring_no_zero_divisors. Minor INCOMPATIBILITY. * Class algebraic_semidom introduces common algebraic notions of -integral (semi)domains, particularly units. Although -logically subsumed by fields, is is not a super class of these -in order not to burden fields with notions that are trivial there. - -* Class normalization_semidom specifies canonical representants -for equivalence classes of associated elements in an integral -(semi)domain. This formalizes associated elements as well. +integral (semi)domains, particularly units. Although logically subsumed +by fields, is is not a super class of these in order not to burden +fields with notions that are trivial there. + +* Class normalization_semidom specifies canonical representants for +equivalence classes of associated elements in an integral (semi)domain. +This formalizes associated elements as well. * Abstract specification of gcd/lcm operations in classes semiring_gcd, -semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute -and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc -and gcd_int.assoc by gcd.assoc. - -* Former constants Fields.divide (_ / _) and Divides.div (_ div _) -are logically unified to Rings.divide in syntactic type class -Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) -for field division is added later as abbreviation in class Fields.inverse. -INCOMPATIBILITY, instantiations must refer to Rings.divide rather -than the former separate constants, hence infix syntax (_ / _) is usually -not available during instantiation. - -* New cancellation simprocs for boolean algebras to cancel -complementary terms for sup and inf. For example, "sup x (sup y (- x))" -simplifies to "top". INCOMPATIBILITY. +semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute +and gcd_int.commute are subsumed by gcd.commute, as well as +gcd_nat.assoc and gcd_int.assoc by gcd.assoc. + +* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are +logically unified to Rings.divide in syntactic type class Rings.divide, +with infix syntax (_ div _). Infix syntax (_ / _) for field division is +added later as abbreviation in class Fields.inverse. INCOMPATIBILITY, +instantiations must refer to Rings.divide rather than the former +separate constants, hence infix syntax (_ / _) is usually not available +during instantiation. + +* New cancellation simprocs for boolean algebras to cancel complementary +terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to +"top". INCOMPATIBILITY. * Library/Multiset: - Renamed multiset inclusion operators: @@ -614,36 +628,27 @@ less_eq_multiset_def INCOMPATIBILITY -* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt -fixpoint theorem for increasing functions in chain-complete partial -orders. - -* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), -Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem, -Fundamental Theorem of Algebra. Ported from HOL Light - -* Multivariate_Analysis: Added topological concepts such as connected components, -homotopic paths and the inside or outside of a set. - -* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' -command. Minor INCOMPATIBILITY, use 'function' instead. - -* Inductive definitions ('inductive', 'coinductive', etc.) expose -low-level facts of the internal construction only if the option -"inductive_defs" is enabled. This refers to the internal predicate -definition and its monotonicity result. Rare INCOMPATIBILITY. - -* Recursive function definitions ('fun', 'function', 'partial_function') -expose low-level facts of the internal construction only if the option -"function_defs" is enabled. Rare INCOMPATIBILITY. +* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a. + +* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the +Bourbaki-Witt fixpoint theorem for increasing functions in +chain-complete partial orders. + +* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. +Minor INCOMPATIBILITY, use 'function' instead. + +* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= +complex path integrals), Cauchy's integral theorem, winding numbers and +Cauchy's integral formula, Liouville theorem, Fundamental Theorem of +Algebra. Ported from HOL Light + +* Multivariate_Analysis: Added topological concepts such as connected +components, homotopic paths and the inside or outside of a set. * Data_Structures: new and growing session of standard data structures. * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. -* Library/Omega_Words_Fun: Infinite words modeled as functions nat => -'a. - * HOL-Statespace: command 'statespace' uses mandatory qualifier for import of parent, as for general 'locale' expressions. INCOMPATIBILITY, remove '!' and add '?' as required. @@ -651,18 +656,19 @@ *** ML *** +* The following combinators for low-level profiling of the ML runtime +system are available: + + profile_time (*CPU time*) + profile_time_thread (*CPU time on this thread*) + profile_allocations (*overall heap allocations*) + +* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). + * Pretty printing of Poly/ML compiler output in Isabelle has been improved: proper treatment of break offsets and blocks with consistent breaks. -* Isar proof methods are based on a slightly more general type -context_tactic, which allows to change the proof context dynamically -(e.g. to update cases) and indicate explicit Seq.Error results. Former -METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are -provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. - -* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). - * The auxiliary module Pure/display.ML has been eliminated. Its elementary thm print operations are now in Pure/more_thm.ML and thus called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. @@ -698,18 +704,26 @@ tools, but can also cause INCOMPATIBILITY for tools that don't observe the proof context discipline. -* The following combinators for low-level profiling of the ML runtime -system are available: - - profile_time (*CPU time*) - profile_time_thread (*CPU time on this thread*) - profile_allocations (*overall heap allocations*) +* Isar proof methods are based on a slightly more general type +context_tactic, which allows to change the proof context dynamically +(e.g. to update cases) and indicate explicit Seq.Error results. Former +METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are +provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. *** System *** * Command-line tool "isabelle console" enables print mode "ASCII". +* Command-line tool "isabelle update_then" expands old Isar command +conflations: + + hence ~> then have + thus ~> then show + +This syntax is more orthogonal and improves readability and +maintainability of proofs. + * Global session timeout is multiplied by timeout_scale factor. This allows to adjust large-scale tests (e.g. AFP) to overall hardware performance. @@ -719,22 +733,6 @@ \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono -* Command-line tool "isabelle update_then" expands old Isar command -conflations: - - hence ~> then have - thus ~> then show - -This syntax is more orthogonal and improves readability and -maintainability of proofs. - -* Poly/ML default platform architecture may be changed from 32bit to -64bit via system option ML_system_64. A system restart (and rebuild) -is required after change. - -* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which -both allow larger heap space than former x86-cygwin. - * Java runtime environment for x86_64-windows allows to use larger heap space. @@ -757,6 +755,13 @@ * Heap images are 10-15% smaller due to less wasteful persistent theory content (using ML type theory_id instead of theory); +* Poly/ML default platform architecture may be changed from 32bit to +64bit via system option ML_system_64. A system restart (and rebuild) +is required after change. + +* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which +both allow larger heap space than former x86-cygwin. + New in Isabelle2015 (May 2015)