20 accordingly. |
32 accordingly. |
21 |
33 |
22 * Toplevel theorem statement 'proposition' is another alias for |
34 * Toplevel theorem statement 'proposition' is another alias for |
23 'theorem'. |
35 'theorem'. |
24 |
36 |
25 * Syntax for formal comments "-- text" now also supports the symbolic |
|
26 form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps |
|
27 to update old sources. |
|
28 |
|
29 * Former "xsymbols" syntax with Isabelle symbols is used by default, |
|
30 without any special print mode. Important ASCII replacement syntax |
|
31 remains available under print mode "ASCII", but less important syntax |
|
32 has been removed (see below). |
|
33 |
|
34 * Support for more arrow symbols, with rendering in LaTeX and |
|
35 Isabelle fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow> |
|
36 |
|
37 |
37 |
38 *** Prover IDE -- Isabelle/Scala/jEdit *** |
38 *** Prover IDE -- Isabelle/Scala/jEdit *** |
39 |
|
40 * Completion of symbols via prefix of \<name> or \<^name> or \name is |
|
41 always possible, independently of the language context. It is never |
|
42 implicit: a popup will show up unconditionally. |
|
43 |
|
44 * Additional abbreviations for syntactic completion may be specified in |
|
45 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. |
|
46 |
|
47 * Improved scheduling for urgent print tasks (e.g. command state output, |
|
48 interactive queries) wrt. long-running background tasks. |
|
49 |
39 |
50 * IDE support for the source-level debugger of Poly/ML, to work with |
40 * IDE support for the source-level debugger of Poly/ML, to work with |
51 Isabelle/ML and official Standard ML. Configuration option "ML_debugger" |
41 Isabelle/ML and official Standard ML. Configuration option "ML_debugger" |
52 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
42 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
53 'SML_file_no_debug' control compilation of sources with debugging |
43 'SML_file_no_debug' control compilation of sources with debugging |
54 information. The Debugger panel allows to set breakpoints (via context |
44 information. The Debugger panel allows to set breakpoints (via context |
55 menu), step through stopped threads, evaluate local ML expressions etc. |
45 menu), step through stopped threads, evaluate local ML expressions etc. |
56 At least one Debugger view needs to be active to have any effect on the |
46 At least one Debugger view needs to be active to have any effect on the |
57 running ML program. |
47 running ML program. |
58 |
48 |
59 * The main Isabelle executable is managed as single-instance Desktop |
|
60 application uniformly on all platforms: Linux, Windows, Mac OS X. |
|
61 |
|
62 * The State panel manages explicit proof state output, with dynamic |
49 * The State panel manages explicit proof state output, with dynamic |
63 auto-update according to cursor movement. Alternatively, the jEdit |
50 auto-update according to cursor movement. Alternatively, the jEdit |
64 action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
51 action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
65 update. |
52 update. |
66 |
53 |
78 situations. The text overview column takes over the role to indicate |
65 situations. The text overview column takes over the role to indicate |
79 unfinished edits in the PIDE pipeline. This avoids flashing text display |
66 unfinished edits in the PIDE pipeline. This avoids flashing text display |
80 due to ad-hoc updates by auxiliary GUI components, such as the State |
67 due to ad-hoc updates by auxiliary GUI components, such as the State |
81 panel. |
68 panel. |
82 |
69 |
|
70 * Improved scheduling for urgent print tasks (e.g. command state output, |
|
71 interactive queries) wrt. long-running background tasks. |
|
72 |
|
73 * Completion of symbols via prefix of \<name> or \<^name> or \name is |
|
74 always possible, independently of the language context. It is never |
|
75 implicit: a popup will show up unconditionally. |
|
76 |
|
77 * Additional abbreviations for syntactic completion may be specified in |
|
78 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with |
|
79 support for simple templates using ASCII 007 (bell) as placeholder. |
|
80 |
83 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
81 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
84 emphasized text style; the effect is visible in document output, not in |
82 emphasized text style; the effect is visible in document output, not in |
85 the editor. |
83 the editor. |
86 |
84 |
87 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, |
85 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, |
88 instead of former C+e LEFT. |
86 instead of former C+e LEFT. |
89 |
|
90 * New command-line tool "isabelle jedit_client" allows to connect to an |
|
91 already running Isabelle/jEdit process. This achieves the effect of |
|
92 single-instance applications seen on common GUI desktops. |
|
93 |
87 |
94 * The command-line tool "isabelle jedit" and the isabelle.Main |
88 * The command-line tool "isabelle jedit" and the isabelle.Main |
95 application wrapper threat the default $USER_HOME/Scratch.thy more |
89 application wrapper threat the default $USER_HOME/Scratch.thy more |
96 uniformly, and allow the dummy file argument ":" to open an empty buffer |
90 uniformly, and allow the dummy file argument ":" to open an empty buffer |
97 instead. |
91 instead. |
98 |
92 |
|
93 * New command-line tool "isabelle jedit_client" allows to connect to an |
|
94 already running Isabelle/jEdit process. This achieves the effect of |
|
95 single-instance applications seen on common GUI desktops. |
|
96 |
|
97 * The main Isabelle executable is managed as single-instance Desktop |
|
98 application uniformly on all platforms: Linux, Windows, Mac OS X. |
|
99 |
99 * The default look-and-feel for Linux is the traditional "Metal", which |
100 * The default look-and-feel for Linux is the traditional "Metal", which |
100 works better with GUI scaling for very high-resolution displays (e.g. |
101 works better with GUI scaling for very high-resolution displays (e.g. |
101 4K). Moreover, it is generally more robust than "Nimbus". |
102 4K). Moreover, it is generally more robust than "Nimbus". |
102 |
103 |
103 |
104 |
104 *** Document preparation *** |
105 *** Document preparation *** |
|
106 |
|
107 * Commands 'paragraph' and 'subparagraph' provide additional section |
|
108 headings. Thus there are 6 levels of standard headings, as in HTML. |
|
109 |
|
110 * Command 'text_raw' has been clarified: input text is processed as in |
|
111 'text' (with antiquotations and control symbols). The key difference is |
|
112 the lack of the surrounding isabelle markup environment in output. |
|
113 |
|
114 * Text is structured in paragraphs and nested lists, using notation that |
|
115 is similar to Markdown. The control symbols for list items are as |
|
116 follows: |
|
117 |
|
118 \<^item> itemize |
|
119 \<^enum> enumerate |
|
120 \<^descr> description |
105 |
121 |
106 * There is a new short form for antiquotations with a single argument |
122 * There is a new short form for antiquotations with a single argument |
107 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
123 that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
108 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
124 \<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
109 \<^name> without following cartouche is equivalent to @{name}. The |
125 \<^name> without following cartouche is equivalent to @{name}. The |
110 standard Isabelle fonts provide glyphs to render important control |
126 standard Isabelle fonts provide glyphs to render important control |
111 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
127 symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
112 |
128 |
113 * Antiquotation @{theory_text} prints uninterpreted theory source text |
|
114 (outer syntax with command keywords etc.). This may be used in the short |
|
115 form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". |
|
116 |
|
117 * @{verbatim [display]} supports option "indent". |
|
118 |
|
119 * Antiquotation @{doc ENTRY} provides a reference to the given |
|
120 documentation, with a hyperlink in the Prover IDE. |
|
121 |
|
122 * Antiquotations @{command}, @{method}, @{attribute} print checked |
|
123 entities of the Isar language. |
|
124 |
|
125 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
129 * Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
126 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
130 corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
127 standard LaTeX macros of the same names. |
131 standard LaTeX macros of the same names. |
128 |
132 |
129 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
133 * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
136 "source". The given text content is output unconditionally, without any |
140 "source". The given text content is output unconditionally, without any |
137 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the |
141 surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the |
138 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial |
142 argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial |
139 or terminal spaces are ignored. |
143 or terminal spaces are ignored. |
140 |
144 |
|
145 * Antiquotations @{emph} and @{bold} output LaTeX source recursively, |
|
146 adding appropriate text style markup. These may be used in the short |
|
147 form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
|
148 |
|
149 * Document antiquotation @{footnote} outputs LaTeX source recursively, |
|
150 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. |
|
151 |
|
152 * Antiquotation @{verbatim [display]} supports option "indent". |
|
153 |
|
154 * Antiquotation @{theory_text} prints uninterpreted theory source text |
|
155 (outer syntax with command keywords etc.). This may be used in the short |
|
156 form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". |
|
157 |
|
158 * Antiquotation @{doc ENTRY} provides a reference to the given |
|
159 documentation, with a hyperlink in the Prover IDE. |
|
160 |
|
161 * Antiquotations @{command}, @{method}, @{attribute} print checked |
|
162 entities of the Isar language. |
|
163 |
141 * HTML presentation uses the standard IsabelleText font and Unicode |
164 * HTML presentation uses the standard IsabelleText font and Unicode |
142 rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former |
165 rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former |
143 print mode "HTML" loses its special meaning. |
166 print mode "HTML" loses its special meaning. |
144 |
167 |
145 * Commands 'paragraph' and 'subparagraph' provide additional section |
|
146 headings. Thus there are 6 levels of standard headings, as in HTML. |
|
147 |
|
148 * Text is structured in paragraphs and nested lists, using notation that |
|
149 is similar to Markdown. The control symbols for list items are as |
|
150 follows: |
|
151 |
|
152 \<^item> itemize |
|
153 \<^enum> enumerate |
|
154 \<^descr> description |
|
155 |
|
156 * Command 'text_raw' has been clarified: input text is processed as in |
|
157 'text' (with antiquotations and control symbols). The key difference is |
|
158 the lack of the surrounding isabelle markup environment in output. |
|
159 |
|
160 * Document antiquotations @{emph} and @{bold} output LaTeX source |
|
161 recursively, adding appropriate text style markup. These may be used in |
|
162 the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
|
163 |
|
164 * Document antiquotation @{footnote} outputs LaTeX source recursively, |
|
165 marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. |
|
166 |
|
167 |
168 |
168 *** Isar *** |
169 *** Isar *** |
169 |
|
170 * Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
|
171 proof body as well, abstracted over relevant parameters. |
|
172 |
|
173 * Improved type-inference for theorem statement 'obtains': separate |
|
174 parameter scope for of each clause. |
|
175 |
|
176 * Term abbreviations via 'is' patterns also work for schematic |
|
177 statements: result is abstracted over unknowns. |
|
178 |
170 |
179 * Local goals ('have', 'show', 'hence', 'thus') allow structured |
171 * Local goals ('have', 'show', 'hence', 'thus') allow structured |
180 rule statements like fixes/assumes/shows in theorem specifications, but |
172 rule statements like fixes/assumes/shows in theorem specifications, but |
181 the notation is postfix with keywords 'if' (or 'when') and 'for'. For |
173 the notation is postfix with keywords 'if' (or 'when') and 'for'. For |
182 example: |
174 example: |
384 INCOMPATIBILITY in exotic situations. |
384 INCOMPATIBILITY in exotic situations. |
385 |
385 |
386 |
386 |
387 *** HOL *** |
387 *** HOL *** |
388 |
388 |
389 * Combinator to represent case distinction on products is named "case_prod", |
389 * The 'typedef' command has been upgraded from a partially checked |
390 uniformly, discontinuing any input aliasses. Very popular theorem aliasses |
390 "axiomatization", to a full definitional specification that takes the |
391 have been retained. |
391 global collection of overloaded constant / type definitions into |
|
392 account. Type definitions with open dependencies on overloaded |
|
393 definitions need to be specified as "typedef (overloaded)". This |
|
394 provides extra robustness in theory construction. Rare INCOMPATIBILITY. |
|
395 |
|
396 * Qualification of various formal entities in the libraries is done more |
|
397 uniformly via "context begin qualified definition ... end" instead of |
|
398 old-style "hide_const (open) ...". Consequently, both the defined |
|
399 constant and its defining fact become qualified, e.g. Option.is_none and |
|
400 Option.is_none_def. Occasional INCOMPATIBILITY in applications. |
|
401 |
|
402 * Some old and rarely used ASCII replacement syntax has been removed. |
|
403 INCOMPATIBILITY, standard syntax with symbols should be used instead. |
|
404 The subsequent commands help to reproduce the old forms, e.g. to |
|
405 simplify porting old theories: |
|
406 |
|
407 notation iff (infixr "<->" 25) |
|
408 |
|
409 notation Times (infixr "<*>" 80) |
|
410 |
|
411 type_notation Map.map (infixr "~=>" 0) |
|
412 notation Map.map_comp (infixl "o'_m" 55) |
|
413 |
|
414 type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) |
|
415 |
|
416 notation FuncSet.funcset (infixr "->" 60) |
|
417 notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) |
|
418 |
|
419 notation Omega_Words_Fun.conc (infixr "conc" 65) |
|
420 |
|
421 notation Preorder.equiv ("op ~~") |
|
422 and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
|
423 |
|
424 notation (in topological_space) tendsto (infixr "--->" 55) |
|
425 notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) |
|
426 notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
|
427 |
|
428 notation NSA.approx (infixl "@=" 50) |
|
429 notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) |
|
430 notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
|
431 |
|
432 * The alternative notation "\<Colon>" for type and sort constraints has been |
|
433 removed: in LaTeX document output it looks the same as "::". |
|
434 INCOMPATIBILITY, use plain "::" instead. |
|
435 |
|
436 * Commands 'inductive' and 'inductive_set' work better when names for |
|
437 intro rules are omitted: the "cases" and "induct" rules no longer |
|
438 declare empty case_names, but no case_names at all. This allows to use |
|
439 numbered cases in proofs, without requiring method "goal_cases". |
|
440 |
|
441 * Inductive definitions ('inductive', 'coinductive', etc.) expose |
|
442 low-level facts of the internal construction only if the option |
|
443 "inductive_defs" is enabled. This refers to the internal predicate |
|
444 definition and its monotonicity result. Rare INCOMPATIBILITY. |
|
445 |
|
446 * Recursive function definitions ('fun', 'function', 'partial_function') |
|
447 expose low-level facts of the internal construction only if the option |
|
448 "function_defs" is enabled. Rare INCOMPATIBILITY. |
|
449 |
|
450 * Combinator to represent case distinction on products is named |
|
451 "case_prod", uniformly, discontinuing any input aliasses. Very popular |
|
452 theorem aliasses have been retained. |
|
453 |
392 Consolidated facts: |
454 Consolidated facts: |
393 PairE ~> prod.exhaust |
455 PairE ~> prod.exhaust |
394 Pair_eq ~> prod.inject |
456 Pair_eq ~> prod.inject |
395 pair_collapse ~> prod.collapse |
457 pair_collapse ~> prod.collapse |
396 Pair_fst_snd_eq ~> prod_eq_iff |
458 Pair_fst_snd_eq ~> prod_eq_iff |
423 Eps_split ~> Eps_case_prod |
485 Eps_split ~> Eps_case_prod |
424 Eps_split_eq ~> Eps_case_prod_eq |
486 Eps_split_eq ~> Eps_case_prod_eq |
425 split_rsp ~> case_prod_rsp |
487 split_rsp ~> case_prod_rsp |
426 curry_split ~> curry_case_prod |
488 curry_split ~> curry_case_prod |
427 split_curry ~> case_prod_curry |
489 split_curry ~> case_prod_curry |
|
490 |
428 Changes in structure HOLogic: |
491 Changes in structure HOLogic: |
429 split_const ~> case_prod_const |
492 split_const ~> case_prod_const |
430 mk_split ~> mk_case_prod |
493 mk_split ~> mk_case_prod |
431 mk_psplits ~> mk_ptupleabs |
494 mk_psplits ~> mk_ptupleabs |
432 strip_psplits ~> strip_ptupleabs |
495 strip_psplits ~> strip_ptupleabs |
|
496 |
433 INCOMPATIBILITY. |
497 INCOMPATIBILITY. |
434 |
498 |
435 * Commands 'inductive' and 'inductive_set' work better when names for |
499 * The coercions to type 'real' have been reorganised. The function |
436 intro rules are omitted: the "cases" and "induct" rules no longer |
500 'real' is no longer overloaded, but has type 'nat => real' and |
437 declare empty case_names, but no case_names at all. This allows to use |
501 abbreviates of_nat for that type. Also 'real_of_int :: int => real' |
438 numbered cases in proofs, without requiring method "goal_cases". |
502 abbreviates of_int for that type. Other overloaded instances of 'real' |
439 |
503 have been replaced by 'real_of_ereal' and 'real_of_float'. |
440 * The 'typedef' command has been upgraded from a partially checked |
504 |
441 "axiomatization", to a full definitional specification that takes the |
|
442 global collection of overloaded constant / type definitions into |
|
443 account. Type definitions with open dependencies on overloaded |
|
444 definitions need to be specified as "typedef (overloaded)". This |
|
445 provides extra robustness in theory construction. Rare INCOMPATIBILITY. |
|
446 |
|
447 * Qualification of various formal entities in the libraries is done more |
|
448 uniformly via "context begin qualified definition ... end" instead of |
|
449 old-style "hide_const (open) ...". Consequently, both the defined |
|
450 constant and its defining fact become qualified, e.g. Option.is_none and |
|
451 Option.is_none_def. Occasional INCOMPATIBILITY in applications. |
|
452 |
|
453 * The coercions to type 'real' have been reorganised. The function 'real' |
|
454 is no longer overloaded, but has type 'nat => real' and abbreviates |
|
455 of_nat for that type. Also 'real_of_int :: int => real' abbreviates |
|
456 of_int for that type. Other overloaded instances of 'real' have been |
|
457 replaced by 'real_of_ereal' and 'real_of_float'. |
|
458 Consolidated facts (among others): |
505 Consolidated facts (among others): |
459 real_of_nat_le_iff -> of_nat_le_iff |
506 real_of_nat_le_iff -> of_nat_le_iff |
460 real_of_nat_numeral of_nat_numeral |
507 real_of_nat_numeral of_nat_numeral |
461 real_of_int_zero of_int_0 |
508 real_of_int_zero of_int_0 |
462 real_of_nat_zero of_nat_0 |
509 real_of_nat_zero of_nat_0 |
476 less_floor_eq less_floor_iff |
523 less_floor_eq less_floor_iff |
477 floor_less_eq floor_less_iff |
524 floor_less_eq floor_less_iff |
478 floor_divide_eq_div floor_divide_of_int_eq |
525 floor_divide_eq_div floor_divide_of_int_eq |
479 real_of_int_zero_cancel of_nat_eq_0_iff |
526 real_of_int_zero_cancel of_nat_eq_0_iff |
480 ceiling_real_of_int ceiling_of_int |
527 ceiling_real_of_int ceiling_of_int |
|
528 |
481 INCOMPATIBILITY. |
529 INCOMPATIBILITY. |
482 |
|
483 * Some old and rarely used ASCII replacement syntax has been removed. |
|
484 INCOMPATIBILITY, standard syntax with symbols should be used instead. |
|
485 The subsequent commands help to reproduce the old forms, e.g. to |
|
486 simplify porting old theories: |
|
487 |
|
488 notation iff (infixr "<->" 25) |
|
489 |
|
490 notation Times (infixr "<*>" 80) |
|
491 |
|
492 type_notation Map.map (infixr "~=>" 0) |
|
493 notation Map.map_comp (infixl "o'_m" 55) |
|
494 |
|
495 type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) |
|
496 |
|
497 notation FuncSet.funcset (infixr "->" 60) |
|
498 notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) |
|
499 |
|
500 notation Omega_Words_Fun.conc (infixr "conc" 65) |
|
501 |
|
502 notation Preorder.equiv ("op ~~") |
|
503 and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
|
504 |
|
505 notation (in topological_space) tendsto (infixr "--->" 55) |
|
506 notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) |
|
507 notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
|
508 |
|
509 notation NSA.approx (infixl "@=" 50) |
|
510 notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) |
|
511 notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
|
512 |
|
513 * The alternative notation "\<Colon>" for type and sort constraints has been |
|
514 removed: in LaTeX document output it looks the same as "::". |
|
515 INCOMPATIBILITY, use plain "::" instead. |
|
516 |
530 |
517 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has |
531 * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has |
518 been removed. INCOMPATIBILITY. |
532 been removed. INCOMPATIBILITY. |
519 |
533 |
520 * Quickcheck setup for finite sets. |
534 * Quickcheck setup for finite sets. |
549 - new methods for interactive debugging of 'transfer' and |
563 - new methods for interactive debugging of 'transfer' and |
550 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', |
564 'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', |
551 'transfer_prover_start' and 'transfer_prover_end'. |
565 'transfer_prover_start' and 'transfer_prover_end'. |
552 |
566 |
553 * Division on integers is bootstrapped directly from division on |
567 * Division on integers is bootstrapped directly from division on |
554 naturals and uses generic numeral algorithm for computations. |
568 naturals and uses generic numeral algorithm for computations. Slight |
555 Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes |
569 INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former |
556 former simprocs binary_int_div and binary_int_mod |
570 simprocs binary_int_div and binary_int_mod |
557 |
571 |
558 * Tightened specification of class semiring_no_zero_divisors. Slight |
572 * Tightened specification of class semiring_no_zero_divisors. Minor |
559 INCOMPATIBILITY. |
573 INCOMPATIBILITY. |
560 |
574 |
561 * Class algebraic_semidom introduces common algebraic notions of |
575 * Class algebraic_semidom introduces common algebraic notions of |
562 integral (semi)domains, particularly units. Although |
576 integral (semi)domains, particularly units. Although logically subsumed |
563 logically subsumed by fields, is is not a super class of these |
577 by fields, is is not a super class of these in order not to burden |
564 in order not to burden fields with notions that are trivial there. |
578 fields with notions that are trivial there. |
565 |
579 |
566 * Class normalization_semidom specifies canonical representants |
580 * Class normalization_semidom specifies canonical representants for |
567 for equivalence classes of associated elements in an integral |
581 equivalence classes of associated elements in an integral (semi)domain. |
568 (semi)domain. This formalizes associated elements as well. |
582 This formalizes associated elements as well. |
569 |
583 |
570 * Abstract specification of gcd/lcm operations in classes semiring_gcd, |
584 * Abstract specification of gcd/lcm operations in classes semiring_gcd, |
571 semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute |
585 semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute |
572 and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc |
586 and gcd_int.commute are subsumed by gcd.commute, as well as |
573 and gcd_int.assoc by gcd.assoc. |
587 gcd_nat.assoc and gcd_int.assoc by gcd.assoc. |
574 |
588 |
575 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) |
589 * Former constants Fields.divide (_ / _) and Divides.div (_ div _) are |
576 are logically unified to Rings.divide in syntactic type class |
590 logically unified to Rings.divide in syntactic type class Rings.divide, |
577 Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) |
591 with infix syntax (_ div _). Infix syntax (_ / _) for field division is |
578 for field division is added later as abbreviation in class Fields.inverse. |
592 added later as abbreviation in class Fields.inverse. INCOMPATIBILITY, |
579 INCOMPATIBILITY, instantiations must refer to Rings.divide rather |
593 instantiations must refer to Rings.divide rather than the former |
580 than the former separate constants, hence infix syntax (_ / _) is usually |
594 separate constants, hence infix syntax (_ / _) is usually not available |
581 not available during instantiation. |
595 during instantiation. |
582 |
596 |
583 * New cancellation simprocs for boolean algebras to cancel |
597 * New cancellation simprocs for boolean algebras to cancel complementary |
584 complementary terms for sup and inf. For example, "sup x (sup y (- x))" |
598 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to |
585 simplifies to "top". INCOMPATIBILITY. |
599 "top". INCOMPATIBILITY. |
586 |
600 |
587 * Library/Multiset: |
601 * Library/Multiset: |
588 - Renamed multiset inclusion operators: |
602 - Renamed multiset inclusion operators: |
589 < ~> <# |
603 < ~> <# |
590 \<subset> ~> \<subset># |
604 \<subset> ~> \<subset># |
612 - Removed lemmas generated by lift_definition: |
626 - Removed lemmas generated by lift_definition: |
613 less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer |
627 less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer |
614 less_eq_multiset_def |
628 less_eq_multiset_def |
615 INCOMPATIBILITY |
629 INCOMPATIBILITY |
616 |
630 |
617 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the Bourbaki-Witt |
631 * Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a. |
618 fixpoint theorem for increasing functions in chain-complete partial |
632 |
619 orders. |
633 * Library/Bourbaki_Witt_Fixpoint: Added formalisation of the |
620 |
634 Bourbaki-Witt fixpoint theorem for increasing functions in |
621 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals), |
635 chain-complete partial orders. |
622 Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem, |
636 |
623 Fundamental Theorem of Algebra. Ported from HOL Light |
637 * Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. |
624 |
638 Minor INCOMPATIBILITY, use 'function' instead. |
625 * Multivariate_Analysis: Added topological concepts such as connected components, |
639 |
626 homotopic paths and the inside or outside of a set. |
640 * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= |
627 |
641 complex path integrals), Cauchy's integral theorem, winding numbers and |
628 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
642 Cauchy's integral formula, Liouville theorem, Fundamental Theorem of |
629 command. Minor INCOMPATIBILITY, use 'function' instead. |
643 Algebra. Ported from HOL Light |
630 |
644 |
631 * Inductive definitions ('inductive', 'coinductive', etc.) expose |
645 * Multivariate_Analysis: Added topological concepts such as connected |
632 low-level facts of the internal construction only if the option |
646 components, homotopic paths and the inside or outside of a set. |
633 "inductive_defs" is enabled. This refers to the internal predicate |
|
634 definition and its monotonicity result. Rare INCOMPATIBILITY. |
|
635 |
|
636 * Recursive function definitions ('fun', 'function', 'partial_function') |
|
637 expose low-level facts of the internal construction only if the option |
|
638 "function_defs" is enabled. Rare INCOMPATIBILITY. |
|
639 |
647 |
640 * Data_Structures: new and growing session of standard data structures. |
648 * Data_Structures: new and growing session of standard data structures. |
641 |
649 |
642 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
650 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
643 |
|
644 * Library/Omega_Words_Fun: Infinite words modeled as functions nat => |
|
645 'a. |
|
646 |
651 |
647 * HOL-Statespace: command 'statespace' uses mandatory qualifier for |
652 * HOL-Statespace: command 'statespace' uses mandatory qualifier for |
648 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
653 import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
649 remove '!' and add '?' as required. |
654 remove '!' and add '?' as required. |
650 |
655 |
651 |
656 |
652 *** ML *** |
657 *** ML *** |
653 |
658 |
|
659 * The following combinators for low-level profiling of the ML runtime |
|
660 system are available: |
|
661 |
|
662 profile_time (*CPU time*) |
|
663 profile_time_thread (*CPU time on this thread*) |
|
664 profile_allocations (*overall heap allocations*) |
|
665 |
|
666 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
|
667 |
654 * Pretty printing of Poly/ML compiler output in Isabelle has been |
668 * Pretty printing of Poly/ML compiler output in Isabelle has been |
655 improved: proper treatment of break offsets and blocks with consistent |
669 improved: proper treatment of break offsets and blocks with consistent |
656 breaks. |
670 breaks. |
|
671 |
|
672 * The auxiliary module Pure/display.ML has been eliminated. Its |
|
673 elementary thm print operations are now in Pure/more_thm.ML and thus |
|
674 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. |
|
675 |
|
676 * Simproc programming interfaces have been simplified: |
|
677 Simplifier.make_simproc and Simplifier.define_simproc supersede various |
|
678 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
|
679 term patterns for the left-hand sides are specified with implicitly |
|
680 fixed variables, like top-level theorem statements. INCOMPATIBILITY. |
|
681 |
|
682 * Instantiation rules have been re-organized as follows: |
|
683 |
|
684 Thm.instantiate (*low-level instantiation with named arguments*) |
|
685 Thm.instantiate' (*version with positional arguments*) |
|
686 |
|
687 Drule.infer_instantiate (*instantiation with type inference*) |
|
688 Drule.infer_instantiate' (*version with positional arguments*) |
|
689 |
|
690 The LHS only requires variable specifications, instead of full terms. |
|
691 Old cterm_instantiate is superseded by infer_instantiate. |
|
692 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly. |
|
693 |
|
694 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been |
|
695 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. |
|
696 instead (with proper context). |
|
697 |
|
698 * Thm.instantiate (and derivatives) no longer require the LHS of the |
|
699 instantiation to be certified: plain variables are given directly. |
|
700 |
|
701 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
|
702 quasi-bound variables (like the Simplifier), instead of accidentally |
|
703 named local fixes. This has the potential to improve stability of proof |
|
704 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
|
705 the proof context discipline. |
657 |
706 |
658 * Isar proof methods are based on a slightly more general type |
707 * Isar proof methods are based on a slightly more general type |
659 context_tactic, which allows to change the proof context dynamically |
708 context_tactic, which allows to change the proof context dynamically |
660 (e.g. to update cases) and indicate explicit Seq.Error results. Former |
709 (e.g. to update cases) and indicate explicit Seq.Error results. Former |
661 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are |
710 METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are |
662 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. |
711 provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. |
663 |
712 |
664 * Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
|
665 |
|
666 * The auxiliary module Pure/display.ML has been eliminated. Its |
|
667 elementary thm print operations are now in Pure/more_thm.ML and thus |
|
668 called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. |
|
669 |
|
670 * Simproc programming interfaces have been simplified: |
|
671 Simplifier.make_simproc and Simplifier.define_simproc supersede various |
|
672 forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
|
673 term patterns for the left-hand sides are specified with implicitly |
|
674 fixed variables, like top-level theorem statements. INCOMPATIBILITY. |
|
675 |
|
676 * Instantiation rules have been re-organized as follows: |
|
677 |
|
678 Thm.instantiate (*low-level instantiation with named arguments*) |
|
679 Thm.instantiate' (*version with positional arguments*) |
|
680 |
|
681 Drule.infer_instantiate (*instantiation with type inference*) |
|
682 Drule.infer_instantiate' (*version with positional arguments*) |
|
683 |
|
684 The LHS only requires variable specifications, instead of full terms. |
|
685 Old cterm_instantiate is superseded by infer_instantiate. |
|
686 INCOMPATIBILITY, need to re-adjust some ML names and types accordingly. |
|
687 |
|
688 * Old tactic shorthands atac, rtac, etac, dtac, ftac have been |
|
689 discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. |
|
690 instead (with proper context). |
|
691 |
|
692 * Thm.instantiate (and derivatives) no longer require the LHS of the |
|
693 instantiation to be certified: plain variables are given directly. |
|
694 |
|
695 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
|
696 quasi-bound variables (like the Simplifier), instead of accidentally |
|
697 named local fixes. This has the potential to improve stability of proof |
|
698 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
|
699 the proof context discipline. |
|
700 |
|
701 * The following combinators for low-level profiling of the ML runtime |
|
702 system are available: |
|
703 |
|
704 profile_time (*CPU time*) |
|
705 profile_time_thread (*CPU time on this thread*) |
|
706 profile_allocations (*overall heap allocations*) |
|
707 |
|
708 |
713 |
709 *** System *** |
714 *** System *** |
710 |
715 |
711 * Command-line tool "isabelle console" enables print mode "ASCII". |
716 * Command-line tool "isabelle console" enables print mode "ASCII". |
|
717 |
|
718 * Command-line tool "isabelle update_then" expands old Isar command |
|
719 conflations: |
|
720 |
|
721 hence ~> then have |
|
722 thus ~> then show |
|
723 |
|
724 This syntax is more orthogonal and improves readability and |
|
725 maintainability of proofs. |
712 |
726 |
713 * Global session timeout is multiplied by timeout_scale factor. This |
727 * Global session timeout is multiplied by timeout_scale factor. This |
714 allows to adjust large-scale tests (e.g. AFP) to overall hardware |
728 allows to adjust large-scale tests (e.g. AFP) to overall hardware |
715 performance. |
729 performance. |
716 |
730 |
717 * Property values in etc/symbols may contain spaces, if written with the |
731 * Property values in etc/symbols may contain spaces, if written with the |
718 replacement character "␣" (Unicode point 0x2324). For example: |
732 replacement character "␣" (Unicode point 0x2324). For example: |
719 |
733 |
720 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
734 \<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
721 |
735 |
722 * Command-line tool "isabelle update_then" expands old Isar command |
736 * Java runtime environment for x86_64-windows allows to use larger heap |
723 conflations: |
737 space. |
724 |
738 |
725 hence ~> then have |
739 * Java runtime options are determined separately for 32bit vs. 64bit |
726 thus ~> then show |
740 platforms as follows. |
727 |
741 |
728 This syntax is more orthogonal and improves readability and |
742 - Isabelle desktop application: platform-specific files that are |
729 maintainability of proofs. |
743 associated with the main app bundle |
|
744 |
|
745 - isabelle jedit: settings |
|
746 JEDIT_JAVA_SYSTEM_OPTIONS |
|
747 JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64 |
|
748 |
|
749 - isabelle build: settings |
|
750 ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64 |
|
751 |
|
752 * Bash shell function "jvmpath" has been renamed to "platform_path": it |
|
753 is relevant both for Poly/ML and JVM processes. |
|
754 |
|
755 * Heap images are 10-15% smaller due to less wasteful persistent theory |
|
756 content (using ML type theory_id instead of theory); |
730 |
757 |
731 * Poly/ML default platform architecture may be changed from 32bit to |
758 * Poly/ML default platform architecture may be changed from 32bit to |
732 64bit via system option ML_system_64. A system restart (and rebuild) |
759 64bit via system option ML_system_64. A system restart (and rebuild) |
733 is required after change. |
760 is required after change. |
734 |
761 |
735 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which |
762 * Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which |
736 both allow larger heap space than former x86-cygwin. |
763 both allow larger heap space than former x86-cygwin. |
737 |
|
738 * Java runtime environment for x86_64-windows allows to use larger heap |
|
739 space. |
|
740 |
|
741 * Java runtime options are determined separately for 32bit vs. 64bit |
|
742 platforms as follows. |
|
743 |
|
744 - Isabelle desktop application: platform-specific files that are |
|
745 associated with the main app bundle |
|
746 |
|
747 - isabelle jedit: settings |
|
748 JEDIT_JAVA_SYSTEM_OPTIONS |
|
749 JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64 |
|
750 |
|
751 - isabelle build: settings |
|
752 ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64 |
|
753 |
|
754 * Bash shell function "jvmpath" has been renamed to "platform_path": it |
|
755 is relevant both for Poly/ML and JVM processes. |
|
756 |
|
757 * Heap images are 10-15% smaller due to less wasteful persistent theory |
|
758 content (using ML type theory_id instead of theory); |
|
759 |
764 |
760 |
765 |
761 |
766 |
762 New in Isabelle2015 (May 2015) |
767 New in Isabelle2015 (May 2015) |
763 ------------------------------ |
768 ------------------------------ |