author | wenzelm |
Wed, 20 Mar 2019 20:15:30 +0100 | |
changeset 69926 | 110fff287217 |
parent 69914 | 72301e1457b9 |
child 69960 | eff4ff8ba515 |
permissions | -rw-r--r-- |
57491 | 1 |
Isabelle NEWS -- history of user-relevant changes |
2 |
================================================= |
|
2553 | 3 |
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
62111
diff
changeset
|
4 |
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
60006 | 5 |
|
64603 | 6 |
|
68683 | 7 |
New in this Isabelle version |
8 |
---------------------------- |
|
9 |
||
69042 | 10 |
*** General *** |
11 |
||
69506 | 12 |
* Old-style {* verbatim *} tokens are explicitly marked as legacy |
13 |
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g. |
|
14 |
via "isabelle update_cartouches -t" (available since Isabelle2015). |
|
15 |
||
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
16 |
* The font family "Isabelle DejaVu" is systematically derived from the |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
17 |
existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
18 |
and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
19 |
The DejaVu base fonts are retricted to well-defined Unicode ranges and |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
20 |
augmented by special Isabelle symbols, taken from the former |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
21 |
"IsabelleText" font (which is no longer provided separately). The line |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
22 |
metrics and overall rendering quality is closer to original DejaVu. |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
23 |
INCOMPATIBILITY with display configuration expecting the old |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
24 |
"IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead. |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
25 |
|
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
26 |
* The Isabelle fonts render "\<inverse>" properly as superscript "-1". |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
27 |
|
69042 | 28 |
* Old-style inner comments (* ... *) within the term language are no |
29 |
longer supported (legacy feature in Isabelle2018). |
|
30 |
||
69066 | 31 |
* Infix operators that begin or end with a "*" can now be paranthesized |
32 |
without additional spaces, eg "(*)" instead of "( * )". |
|
33 |
||
69580 | 34 |
* Mixfix annotations may use cartouches instead of old-style double |
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset
|
35 |
quotes, e.g. (infixl \<open>+\<close> 60). The command-line tool "isabelle update -u |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset
|
36 |
mixfix_cartouches" allows to update existing theory sources |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset
|
37 |
automatically. |
69580 | 38 |
|
69216
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset
|
39 |
* ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset
|
40 |
need to provide a closed expression -- without trailing semicolon. Minor |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset
|
41 |
INCOMPATIBILITY. |
1a52baa70aed
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
wenzelm
parents:
69213
diff
changeset
|
42 |
|
69913 | 43 |
* Command keywords of kind thy_decl / thy_goal may be more specifically |
44 |
fit into the traditional document model of "definition-statement-proof" |
|
45 |
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. |
|
46 |
||
69042 | 47 |
|
69189 | 48 |
*** Isabelle/jEdit Prover IDE *** |
49 |
||
69780 | 50 |
* The jEdit File Browser is more prominent in the default GUI layout of |
51 |
Isabelle/jEdit: various virtual file-systems provide access to Isabelle |
|
52 |
resources, notably via "favorites:" (or "Edit Favorites"). |
|
53 |
||
69643 | 54 |
* Action "isabelle-export-browser" points the File Browser to the theory |
69764 | 55 |
exports of the current buffer, based on the "isabelle-export:" virtual |
56 |
file-system. The directory view needs to be reloaded manually to follow |
|
57 |
ongoing document processing. |
|
58 |
||
59 |
* Action "isabelle-session-browser" points the File Browser to session |
|
60 |
information, based on the "isabelle-session:" virtual file-system. Its |
|
61 |
entries are structured according to chapter / session names, the open |
|
62 |
operation is redirected to the session ROOT file. |
|
69643 | 63 |
|
69775
5a8ae7a4b7d0
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
wenzelm
parents:
69764
diff
changeset
|
64 |
* System option "jedit_text_overview" allows to disable the text |
5a8ae7a4b7d0
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
wenzelm
parents:
69764
diff
changeset
|
65 |
overview column. |
5a8ae7a4b7d0
added option jedit_text_overview for visual appearance (not performance, see also 72216713733a);
wenzelm
parents:
69764
diff
changeset
|
66 |
|
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
67 |
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle |
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
68 |
DejaVu" collection by default, which provides uniform rendering quality |
69377 | 69 |
with the usual Isabelle symbols. Line spacing no longer needs to be |
70 |
adjusted: properties for the old IsabelleText font had "Global Options / |
|
71 |
Text Area / Extra vertical line spacing (in pixels): -2", now it |
|
72 |
defaults to 0. |
|
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
73 |
|
69189 | 74 |
* Improved sub-pixel font rendering (especially on Linux), thanks to |
75 |
OpenJDK 11. |
|
76 |
||
69273 | 77 |
* Support for user-defined file-formats via class isabelle.File_Format |
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
78 |
in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
79 |
the shell function "isabelle_file_format" in etc/settings (e.g. of an |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
80 |
Isabelle component). |
69273 | 81 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
82 |
* Command-line options "-s" and "-u" of "isabelle jedit" override the |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
83 |
default for system option "system_heaps" that determines the heap |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
84 |
storage directory for "isabelle build". Option "-n" is now clearly |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
85 |
separated from option "-s". |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
86 |
|
69189 | 87 |
|
68879 | 88 |
*** Isar *** |
89 |
||
90 |
* More robust treatment of structural errors: begin/end blocks take |
|
91 |
precedence over goal/proof. |
|
92 |
||
69045 | 93 |
* Implicit cases goal1, goal2, goal3, etc. have been discontinued |
94 |
(legacy feature since Isabelle2016). |
|
95 |
||
96 |
||
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
97 |
*** HOL *** |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
98 |
|
69791
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69790
diff
changeset
|
99 |
* Formal Laurent series and overhaul of Formal power series |
69828 | 100 |
in session HOL-Computational_Algebra. |
101 |
||
102 |
* Exponentiation by squaring in session HOL-Library; used for computing |
|
103 |
powers in class monoid_mult and modular exponentiation in session |
|
104 |
HOL-Number_Theory. |
|
105 |
||
106 |
* More material on residue rings in session HOL-Number_Theory: |
|
107 |
Carmichael's function, primitive roots, more properties for "ord". |
|
108 |
||
109 |
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> |
|
69746
7404f5b91e56
changed precedence of big operators: now like any other function symbol
nipkow
parents:
69743
diff
changeset
|
110 |
(not the corresponding binding operators) now have the same precedence |
69828 | 111 |
as any other prefix function symbol. Minor INCOMPATIBILITY. |
69746
7404f5b91e56
changed precedence of big operators: now like any other function symbol
nipkow
parents:
69743
diff
changeset
|
112 |
|
69733 | 113 |
* Slightly more conventional naming schema in structure Inductive. |
114 |
Minor INCOMPATIBILITY. |
|
115 |
||
69829 | 116 |
* Various _global variants of specification tools have been removed. |
117 |
Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result] |
|
118 |
to lift specifications to the global theory level. |
|
119 |
||
69624 | 120 |
* Code generation: command 'export_code' without file keyword exports |
69649
e61b0b819d28
information with hyperlink to "isabelle-export:";
wenzelm
parents:
69643
diff
changeset
|
121 |
code as regular theory export, which can be materialized using the |
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
122 |
command-line tools "isabelle export" or "isabelle build -e" (with |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
123 |
'export_files' in the session ROOT), or browsed in Isabelle/jEdit via |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
124 |
the "isabelle-export:" file-system. To get generated code dumped into |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
125 |
output, use "file \<open>\<close>". Minor INCOMPATIBILITY. |
69624 | 126 |
|
69743 | 127 |
* Code generation for OCaml: proper strings are used for literals. |
128 |
Minor INCOMPATIBILITY. |
|
129 |
||
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
130 |
* Code generation for OCaml: Zarith supersedes Nums as library for |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
131 |
proper integer arithmetic. The library is located via standard |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
132 |
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable). |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
133 |
The environment provided by "isabelle ocaml_setup" already contains this |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
134 |
tool and the required packages. Minor INCOMPATIBILITY. |
69906
55534affe445
migrated from Nums to Zarith as library for OCaml integer arithmetic
haftmann
parents:
69903
diff
changeset
|
135 |
|
69690 | 136 |
* Code generation for Haskell: code includes for Haskell must contain |
137 |
proper module frame, nothing is added magically any longer. |
|
138 |
INCOMPATIBILITY. |
|
139 |
||
69697
4d95261fab5a
more conventional syntax for code_stmts antiquotation
haftmann
parents:
69690
diff
changeset
|
140 |
* Code generation: slightly more conventional syntax for |
4d95261fab5a
more conventional syntax for code_stmts antiquotation
haftmann
parents:
69690
diff
changeset
|
141 |
'code_stmts' antiquotation. Minor INCOMPATIBILITY. |
4d95261fab5a
more conventional syntax for code_stmts antiquotation
haftmann
parents:
69690
diff
changeset
|
142 |
|
69768 | 143 |
* The simplifier uses image_cong_simp as a congruence rule. The historic |
144 |
and not really well-formed congruence rules INF_cong*, SUP_cong*, |
|
145 |
are not used by default any longer. INCOMPATIBILITY; consider using |
|
146 |
declare image_cong_simp [cong del] in extreme situations. |
|
147 |
||
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69854
diff
changeset
|
148 |
* INF_image and SUP_image are no default simp rules any longer. |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69854
diff
changeset
|
149 |
INCOMPATIBILITY, prefer image_comp as simp rule if needed. |
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69854
diff
changeset
|
150 |
|
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
151 |
* Simplified syntax setup for big operators under image. In rare |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
152 |
situations, type conversions are not inserted implicitly any longer |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
153 |
and need to be given explicitly. Auxiliary abbreviations INFIMUM, |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
154 |
SUPREMUM, UNION, INTER should now rarely occur in output and are just |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
155 |
retained as migration auxiliary. INCOMPATIBILITY. |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
156 |
|
69094 | 157 |
* Theory List: the precedence of the list_update operator has changed: |
158 |
"f a [n := x]" now needs to be written "(f a)[n := x]". |
|
159 |
||
160 |
* Theory "HOL-Library.Multiset": the <Union># operator now has the same |
|
161 |
precedence as any other prefix function symbol. |
|
68848
8825efd1c2cf
updated URL to remote TPTP, following heads-up from Geoff Sutcliffe
blanchet
parents:
68824
diff
changeset
|
162 |
|
69316
248696d0a05f
Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
nipkow
parents:
69282
diff
changeset
|
163 |
* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead. |
248696d0a05f
Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.
nipkow
parents:
69282
diff
changeset
|
164 |
|
68938 | 165 |
* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap |
166 |
and prod_mset.swap, similarly to sum.swap and prod.swap. |
|
167 |
INCOMPATIBILITY. |
|
168 |
||
69164 | 169 |
* Strong congruence rules (with =simp=> in the premises) for constant f |
69546
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69506
diff
changeset
|
170 |
are now uniformly called f_cong_simp, in accordance with congruence |
27dae626822b
prefer naming convention from datatype package for strong congruence rules
haftmann
parents:
69506
diff
changeset
|
171 |
rules produced for mappers by the datatype package. INCOMPATIBILITY. |
69164 | 172 |
|
69707 | 173 |
* Sledgehammer: |
174 |
- The URL for SystemOnTPTP, which is used by remote provers, has |
|
175 |
been updated. |
|
176 |
- The machine-learning-based filter MaSh has been optimized to take |
|
177 |
less time (in most cases). |
|
69037 | 178 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69189
diff
changeset
|
179 |
* SMT: reconstruction is now possible using the SMT solver veriT. |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69189
diff
changeset
|
180 |
|
69568
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
181 |
* HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
182 |
and non-exhaustive patterns and handles arbitrarily nested patterns. |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
183 |
It uses on the same algorithm as HOL-Library.Code_Lazy, which assumes |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
184 |
sequential left-to-right pattern matching. The generated |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
185 |
equation no longer tuples the arguments on the right-hand side. |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
186 |
INCOMPATIBILITY. |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
187 |
|
69099
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
188 |
* Session HOL-SPARK: .prv files are no longer written to the |
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
189 |
file-system, but exported to the session database. Results may be |
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
190 |
retrieved with the "isabelle export" command-line tool like this: |
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
191 |
|
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
192 |
isabelle export -x "*:**.prv" HOL-SPARK-Examples |
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
193 |
|
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
194 |
|
68803 | 195 |
*** ML *** |
196 |
||
69708
1c201e4792cb
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
haftmann
parents:
69707
diff
changeset
|
197 |
* Local_Theory.reset is no longer available in user space. Regular |
1c201e4792cb
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
haftmann
parents:
69707
diff
changeset
|
198 |
definitional packages should use balanced blocks of |
1c201e4792cb
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
haftmann
parents:
69707
diff
changeset
|
199 |
Local_Theory.open_target versus Local_Theory.close_target instead, |
1c201e4792cb
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
haftmann
parents:
69707
diff
changeset
|
200 |
or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. |
1c201e4792cb
Local_Theory.reset only required for toplevel interaction, attempt to withhold it from user space
haftmann
parents:
69707
diff
changeset
|
201 |
|
68803 | 202 |
* Original PolyML.pointerEq is retained as a convenience for tools that |
203 |
don't use Isabelle/ML (where this is called "pointer_eq"). |
|
204 |
||
68824 | 205 |
* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |
206 |
option ML_environment to select a named environment, such as "Isabelle" |
|
207 |
for Isabelle/ML, or "SML" for official Standard ML. It is also possible |
|
208 |
to move toplevel bindings between environments, using a notation with |
|
209 |
">" as separator. For example: |
|
210 |
||
211 |
declare [[ML_environment = "Isabelle>SML"]] |
|
212 |
ML \<open>val println = writeln\<close> |
|
213 |
||
214 |
declare [[ML_environment = "SML"]] |
|
215 |
ML \<open>println "test"\<close> |
|
216 |
||
217 |
declare [[ML_environment = "Isabelle"]] |
|
218 |
ML \<open>println\<close> \<comment> \<open>not present\<close> |
|
219 |
||
220 |
The Isabelle/ML function ML_Env.setup defines new ML environments. This |
|
221 |
is useful to incorporate big SML projects in an isolated name space, and |
|
222 |
potentially with variations on ML syntax (existing ML_Env.SML_operations |
|
223 |
observes the official standard). |
|
68803 | 224 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
225 |
* ML antiquotation @{master_dir} refers to the master directory of the |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
226 |
underlying theory, i.e. the directory of the theory file. |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
227 |
|
69470 | 228 |
* ML antiquotation @{verbatim} inlines its argument as string literal, |
229 |
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly |
|
230 |
useful. |
|
231 |
||
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
232 |
* Command 'generate_file' allows to produce sources for other languages, |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
233 |
with antiquotations in the Isabelle context (only the control-cartouche |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
234 |
form). The default "cartouche" antiquotation evaluates an ML expression |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
235 |
of type string and inlines the result as a string literal of the target |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
236 |
language. For example, this works for Haskell as follows: |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
237 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
238 |
generate_file "Pure.hs" = \<open> |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
239 |
module Isabelle.Pure where |
69211
7062639cfdaa
added GHC.read_source: read Haskell source text with antiquotations;
wenzelm
parents:
69189
diff
changeset
|
240 |
allConst, impConst, eqConst :: String |
7062639cfdaa
added GHC.read_source: read Haskell source text with antiquotations;
wenzelm
parents:
69189
diff
changeset
|
241 |
allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> |
7062639cfdaa
added GHC.read_source: read Haskell source text with antiquotations;
wenzelm
parents:
69189
diff
changeset
|
242 |
impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> |
7062639cfdaa
added GHC.read_source: read Haskell source text with antiquotations;
wenzelm
parents:
69189
diff
changeset
|
243 |
eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> |
7062639cfdaa
added GHC.read_source: read Haskell source text with antiquotations;
wenzelm
parents:
69189
diff
changeset
|
244 |
\<close> |
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
245 |
|
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
246 |
The ML function Generate_File.generate writes all generated files from a |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
247 |
given theory to the file-system, e.g. a temporary directory where some |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
248 |
external compiler is applied. |
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
249 |
|
69282 | 250 |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
251 |
*** System *** |
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
252 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
253 |
* The system option "system_heaps" determines where to store the session |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
254 |
image of "isabelle build" (and other tools using that internally). |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
255 |
Former option "-s" is superseded by option "-o system_heaps". |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
256 |
INCOMPATIBILITY in command-line syntax. |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
257 |
|
69585 | 258 |
* The command-line tool "isabelle update" uses Isabelle/PIDE in |
259 |
batch-mode to update theory sources based on semantic markup produced in |
|
69609 | 260 |
Isabelle/ML. Actual updates depend on system options that may be enabled |
69588 | 261 |
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options |
262 |
section "Theory update". Theory sessions are specified as in "isabelle |
|
69585 | 263 |
dump". |
264 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
265 |
* The command-line tool "isabelle update -u control_cartouches" changes |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
266 |
antiquotations into control-symbol format (where possible): @{NAME} |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
267 |
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>. |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
268 |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
269 |
* Support for Isabelle command-line tools defined in Isabelle/Scala. |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
270 |
Instances of class Isabelle_Scala_Tools may be configured via the shell |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
271 |
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
272 |
component). |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
273 |
|
69230 | 274 |
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some |
275 |
source modules for Isabelle tools implemented in Haskell, notably for |
|
276 |
Isabelle/PIDE. |
|
277 |
||
69044 | 278 |
* Isabelle server command "use_theories" supports "nodes_status_delay" |
279 |
for continuous output of node status information. The time interval is |
|
280 |
specified in seconds; a negative value means it is disabled (default). |
|
281 |
||
282 |
* Isabelle Server command "use_theories" terminates more robustly in the |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
283 |
presence of structurally broken sources: full consolidation of theories |
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
284 |
is no longer required. |
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
285 |
|
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
286 |
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND, |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
287 |
which needs to point to a suitable version of "ocamlfind" (e.g. via |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
288 |
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
289 |
ISABELLE_OCAMLC are no longer supported. |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
290 |
|
69268
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
291 |
* Support for managed installations of Glasgow Haskell Compiler and |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
292 |
OCaml via the following command-line tools: |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
293 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
294 |
isabelle ghc_setup |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
295 |
isabelle ghc_stack |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
296 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
297 |
isabelle ocaml_setup |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
298 |
isabelle ocaml_opam |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
299 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
300 |
The global installation state is determined by the following settings |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
301 |
(and corresponding directory contents): |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
302 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
303 |
ISABELLE_STACK_ROOT |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
304 |
ISABELLE_STACK_RESOLVER |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
305 |
ISABELLE_GHC_VERSION |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
306 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
307 |
ISABELLE_OPAM_ROOT |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
308 |
ISABELLE_OCAML_VERSION |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
309 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
310 |
After setup, the following Isabelle settings are automatically |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
311 |
redirected (overriding existing user settings): |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
312 |
|
69269 | 313 |
ISABELLE_GHC |
314 |
||
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
315 |
ISABELLE_OCAMLFIND |
69268
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
316 |
|
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
317 |
The old meaning of these settings as locally installed executables may |
c1a27fce2076
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
wenzelm
parents:
69230
diff
changeset
|
318 |
be recovered by purging the directories ISABELLE_STACK_ROOT / |
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
319 |
ISABELLE_OPAM_ROOT, or by resetting these variables in |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
320 |
$ISABELLE_HOME_USER/etc/settings. |
69189 | 321 |
|
322 |
* Update to Java 11: the latest long-term support version of OpenJDK. |
|
69151 | 323 |
|
69755 | 324 |
* System option "checkpoint" has been discontinued: obsolete thanks to |
325 |
improved memory management in Poly/ML. |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
326 |
|
69903 | 327 |
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without |
328 |
the full overhead of 64-bit values everywhere. This special x86_64_32 |
|
329 |
mode provides up to 16GB ML heap, while program code and stacks are |
|
330 |
allocated elsewhere. Thus approx. 5 times more memory is available for |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
331 |
applications compared to old x86 mode (which is no longer used by |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
332 |
Isabelle). The switch to the x86_64 CPU architecture also avoids |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
333 |
compatibility problems with Linux and macOS, where 32-bit applications |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
334 |
are gradually phased out. |
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
335 |
|
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
336 |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
337 |
|
68391 | 338 |
New in Isabelle2018 (August 2018) |
339 |
--------------------------------- |
|
66651 | 340 |
|
66712 | 341 |
*** General *** |
342 |
||
68393 | 343 |
* Session-qualified theory names are mandatory: it is no longer possible |
344 |
to refer to unqualified theories from the parent session. |
|
345 |
INCOMPATIBILITY for old developments that have not been updated to |
|
346 |
Isabelle2017 yet (using the "isabelle imports" tool). |
|
347 |
||
348 |
* Only the most fundamental theory names are global, usually the entry |
|
349 |
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL, |
|
350 |
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for |
|
351 |
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". |
|
352 |
||
68558
7aae213d9e69
discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents:
68548
diff
changeset
|
353 |
* Global facts need to be closed: no free variables and no hypotheses. |
7aae213d9e69
discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents:
68548
diff
changeset
|
354 |
Rare INCOMPATIBILITY. |
68540 | 355 |
|
68661 | 356 |
* Facts stemming from locale interpretation are subject to lazy |
357 |
evaluation for improved performance. Rare INCOMPATIBILITY: errors |
|
358 |
stemming from interpretation morphisms might be deferred and thus |
|
359 |
difficult to locate; enable system option "strict_facts" temporarily to |
|
360 |
avoid this. |
|
361 |
||
67446 | 362 |
* Marginal comments need to be written exclusively in the new-style form |
363 |
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
|
364 |
supported. INCOMPATIBILITY, use the command-line tool "isabelle |
|
365 |
update_comments" to update existing theory files. |
|
366 |
||
67507 | 367 |
* Old-style inner comments (* ... *) within the term language are legacy |
368 |
and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>" |
|
369 |
instead. |
|
370 |
||
67402 | 371 |
* The "op <infix-op>" syntax for infix operators has been replaced by |
67400 | 372 |
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to |
373 |
be a space between the "*" and the corresponding parenthesis. |
|
68543 | 374 |
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to |
375 |
convert theory and ML files to the new syntax. Because it is based on |
|
376 |
regular expression matching, the result may need a bit of manual |
|
377 |
postprocessing. Invoking "isabelle update_op" converts all files in the |
|
378 |
current directory (recursively). In case you want to exclude conversion |
|
379 |
of ML files (because the tool frequently also converts ML's "op" |
|
380 |
syntax), use option "-m". |
|
67398 | 381 |
|
67013
335a7dce7cb3
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents:
66994
diff
changeset
|
382 |
* Theory header 'abbrevs' specifications need to be separated by 'and'. |
335a7dce7cb3
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents:
66994
diff
changeset
|
383 |
INCOMPATIBILITY. |
335a7dce7cb3
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents:
66994
diff
changeset
|
384 |
|
66757 | 385 |
* Command 'external_file' declares the formal dependency on the given |
386 |
file name, such that the Isabelle build process knows about it, but |
|
387 |
without specific Prover IDE management. |
|
388 |
||
66759 | 389 |
* Session ROOT entries no longer allow specification of 'files'. Rare |
390 |
INCOMPATIBILITY, use command 'external_file' within a proper theory |
|
391 |
context. |
|
392 |
||
66764
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
393 |
* Session root directories may be specified multiple times: each |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
394 |
accessible ROOT file is processed only once. This facilitates |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
395 |
specification of $ISABELLE_HOME_USER/ROOTS or command-line options like |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
396 |
-d or -D for "isabelle build" and "isabelle jedit". Example: |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
397 |
|
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
398 |
isabelle build -D '~~/src/ZF' |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
399 |
|
67263 | 400 |
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY, |
401 |
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead. |
|
402 |
||
68393 | 403 |
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit |
404 |
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen" |
|
405 |
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML |
|
406 |
output. |
|
67305
ecb74607063f
more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents:
67304
diff
changeset
|
407 |
|
66712 | 408 |
|
67261 | 409 |
*** Isabelle/jEdit Prover IDE *** |
66768 | 410 |
|
68393 | 411 |
* The command-line tool "isabelle jedit" provides more flexible options |
412 |
for session management: |
|
413 |
||
68472 | 414 |
- option -R builds an auxiliary logic image with all theories from |
415 |
other sessions that are not already present in its parent |
|
68393 | 416 |
|
417 |
- option -S is like -R, with a focus on the selected session and its |
|
418 |
descendants (this reduces startup time for big projects like AFP) |
|
419 |
||
68472 | 420 |
- option -A specifies an alternative ancestor session for options -R |
421 |
and -S |
|
422 |
||
68541 | 423 |
- option -i includes additional sessions into the name-space of |
424 |
theories |
|
425 |
||
68393 | 426 |
Examples: |
427 |
isabelle jedit -R HOL-Number_Theory |
|
428 |
isabelle jedit -R HOL-Number_Theory -A HOL |
|
429 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL |
|
430 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis |
|
68541 | 431 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL |
68393 | 432 |
|
433 |
* PIDE markup for session ROOT files: allows to complete session names, |
|
434 |
follow links to theories and document files etc. |
|
435 |
||
436 |
* Completion supports theory header imports, using theory base name. |
|
437 |
E.g. "Prob" may be completed to "HOL-Probability.Probability". |
|
438 |
||
439 |
* Named control symbols (without special Unicode rendering) are shown as |
|
440 |
bold-italic keyword. This is particularly useful for the short form of |
|
441 |
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action |
|
442 |
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1 |
|
443 |
arguments into this format. |
|
444 |
||
445 |
* Completion provides templates for named symbols with arguments, |
|
446 |
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>". |
|
447 |
||
68368 | 448 |
* Slightly more parallel checking, notably for high priority print |
449 |
functions (e.g. State output). |
|
450 |
||
68080 | 451 |
* The view title is set dynamically, according to the Isabelle |
452 |
distribution and the logic session name. The user can override this via |
|
453 |
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml). |
|
454 |
||
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67381
diff
changeset
|
455 |
* System options "spell_checker_include" and "spell_checker_exclude" |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67381
diff
changeset
|
456 |
supersede former "spell_checker_elements" to determine regions of text |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67381
diff
changeset
|
457 |
that are subject to spell-checking. Minor INCOMPATIBILITY. |
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67381
diff
changeset
|
458 |
|
67248
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67246
diff
changeset
|
459 |
* Action "isabelle.preview" is able to present more file formats, |
67266 | 460 |
notably bibtex database files and ML files. |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67224
diff
changeset
|
461 |
|
67262 | 462 |
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a |
68067 | 463 |
plain-text document draft. Both are available via the menu "Plugins / |
464 |
Isabelle". |
|
67262 | 465 |
|
67304
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
466 |
* When loading text files, the Isabelle symbols encoding UTF-8-Isabelle |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
467 |
is only used if there is no conflict with existing Unicode sequences in |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
468 |
the file. Otherwise, the fallback encoding is plain UTF-8 and Isabelle |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
469 |
symbols remain in literal \<symbol> form. This avoids accidental loss of |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
470 |
Unicode content when saving the file. |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
471 |
|
68545 | 472 |
* Bibtex database files (.bib) are semantically checked. |
473 |
||
67993 | 474 |
* Update to jedit-5.5.0, the latest release. |
475 |
||
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67224
diff
changeset
|
476 |
|
67261 | 477 |
*** Isabelle/VSCode Prover IDE *** |
478 |
||
479 |
* HTML preview of theories and other file-formats similar to |
|
480 |
Isabelle/jEdit. |
|
481 |
||
68690
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
482 |
* Command-line tool "isabelle vscode_server" accepts the same options |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
483 |
-A, -R, -S, -i for session selection as "isabelle jedit". This is |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
484 |
relevant for isabelle.args configuration settings in VSCode. The former |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
485 |
option -A (explore all known session files) has been discontinued: it is |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
486 |
enabled by default, unless option -S is used to focus on a particular |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
487 |
spot in the session structure. INCOMPATIBILITY. |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
488 |
|
66768 | 489 |
|
67140 | 490 |
*** Document preparation *** |
491 |
||
67448 | 492 |
* Formal comments work uniformly in outer syntax, inner syntax (term |
493 |
language), Isabelle/ML and some other embedded languages of Isabelle. |
|
494 |
See also "Document comments" in the isar-ref manual. The following forms |
|
495 |
are supported: |
|
496 |
||
497 |
- marginal text comment: \<comment> \<open>\<dots>\<close> |
|
498 |
- canceled source: \<^cancel>\<open>\<dots>\<close> |
|
499 |
- raw LaTeX: \<^latex>\<open>\<dots>\<close> |
|
67413 | 500 |
|
67381 | 501 |
* Outside of the inner theory body, the default presentation context is |
502 |
theory Pure. Thus elementary antiquotations may be used in markup |
|
503 |
commands (e.g. 'chapter', 'section', 'text') and formal comments. |
|
504 |
||
68513 | 505 |
* System option "document_tags" specifies alternative command tags. This |
506 |
is occasionally useful to control the global visibility of commands via |
|
507 |
session options (e.g. in ROOT). |
|
67140 | 508 |
|
509 |
* Document markup commands ('section', 'text' etc.) are implicitly |
|
510 |
tagged as "document" and visible by default. This avoids the application |
|
511 |
of option "document_tags" to these commands. |
|
512 |
||
67145 | 513 |
* Isabelle names are mangled into LaTeX macro names to allow the full |
514 |
identifier syntax with underscore, prime, digits. This is relevant for |
|
515 |
antiquotations in control symbol notation, e.g. \<^const_name> becomes |
|
516 |
\isactrlconstUNDERSCOREname. |
|
517 |
||
68393 | 518 |
* Document preparation with skip_proofs option now preserves the content |
519 |
more accurately: only terminal proof steps ('by' etc.) are skipped. |
|
67297
86a099f896fc
formal check of @{cite} bibtex entries -- only in batch-mode session builds;
wenzelm
parents:
67295
diff
changeset
|
520 |
|
68484 | 521 |
* Document antiquotation @{theory name} requires the long |
522 |
session-qualified theory name: this is what users reading the text |
|
523 |
normally need to import. |
|
524 |
||
67219 | 525 |
* Document antiquotation @{session name} checks and prints the given |
526 |
session name verbatim. |
|
527 |
||
68393 | 528 |
* Document antiquotation @{cite} now checks the given Bibtex entries |
529 |
against the Bibtex database files -- only in batch-mode session builds. |
|
67157 | 530 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67173
diff
changeset
|
531 |
* Command-line tool "isabelle document" has been re-implemented in |
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %-forms into main tex source;
wenzelm
parents:
67191
diff
changeset
|
532 |
Isabelle/Scala, with simplified arguments and explicit errors from the |
67203 | 533 |
latex and bibtex process. Minor INCOMPATIBILITY. |
67173 | 534 |
|
68393 | 535 |
* Session ROOT entry: empty 'document_files' means there is no document |
536 |
for this session. There is no need to specify options [document = false] |
|
537 |
anymore. |
|
538 |
||
67140 | 539 |
|
67702
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
540 |
*** Isar *** |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
541 |
|
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
542 |
* Command 'interpret' no longer exposes resulting theorems as literal |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
543 |
facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
544 |
improves modularity of proofs and scalability of locale interpretation. |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
545 |
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
546 |
(e.g. use 'find_theorems' or 'try' to figure this out). |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
547 |
|
68393 | 548 |
* The old 'def' command has been discontinued (legacy since |
549 |
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with |
|
550 |
object-logic equality or equivalence. |
|
551 |
||
68543 | 552 |
|
553 |
*** Pure *** |
|
554 |
||
555 |
* The inner syntax category "sort" now includes notation "_" for the |
|
556 |
dummy sort: it is effectively ignored in type-inference. |
|
557 |
||
67740 | 558 |
* Rewrites clauses (keyword 'rewrites') were moved into the locale |
68393 | 559 |
expression syntax, where they are part of locale instances. In |
560 |
interpretation commands rewrites clauses now need to occur before 'for' |
|
68469
aad109fde9ec
In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents:
68466
diff
changeset
|
561 |
and 'defines'. Rare INCOMPATIBILITY; definitions immediately subject to |
aad109fde9ec
In interpretation commands, clarify what to do with definitions immediately subject to rewriting.
ballarin
parents:
68466
diff
changeset
|
562 |
rewriting may need to be pulled up into the surrounding theory. |
68393 | 563 |
|
564 |
* For 'rewrites' clauses, if activating a locale instance fails, fall |
|
565 |
back to reading the clause first. This helps avoid qualification of |
|
67764 | 566 |
locale instances where the qualifier's sole purpose is avoiding |
567 |
duplicate constant declarations. |
|
67741
d5a7f2c54655
Fall back to reading rewrite morphism first if activation fails without it.
ballarin
parents:
67740
diff
changeset
|
568 |
|
68543 | 569 |
* Proof method "simp" now supports a new modifier "flip:" followed by a |
570 |
list of theorems. Each of these theorems is removed from the simpset |
|
571 |
(without warning if it is not there) and the symmetric version of the |
|
572 |
theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" |
|
573 |
and friends the modifier is "simp flip:". |
|
67718 | 574 |
|
575 |
||
66661 | 576 |
*** HOL *** |
577 |
||
68568 | 578 |
* Sledgehammer: bundled version of "vampire" (for non-commercial users) |
579 |
helps to avoid fragility of "remote_vampire" service. |
|
580 |
||
68028 | 581 |
* Clarified relationship of characters, strings and code generation: |
582 |
||
68393 | 583 |
- Type "char" is now a proper datatype of 8-bit values. |
584 |
||
585 |
- Conversions "nat_of_char" and "char_of_nat" are gone; use more |
|
586 |
general conversions "of_char" and "char_of" with suitable type |
|
587 |
constraints instead. |
|
588 |
||
589 |
- The zero character is just written "CHR 0x00", not "0" any longer. |
|
590 |
||
591 |
- Type "String.literal" (for code generation) is now isomorphic to |
|
592 |
lists of 7-bit (ASCII) values; concrete values can be written as |
|
593 |
"STR ''...''" for sequences of printable characters and "STR 0x..." |
|
594 |
for one single ASCII code point given as hexadecimal numeral. |
|
595 |
||
596 |
- Type "String.literal" supports concatenation "... + ..." for all |
|
597 |
standard target languages. |
|
598 |
||
599 |
- Theory HOL-Library.Code_Char is gone; study the explanations |
|
600 |
concerning "String.literal" in the tutorial on code generation to |
|
601 |
get an idea how target-language string literals can be converted to |
|
602 |
HOL string values and vice versa. |
|
603 |
||
604 |
- Session Imperative-HOL: operation "raise" directly takes a value of |
|
605 |
type "String.literal" as argument, not type "string". |
|
606 |
||
607 |
INCOMPATIBILITY. |
|
608 |
||
609 |
* Code generation: Code generation takes an explicit option |
|
610 |
"case_insensitive" to accomodate case-insensitive file systems. |
|
611 |
||
612 |
* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit. |
|
613 |
||
614 |
* New, more general, axiomatization of complete_distrib_lattice. The |
|
615 |
former axioms: |
|
616 |
||
617 |
"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" |
|
618 |
||
619 |
are replaced by: |
|
620 |
||
621 |
"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})" |
|
622 |
||
623 |
The instantiations of sets and functions as complete_distrib_lattice are |
|
624 |
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice |
|
625 |
operator. The dual of this property is also proved in theory |
|
626 |
HOL.Hilbert_Choice. |
|
67831
07f5588f2735
Removed stray 'sledgehammer' invocation
Manuel Eberl <eberlm@in.tum.de>
parents:
67830
diff
changeset
|
627 |
|
67999
1b05f74f2e5f
tidying up including contributions from Paulo EmÃlio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67993
diff
changeset
|
628 |
* New syntax for the minimum/maximum of a function over a finite set: |
68393 | 629 |
MIN x\<in>A. B and even MIN x. B (only useful for finite types), also MAX. |
67999
1b05f74f2e5f
tidying up including contributions from Paulo EmÃlio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67993
diff
changeset
|
630 |
|
67525
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
631 |
* Clarifed theorem names: |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
632 |
|
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
633 |
Min.antimono ~> Min.subset_imp |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
634 |
Max.antimono ~> Max.subset_imp |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
635 |
|
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
636 |
Minor INCOMPATIBILITY. |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
637 |
|
66661 | 638 |
* SMT module: |
68393 | 639 |
|
66661 | 640 |
- The 'smt_oracle' option is now necessary when using the 'smt' method |
66662 | 641 |
with a solver other than Z3. INCOMPATIBILITY. |
68393 | 642 |
|
66844 | 643 |
- The encoding to first-order logic is now more complete in the |
644 |
presence of higher-order quantifiers. An 'smt_explicit_application' |
|
645 |
option has been added to control this. INCOMPATIBILITY. |
|
646 |
||
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66803
diff
changeset
|
647 |
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to |
66844 | 648 |
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on |
649 |
interpretation of abstract locales. INCOMPATIBILITY. |
|
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66803
diff
changeset
|
650 |
|
68393 | 651 |
* Predicate coprime is now a real definition, not a mere abbreviation. |
652 |
INCOMPATIBILITY. |
|
653 |
||
66803 | 654 |
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead. |
655 |
INCOMPATIBILITY. |
|
656 |
||
68373 | 657 |
* The relator rel_filter on filters has been strengthened to its |
68393 | 658 |
canonical categorical definition with better properties. |
659 |
INCOMPATIBILITY. |
|
67616
1d005f514417
strengthen filter relator to canonical categorical definition with better properties
Andreas Lochbihler
parents:
67591
diff
changeset
|
660 |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67999
diff
changeset
|
661 |
* Generalized linear algebra involving linear, span, dependent, dim |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67999
diff
changeset
|
662 |
from type class real_vector to locales module and vector_space. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67999
diff
changeset
|
663 |
Renamed: |
68393 | 664 |
|
665 |
span_inc ~> span_superset |
|
666 |
span_superset ~> span_base |
|
667 |
span_eq ~> span_eq_iff |
|
668 |
||
669 |
INCOMPATIBILITY. |
|
66844 | 670 |
|
66937 | 671 |
* Class linordered_semiring_1 covers zero_less_one also, ruling out |
672 |
pathologic instances. Minor INCOMPATIBILITY. |
|
673 |
||
68393 | 674 |
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every |
675 |
element in a list to all following elements, not just the next one. |
|
676 |
||
677 |
* Theory HOL.List syntax: |
|
678 |
||
679 |
- filter-syntax "[x <- xs. P]" is no longer output syntax, but only |
|
680 |
input syntax |
|
681 |
||
682 |
- list comprehension syntax now supports tuple patterns in "pat <- xs" |
|
68249
949d93804740
First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents:
68246
diff
changeset
|
683 |
|
68450 | 684 |
* Theory Map: "empty" must now be qualified as "Map.empty". |
685 |
||
67051 | 686 |
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY. |
687 |
||
68100 | 688 |
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid |
689 |
clash with fact mod_mult_self4 (on more generic semirings). |
|
690 |
INCOMPATIBILITY. |
|
691 |
||
692 |
* Eliminated some theorem aliasses: |
|
693 |
even_times_iff ~> even_mult_iff |
|
694 |
mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1 |
|
695 |
even_of_nat ~> even_int_iff |
|
696 |
||
697 |
INCOMPATIBILITY. |
|
698 |
||
68157 | 699 |
* Eliminated some theorem duplicate variations: |
68393 | 700 |
|
701 |
- dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0 |
|
702 |
- mod_Suc_eq_Suc_mod can be replaced by mod_Suc |
|
703 |
- mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps |
|
704 |
- mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def |
|
705 |
- the witness of mod_eqD can be given directly as "_ div _" |
|
68157 | 706 |
|
707 |
INCOMPATIBILITY. |
|
708 |
||
68260 | 709 |
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no |
68393 | 710 |
longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding |
711 |
"elim!: dvd" to classical proof methods in most situations restores |
|
712 |
broken proofs. |
|
713 |
||
714 |
* Theory HOL-Library.Conditional_Parametricity provides command |
|
715 |
'parametric_constant' for proving parametricity of non-recursive |
|
716 |
definitions. For constants that are not fully parametric the command |
|
717 |
will infer conditions on relations (e.g., bi_unique, bi_total, or type |
|
718 |
class conditions such as "respects 0") sufficient for parametricity. See |
|
719 |
theory HOL-ex.Conditional_Parametricity_Examples for some examples. |
|
720 |
||
721 |
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code |
|
722 |
generator to generate code for algebraic types with lazy evaluation |
|
68639 | 723 |
semantics even in call-by-value target languages. See the theories |
68647 | 724 |
HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some |
725 |
examples. |
|
68393 | 726 |
|
727 |
* Theory HOL-Library.Landau_Symbols has been moved here from AFP. |
|
728 |
||
729 |
* Theory HOL-Library.Old_Datatype no longer provides the legacy command |
|
730 |
'old_datatype'. INCOMPATIBILITY. |
|
731 |
||
732 |
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide |
|
733 |
instances of rat, real, complex as factorial rings etc. Import |
|
734 |
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. |
|
735 |
INCOMPATIBILITY. |
|
736 |
||
737 |
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new |
|
738 |
infix/prefix notation. |
|
739 |
||
68543 | 740 |
* Session HOL-Algebra: revamped with much new material. The set of |
741 |
isomorphisms between two groups is now denoted iso rather than iso_set. |
|
742 |
INCOMPATIBILITY. |
|
743 |
||
744 |
* Session HOL-Analysis: the Arg function now respects the same interval |
|
745 |
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi. |
|
68499
d4312962161a
Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents:
68484
diff
changeset
|
746 |
INCOMPATIBILITY. |
d4312962161a
Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents:
68484
diff
changeset
|
747 |
|
68548 | 748 |
* Session HOL-Analysis: the functions zorder, zer_poly, porder and |
749 |
pol_poly have been redefined. All related lemmas have been reworked. |
|
68531 | 750 |
INCOMPATIBILITY. |
751 |
||
68393 | 752 |
* Session HOL-Analysis: infinite products, Moebius functions, the |
753 |
Riemann mapping theorem, the Vitali covering theorem, |
|
754 |
change-of-variables results for integration and measures. |
|
68260 | 755 |
|
68647 | 756 |
* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics |
757 |
or real-valued functions (limits, "Big-O", etc.) automatically. |
|
68681 | 758 |
See also ~~/src/HOL/Real_Asymp/Manual for some documentation. |
68647 | 759 |
|
68545 | 760 |
* Session HOL-Types_To_Sets: more tool support (unoverload_type combines |
761 |
internalize_sorts and unoverload) and larger experimental application |
|
762 |
(type based linear algebra transferred to linear algebra on subspaces). |
|
68522
d9cbc1e8644d
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents:
68515
diff
changeset
|
763 |
|
66651 | 764 |
|
68116 | 765 |
*** ML *** |
766 |
||
767 |
* Operation Export.export emits theory exports (arbitrary blobs), which |
|
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
768 |
are stored persistently in the session build database. Command-line |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
769 |
tools "isabelle export" and "isabelle build -e" allow to materialize |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
770 |
exports in the physical file-system. |
68116 | 771 |
|
68276 | 772 |
* Command 'ML_export' exports ML toplevel bindings to the global |
773 |
bootstrap environment of the ML process. This allows ML evaluation |
|
774 |
without a formal theory context, e.g. in command-line tools like |
|
775 |
"isabelle process". |
|
776 |
||
68116 | 777 |
|
66729 | 778 |
*** System *** |
779 |
||
67088 | 780 |
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no |
781 |
longer supported. |
|
782 |
||
68393 | 783 |
* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform |
784 |
support has been discontinued. |
|
785 |
||
66906 | 786 |
* Java runtime is for x86_64 only. Corresponding Isabelle settings have |
787 |
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS, |
|
788 |
instead of former 32/64 variants. INCOMPATIBILITY. |
|
789 |
||
68003 | 790 |
* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be |
791 |
phased out due to unclear preference of 32bit vs. 64bit architecture. |
|
792 |
Explicit GNU bash expressions are now preferred, for example (with |
|
793 |
quotes): |
|
794 |
||
795 |
#Posix executables (Unix or Cygwin), with preference for 64bit |
|
796 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
|
797 |
||
798 |
#native Windows or Unix executables, with preference for 64bit |
|
799 |
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" |
|
800 |
||
801 |
#native Windows (32bit) or Unix executables (preference for 64bit) |
|
802 |
"${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}" |
|
803 |
||
66745 | 804 |
* Command-line tool "isabelle build" supports new options: |
805 |
- option -B NAME: include session NAME and all descendants |
|
806 |
- option -S: only observe changes of sources, not heap images |
|
66841 | 807 |
- option -f: forces a fresh build |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66729
diff
changeset
|
808 |
|
68734
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
809 |
* Command-line tool "isabelle build" options -c -x -B refer to |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
810 |
descendants wrt. the session parent or import graph. Subtle |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
811 |
INCOMPATIBILITY: options -c -x used to refer to the session parent graph |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
812 |
only. |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
813 |
|
66843 | 814 |
* Command-line tool "isabelle build" takes "condition" options with the |
815 |
corresponding environment values into account, when determining the |
|
816 |
up-to-date status of a session. |
|
817 |
||
68393 | 818 |
* The command-line tool "dump" dumps information from the cumulative |
819 |
PIDE session database: many sessions may be loaded into a given logic |
|
820 |
image, results from all loaded theories are written to the output |
|
821 |
directory. |
|
822 |
||
66851
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66844
diff
changeset
|
823 |
* Command-line tool "isabelle imports -I" also reports actual session |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66844
diff
changeset
|
824 |
imports. This helps to minimize the session dependency graph. |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66844
diff
changeset
|
825 |
|
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
826 |
* The command-line tool "export" and "isabelle build -e" (with |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
827 |
'export_files' in session ROOT entries) retrieve theory exports from the |
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69791
diff
changeset
|
828 |
session build database. |
68393 | 829 |
|
830 |
* The command-line tools "isabelle server" and "isabelle client" provide |
|
831 |
access to the Isabelle Server: it supports responsive session management |
|
832 |
and concurrent use of theories, based on Isabelle/PIDE infrastructure. |
|
833 |
See also the "system" manual. |
|
834 |
||
835 |
* The command-line tool "isabelle update_comments" normalizes formal |
|
836 |
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to |
|
837 |
approximate the appearance in document output). This is more specific |
|
838 |
than former "isabelle update_cartouches -c": the latter tool option has |
|
839 |
been discontinued. |
|
840 |
||
841 |
* The command-line tool "isabelle mkroot" now always produces a document |
|
842 |
outline: its options have been adapted accordingly. INCOMPATIBILITY. |
|
843 |
||
844 |
* The command-line tool "isabelle mkroot -I" initializes a Mercurial |
|
845 |
repository for the generated session files. |
|
846 |
||
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
847 |
* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
848 |
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
849 |
mode") determine the directory locations of the main build artefacts -- |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
850 |
instead of hard-wired directories in ISABELLE_HOME_USER (or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
851 |
ISABELLE_HOME). |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
852 |
|
68393 | 853 |
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued: |
854 |
heap images and session databases are always stored in |
|
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
855 |
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
856 |
$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or |
68393 | 857 |
"isabelle jedit -s" or "isabelle build -s"). |
67099 | 858 |
|
67199 | 859 |
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific |
860 |
options for improved error reporting. Potential INCOMPATIBILITY with |
|
861 |
unusual LaTeX installations, may have to adapt these settings. |
|
862 |
||
68393 | 863 |
* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE |
864 |
markup for identifier bindings. It now uses The GNU Multiple Precision |
|
67591 | 865 |
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with |
866 |
32/64 bit. |
|
867 |
||
67099 | 868 |
|
66729 | 869 |
|
66472 | 870 |
New in Isabelle2017 (October 2017) |
871 |
---------------------------------- |
|
64439 | 872 |
|
64986 | 873 |
*** General *** |
874 |
||
66238 | 875 |
* Experimental support for Visual Studio Code (VSCode) as alternative |
876 |
Isabelle/PIDE front-end, see also |
|
66599 | 877 |
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017 |
66238 | 878 |
|
879 |
VSCode is a new type of application that continues the concepts of |
|
880 |
"programmer's editor" and "integrated development environment" towards |
|
881 |
fully semantic editing and debugging -- in a relatively light-weight |
|
882 |
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure. |
|
883 |
Technically, VSCode is based on the Electron application framework |
|
884 |
(Node.js + Chromium browser + V8), which is implemented in JavaScript |
|
885 |
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala |
|
886 |
modules around a Language Server implementation. |
|
887 |
||
65504 | 888 |
* Theory names are qualified by the session name that they belong to. |
66454 | 889 |
This affects imports, but not the theory name space prefix (which is |
890 |
just the theory base name as before). |
|
891 |
||
892 |
In order to import theories from other sessions, the ROOT file format |
|
893 |
provides a new 'sessions' keyword. In contrast, a theory that is |
|
894 |
imported in the old-fashioned manner via an explicit file-system path |
|
66472 | 895 |
belongs to the current session, and might cause theory name conflicts |
66454 | 896 |
later on. Theories that are imported from other sessions are excluded |
897 |
from the current session document. The command-line tool "isabelle |
|
898 |
imports" helps to update theory imports. |
|
899 |
||
65451 | 900 |
* The main theory entry points for some non-HOL sessions have changed, |
901 |
to avoid confusion with the global name "Main" of the session HOL. This |
|
902 |
leads to the follow renamings: |
|
903 |
||
904 |
CTT/Main.thy ~> CTT/CTT.thy |
|
905 |
ZF/Main.thy ~> ZF/ZF.thy |
|
906 |
ZF/Main_ZF.thy ~> ZF/ZF.thy |
|
907 |
ZF/Main_ZFC.thy ~> ZF/ZFC.thy |
|
908 |
ZF/ZF.thy ~> ZF/ZF_Base.thy |
|
909 |
||
910 |
INCOMPATIBILITY. |
|
911 |
||
66472 | 912 |
* Commands 'alias' and 'type_alias' introduce aliases for constants and |
913 |
type constructors, respectively. This allows adhoc changes to name-space |
|
914 |
accesses within global or local theory contexts, e.g. within a 'bundle'. |
|
915 |
||
64986 | 916 |
* Document antiquotations @{prf} and @{full_prf} output proof terms |
917 |
(again) in the same way as commands 'prf' and 'full_prf'. |
|
918 |
||
65055 | 919 |
* Computations generated by the code generator can be embedded directly |
920 |
into ML, alongside with @{code} antiquotations, using the following |
|
921 |
antiquotations: |
|
922 |
||
923 |
@{computation ... terms: ... datatypes: ...} : |
|
924 |
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a |
|
925 |
@{computation_conv ... terms: ... datatypes: ...} : |
|
926 |
(Proof.context -> 'ml -> conv) -> Proof.context -> conv |
|
65045
b69ef432438d
avoid Unicode that conflicts with Isabelle symbol rendering;
wenzelm
parents:
65042
diff
changeset
|
927 |
@{computation_check terms: ... datatypes: ...} : Proof.context -> conv |
65041 | 928 |
|
65055 | 929 |
See src/HOL/ex/Computations.thy, |
930 |
src/HOL/Decision_Procs/Commutative_Ring.thy and |
|
931 |
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the |
|
932 |
tutorial on code generation. |
|
65041 | 933 |
|
64986 | 934 |
|
64602 | 935 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
936 |
||
66472 | 937 |
* Session-qualified theory imports allow the Prover IDE to process |
938 |
arbitrary theory hierarchies independently of the underlying logic |
|
939 |
session image (e.g. option "isabelle jedit -l"), but the directory |
|
940 |
structure needs to be known in advance (e.g. option "isabelle jedit -d" |
|
941 |
or a line in the file $ISABELLE_HOME_USER/ROOTS). |
|
64602 | 942 |
|
64842 | 943 |
* The PIDE document model maintains file content independently of the |
944 |
status of jEdit editor buffers. Reloading jEdit buffers no longer causes |
|
945 |
changes of formal document content. Theory dependencies are always |
|
946 |
resolved internally, without the need for corresponding editor buffers. |
|
947 |
The system option "jedit_auto_load" has been discontinued: it is |
|
948 |
effectively always enabled. |
|
949 |
||
64867 | 950 |
* The Theories dockable provides a "Purge" button, in order to restrict |
951 |
the document model to theories that are required for open editor |
|
952 |
buffers. |
|
953 |
||
66424 | 954 |
* The Theories dockable indicates the overall status of checking of each |
955 |
entry. When all forked tasks of a theory are finished, the border is |
|
956 |
painted with thick lines; remaining errors in this situation are |
|
957 |
represented by a different border color. |
|
958 |
||
66472 | 959 |
* Automatic indentation is more careful to avoid redundant spaces in |
960 |
intermediate situations. Keywords are indented after input (via typed |
|
961 |
characters or completion); see also option "jedit_indent_input". |
|
962 |
||
963 |
* Action "isabelle.preview" opens an HTML preview of the current theory |
|
964 |
document in the default web browser. |
|
965 |
||
66574
e16b27bd3f76
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents:
66563
diff
changeset
|
966 |
* Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT |
e16b27bd3f76
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents:
66563
diff
changeset
|
967 |
entry of the specified logic session in the editor, while its parent is |
e16b27bd3f76
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents:
66563
diff
changeset
|
968 |
used for formal checking. |
66472 | 969 |
|
66462 | 970 |
* The main Isabelle/jEdit plugin may be restarted manually (using the |
971 |
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains |
|
972 |
enabled at all times. |
|
973 |
||
66472 | 974 |
* Update to current jedit-5.4.0. |
65329 | 975 |
|
64602 | 976 |
|
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
977 |
*** Pure *** |
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
978 |
|
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
979 |
* Deleting the last code equations for a particular function using |
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
980 |
[code del] results in function with no equations (runtime abort) rather |
66472 | 981 |
than an unimplemented function (generation time abort). Use explicit |
66665 | 982 |
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY. |
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
983 |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66298
diff
changeset
|
984 |
* Proper concept of code declarations in code.ML: |
66472 | 985 |
- Regular code declarations act only on the global theory level, being |
986 |
ignored with warnings if syntactically malformed. |
|
987 |
- Explicitly global code declarations yield errors if syntactically |
|
988 |
malformed. |
|
989 |
- Default code declarations are silently ignored if syntactically |
|
990 |
malformed. |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66298
diff
changeset
|
991 |
Minor INCOMPATIBILITY. |
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66298
diff
changeset
|
992 |
|
66472 | 993 |
* Clarified and standardized internal data bookkeeping of code |
994 |
declarations: history of serials allows to track potentially |
|
995 |
non-monotonous declarations appropriately. Minor INCOMPATIBILITY. |
|
66310
e8d2862ec203
simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping;
haftmann
parents:
66298
diff
changeset
|
996 |
|
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
997 |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
998 |
*** HOL *** |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
999 |
|
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
66599
diff
changeset
|
1000 |
* The Nunchaku model finder is now part of "Main". |
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
66599
diff
changeset
|
1001 |
|
66472 | 1002 |
* SMT module: |
1003 |
- A new option, 'smt_nat_as_int', has been added to translate 'nat' to |
|
1004 |
'int' and benefit from the SMT solver's theory reasoning. It is |
|
1005 |
disabled by default. |
|
1006 |
- The legacy module "src/HOL/Library/Old_SMT.thy" has been removed. |
|
1007 |
- Several small issues have been rectified in the 'smt' command. |
|
1008 |
||
1009 |
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer |
|
1010 |
generated for datatypes with type class annotations. As a result, the |
|
1011 |
tactic that derives it no longer fails on nested datatypes. Slight |
|
1012 |
INCOMPATIBILITY. |
|
66450
a8299195ed82
NEWS: Removed constant subseq; subsumed by strict_mono
eberlm <eberlm@in.tum.de>
parents:
66449
diff
changeset
|
1013 |
|
66345
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
66310
diff
changeset
|
1014 |
* Command and antiquotation "value" with modified default strategy: |
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
66310
diff
changeset
|
1015 |
terms without free variables are always evaluated using plain evaluation |
66472 | 1016 |
only, with no fallback on normalization by evaluation. Minor |
1017 |
INCOMPATIBILITY. |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65841
diff
changeset
|
1018 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65544
diff
changeset
|
1019 |
* Theories "GCD" and "Binomial" are already included in "Main" (instead |
65575 | 1020 |
of "Complex_Main"). |
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65544
diff
changeset
|
1021 |
|
65170
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1022 |
* Constant "surj" is a full input/output abbreviation (again). |
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1023 |
Minor INCOMPATIBILITY. |
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1024 |
|
64632 | 1025 |
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. |
1026 |
INCOMPATIBILITY. |
|
1027 |
||
66472 | 1028 |
* Renamed ii to imaginary_unit in order to free up ii as a variable |
1029 |
name. The syntax \<i> remains available. INCOMPATIBILITY. |
|
1030 |
||
1031 |
* Dropped abbreviations transP, antisymP, single_valuedP; use constants |
|
1032 |
transp, antisymp, single_valuedp instead. INCOMPATIBILITY. |
|
1033 |
||
1034 |
* Constant "subseq" in Topological_Spaces has been removed -- it is |
|
1035 |
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have |
|
1036 |
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc. |
|
1037 |
||
1038 |
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and |
|
1039 |
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY. |
|
1040 |
||
1041 |
* Theory List: new generic function "sorted_wrt". |
|
1042 |
||
1043 |
* Named theorems mod_simps covers various congruence rules concerning |
|
1044 |
mod, replacing former zmod_simps. INCOMPATIBILITY. |
|
64787 | 1045 |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1046 |
* Swapped orientation of congruence rules mod_add_left_eq, |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1047 |
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1048 |
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
66472 | 1049 |
mod_diff_eq. INCOMPATIBILITY. |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1050 |
|
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1051 |
* Generalized some facts: |
64876 | 1052 |
measure_induct_rule |
1053 |
measure_induct |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1054 |
zminus_zmod ~> mod_minus_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1055 |
zdiff_zmod_left ~> mod_diff_left_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1056 |
zdiff_zmod_right ~> mod_diff_right_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1057 |
zmod_eq_dvd_iff ~> mod_eq_dvd_iff |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1058 |
INCOMPATIBILITY. |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1059 |
|
66472 | 1060 |
* Algebraic type class hierarchy of euclidean (semi)rings in HOL: |
1061 |
euclidean_(semi)ring, euclidean_(semi)ring_cancel, |
|
1062 |
unique_euclidean_(semi)ring; instantiation requires provision of a |
|
1063 |
euclidean size. |
|
1064 |
||
1065 |
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked: |
|
1066 |
- Euclidean induction is available as rule eucl_induct. |
|
1067 |
- Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm, |
|
1068 |
Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow |
|
1069 |
easy instantiation of euclidean (semi)rings as GCD (semi)rings. |
|
1070 |
- Coefficients obtained by extended euclidean algorithm are |
|
1071 |
available as "bezout_coefficients". |
|
1072 |
INCOMPATIBILITY. |
|
1073 |
||
1074 |
* Theory "Number_Theory.Totient" introduces basic notions about Euler's |
|
1075 |
totient function previously hidden as solitary example in theory |
|
1076 |
Residues. Definition changed so that "totient 1 = 1" in agreement with |
|
1077 |
the literature. Minor INCOMPATIBILITY. |
|
1078 |
||
66542 | 1079 |
* New styles in theory "HOL-Library.LaTeXsugar": |
66541 | 1080 |
- "dummy_pats" for printing equations with "_" on the lhs; |
1081 |
- "eta_expand" for printing eta-expanded terms. |
|
1082 |
||
66472 | 1083 |
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has |
1084 |
been renamed to bij_swap_compose_bij. INCOMPATIBILITY. |
|
1085 |
||
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
1086 |
* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" |
66488
9d83e8fe3de3
HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents:
66481
diff
changeset
|
1087 |
filter for describing points x such that f(x) is in the filter F. |
9d83e8fe3de3
HOL-Library: going_to filter
Manuel Eberl <eberlm@in.tum.de>
parents:
66481
diff
changeset
|
1088 |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66474
diff
changeset
|
1089 |
* Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been |
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66474
diff
changeset
|
1090 |
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name |
66472 | 1091 |
space. INCOMPATIBILITY. |
1092 |
||
1093 |
* Theory "HOL-Library.FinFun" has been moved to AFP (again). |
|
1094 |
INCOMPATIBILITY. |
|
1095 |
||
1096 |
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII |
|
1097 |
replacement syntax has been removed. INCOMPATIBILITY, standard syntax |
|
1098 |
with symbols should be used instead. The subsequent commands help to |
|
1099 |
reproduce the old forms, e.g. to simplify porting old theories: |
|
1100 |
||
1101 |
syntax (ASCII) |
|
1102 |
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10) |
|
1103 |
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10) |
|
1104 |
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3) |
|
1105 |
||
1106 |
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of |
|
1107 |
multisets have been renamed: |
|
1108 |
||
1109 |
msetless_cancel_numerals ~> msetsubset_cancel |
|
1110 |
msetle_cancel_numerals ~> msetsubset_eq_cancel |
|
1111 |
||
1112 |
INCOMPATIBILITY. |
|
1113 |
||
66481
d35f7a9f92e2
output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents:
66480
diff
changeset
|
1114 |
* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax |
d35f7a9f92e2
output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents:
66480
diff
changeset
|
1115 |
for pattern aliases as known from Haskell, Scala and ML. |
65515 | 1116 |
|
66563 | 1117 |
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs. |
1118 |
||
64898 | 1119 |
* Session HOL-Analysis: more material involving arcs, paths, covering |
66650 | 1120 |
spaces, innessential maps, retracts, infinite products, simplicial |
1121 |
complexes. Baire Category theorem. Major results include the Jordan |
|
1122 |
Curve Theorem and the Great Picard Theorem. |
|
66472 | 1123 |
|
1124 |
* Session HOL-Algebra has been extended by additional lattice theory: |
|
1125 |
the Knaster-Tarski fixed point theorem and Galois Connections. |
|
1126 |
||
1127 |
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions |
|
1128 |
of squarefreeness, n-th powers, and prime powers. |
|
1129 |
||
1130 |
* Session "HOL-Computional_Algebra" covers many previously scattered |
|
1131 |
theories, notably Euclidean_Algorithm, Factorial_Ring, |
|
1132 |
Formal_Power_Series, Fraction_Field, Fundamental_Theorem_Algebra, |
|
1133 |
Normalized_Fraction, Polynomial_FPS, Polynomial, Primes. Minor |
|
1134 |
INCOMPATIBILITY. |
|
65027
2b8583507891
renaming multiset simprocs
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
64986
diff
changeset
|
1135 |
|
60331 | 1136 |
|
64844 | 1137 |
*** System *** |
1138 |
||
66474 | 1139 |
* Isabelle/Scala: the SQL module supports access to relational |
1140 |
databases, either as plain file (SQLite) or full-scale server |
|
1141 |
(PostgreSQL via local port or remote ssh connection). |
|
1142 |
||
1143 |
* Results of "isabelle build" are recorded as SQLite database (i.e. |
|
1144 |
"Application File Format" in the sense of |
|
1145 |
https://www.sqlite.org/appfileformat.html). This allows systematic |
|
1146 |
access via operations from module Sessions.Store in Isabelle/Scala. |
|
1147 |
||
66472 | 1148 |
* System option "parallel_proofs" is 1 by default (instead of more |
1149 |
aggressive 2). This requires less heap space and avoids burning parallel |
|
1150 |
CPU cycles, while full subproof parallelization is enabled for repeated |
|
1151 |
builds (according to parallel_subproofs_threshold). |
|
65072 | 1152 |
|
65448
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65417
diff
changeset
|
1153 |
* System option "record_proofs" allows to change the global |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65417
diff
changeset
|
1154 |
Proofterm.proofs variable for a session. Regular values are are 0, 1, 2; |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65417
diff
changeset
|
1155 |
a negative value means the current state in the ML heap image remains |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65417
diff
changeset
|
1156 |
unchanged. |
9bc3b57c1fa7
added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
wenzelm
parents:
65417
diff
changeset
|
1157 |
|
66472 | 1158 |
* Isabelle settings variable ISABELLE_SCALA_BUILD_OPTIONS has been |
1159 |
renamed to ISABELLE_SCALAC_OPTIONS. Rare INCOMPATIBILITY. |
|
1160 |
||
1161 |
* Isabelle settings variables ISABELLE_WINDOWS_PLATFORM, |
|
1162 |
ISABELLE_WINDOWS_PLATFORM32, ISABELLE_WINDOWS_PLATFORM64 indicate the |
|
1163 |
native Windows platform (independently of the Cygwin installation). This |
|
1164 |
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32, |
|
1165 |
ISABELLE_PLATFORM64. |
|
65557 | 1166 |
|
66786 | 1167 |
* Command-line tool "isabelle build_docker" builds a Docker image from |
1168 |
the Isabelle application bundle for Linux. See also |
|
1169 |
https://hub.docker.com/r/makarius/isabelle |
|
1170 |
||
66473 | 1171 |
* Command-line tool "isabelle vscode_server" provides a Language Server |
1172 |
Protocol implementation, e.g. for the Visual Studio Code editor. It |
|
1173 |
serves as example for alternative PIDE front-ends. |
|
1174 |
||
66472 | 1175 |
* Command-line tool "isabelle imports" helps to maintain theory imports |
66671 | 1176 |
wrt. session structure. Examples for the main Isabelle distribution: |
66472 | 1177 |
|
1178 |
isabelle imports -I -a |
|
1179 |
isabelle imports -U -a |
|
1180 |
isabelle imports -U -i -a |
|
1181 |
isabelle imports -M -a -d '~~/src/Benchmarks' |
|
1182 |
||
64844 | 1183 |
|
67099 | 1184 |
|
64072 | 1185 |
New in Isabelle2016-1 (December 2016) |
1186 |
------------------------------------- |
|
62216 | 1187 |
|
62440 | 1188 |
*** General *** |
1189 |
||
64390 | 1190 |
* Splitter in proof methods "simp", "auto" and friends: |
1191 |
- The syntax "split add" has been discontinued, use plain "split", |
|
1192 |
INCOMPATIBILITY. |
|
1193 |
- For situations with many conditional or case expressions, there is |
|
1194 |
an alternative splitting strategy that can be much faster. It is |
|
1195 |
selected by writing "split!" instead of "split". It applies safe |
|
1196 |
introduction and elimination rules after each split rule. As a |
|
1197 |
result the subgoal may be split into several subgoals. |
|
1198 |
||
63273 | 1199 |
* Command 'bundle' provides a local theory target to define a bundle |
1200 |
from the body of specification commands (such as 'declare', |
|
1201 |
'declaration', 'notation', 'lemmas', 'lemma'). For example: |
|
1202 |
||
1203 |
bundle foo |
|
1204 |
begin |
|
1205 |
declare a [simp] |
|
1206 |
declare b [intro] |
|
1207 |
end |
|
63272 | 1208 |
|
63282 | 1209 |
* Command 'unbundle' is like 'include', but works within a local theory |
1210 |
context. Unlike "context includes ... begin", the effect of 'unbundle' |
|
1211 |
on the target context persists, until different declarations are given. |
|
1212 |
||
63977 | 1213 |
* Simplified outer syntax: uniform category "name" includes long |
1214 |
identifiers. Former "xname" / "nameref" / "name reference" has been |
|
1215 |
discontinued. |
|
1216 |
||
1217 |
* Embedded content (e.g. the inner syntax of types, terms, props) may be |
|
1218 |
delimited uniformly via cartouches. This works better than old-fashioned |
|
1219 |
quotes when sub-languages are nested. |
|
1220 |
||
1221 |
* Mixfix annotations support general block properties, with syntax |
|
1222 |
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", |
|
1223 |
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent |
|
1224 |
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks |
|
1225 |
is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY. |
|
63650 | 1226 |
|
63383 | 1227 |
* Proof method "blast" is more robust wrt. corner cases of Pure |
1228 |
statements without object-logic judgment. |
|
1229 |
||
63624
994d1a1105ef
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
wenzelm
parents:
63610
diff
changeset
|
1230 |
* Commands 'prf' and 'full_prf' are somewhat more informative (again): |
63977 | 1231 |
proof terms are reconstructed and cleaned from administrative thm nodes. |
1232 |
||
1233 |
* Code generator: config option "code_timing" triggers measurements of |
|
1234 |
different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
|
1235 |
examples. |
|
1236 |
||
1237 |
* Code generator: implicits in Scala (stemming from type class |
|
1238 |
instances) are generated into companion object of corresponding type |
|
1239 |
class, to resolve some situations where ambiguities may occur. |
|
1240 |
||
64390 | 1241 |
* Solve direct: option "solve_direct_strict_warnings" gives explicit |
1242 |
warnings for lemma statements with trivial proofs. |
|
64013
048b7dbfdfa3
option to report results of solve_direct as explicit warnings
haftmann
parents:
63995
diff
changeset
|
1243 |
|
64602 | 1244 |
|
62904 | 1245 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
1246 |
||
64527 | 1247 |
* More aggressive flushing of machine-generated input, according to |
1248 |
system option editor_generated_input_delay (in addition to existing |
|
1249 |
editor_input_delay for regular user edits). This may affect overall PIDE |
|
1250 |
reactivity and CPU usage. |
|
1251 |
||
64390 | 1252 |
* Syntactic indentation according to Isabelle outer syntax. Action |
1253 |
"indent-lines" (shortcut C+i) indents the current line according to |
|
1254 |
command keywords and some command substructure. Action |
|
1255 |
"isabelle.newline" (shortcut ENTER) indents the old and the new line |
|
1256 |
according to command keywords only; see also option |
|
1257 |
"jedit_indent_newline". |
|
1258 |
||
1259 |
* Semantic indentation for unstructured proof scripts ('apply' etc.) via |
|
1260 |
number of subgoals. This requires information of ongoing document |
|
1261 |
processing and may thus lag behind, when the user is editing too |
|
1262 |
quickly; see also option "jedit_script_indent" and |
|
1263 |
"jedit_script_indent_limit". |
|
1264 |
||
1265 |
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' |
|
1266 |
are treated as delimiters for fold structure; 'begin' and 'end' |
|
1267 |
structure of theory specifications is treated as well. |
|
1268 |
||
1269 |
* Command 'proof' provides information about proof outline with cases, |
|
1270 |
e.g. for proof methods "cases", "induct", "goal_cases". |
|
1271 |
||
1272 |
* Completion templates for commands involving "begin ... end" blocks, |
|
1273 |
e.g. 'context', 'notepad'. |
|
1274 |
||
1275 |
* Sidekick parser "isabelle-context" shows nesting of context blocks |
|
1276 |
according to 'begin' and 'end' structure. |
|
1277 |
||
63977 | 1278 |
* Highlighting of entity def/ref positions wrt. cursor. |
1279 |
||
1280 |
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all |
|
64514 | 1281 |
occurrences of the formal entity at the caret position. This facilitates |
63977 | 1282 |
systematic renaming. |
1283 |
||
1284 |
* PIDE document markup works across multiple Isar commands, e.g. the |
|
1285 |
results established at the end of a proof are properly identified in the |
|
1286 |
theorem statement. |
|
1287 |
||
1288 |
* Cartouche abbreviations work both for " and ` to accomodate typical |
|
1289 |
situations where old ASCII notation may be updated. |
|
1290 |
||
63875 | 1291 |
* Dockable window "Symbols" also provides access to 'abbrevs' from the |
1292 |
outer syntax of the current theory buffer. This provides clickable |
|
1293 |
syntax templates, including entries with empty abbrevs name (which are |
|
1294 |
inaccessible via keyboard completion). |
|
1295 |
||
63022 | 1296 |
* IDE support for the Isabelle/Pure bootstrap process, with the |
1297 |
following independent stages: |
|
1298 |
||
1299 |
src/Pure/ROOT0.ML |
|
1300 |
src/Pure/ROOT.ML |
|
1301 |
src/Pure/Pure.thy |
|
1302 |
src/Pure/ML_Bootstrap.thy |
|
1303 |
||
1304 |
The ML ROOT files act like quasi-theories in the context of theory |
|
1305 |
ML_Bootstrap: this allows continuous checking of all loaded ML files. |
|
1306 |
The theory files are presented with a modified header to import Pure |
|
1307 |
from the running Isabelle instance. Results from changed versions of |
|
1308 |
each stage are *not* propagated to the next stage, and isolated from the |
|
1309 |
actual Isabelle/Pure that runs the IDE itself. The sequential |
|
63307 | 1310 |
dependencies of the above files are only observed for batch build. |
62904 | 1311 |
|
63977 | 1312 |
* Isabelle/ML and Standard ML files are presented in Sidekick with the |
1313 |
tree structure of section headings: this special comment format is |
|
1314 |
described in "implementation" chapter 0, e.g. (*** section ***). |
|
63461 | 1315 |
|
63581 | 1316 |
* Additional abbreviations for syntactic completion may be specified |
63871 | 1317 |
within the theory header as 'abbrevs'. The theory syntax for 'keywords' |
1318 |
has been simplified accordingly: optional abbrevs need to go into the |
|
1319 |
new 'abbrevs' section. |
|
1320 |
||
1321 |
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and |
|
1322 |
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor |
|
1323 |
INCOMPATIBILITY, use 'abbrevs' within theory header instead. |
|
63579 | 1324 |
|
64390 | 1325 |
* Action "isabelle.keymap-merge" asks the user to resolve pending |
1326 |
Isabelle keymap changes that are in conflict with the current jEdit |
|
1327 |
keymap; non-conflicting changes are always applied implicitly. This |
|
1328 |
action is automatically invoked on Isabelle/jEdit startup and thus |
|
1329 |
increases chances that users see new keyboard shortcuts when re-using |
|
1330 |
old keymaps. |
|
1331 |
||
63675 | 1332 |
* ML and document antiquotations for file-systems paths are more uniform |
1333 |
and diverse: |
|
1334 |
||
1335 |
@{path NAME} -- no file-system check |
|
1336 |
@{file NAME} -- check for plain file |
|
1337 |
@{dir NAME} -- check for directory |
|
1338 |
||
1339 |
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may |
|
1340 |
have to be changed. |
|
63669 | 1341 |
|
1342 |
||
63977 | 1343 |
*** Document preparation *** |
1344 |
||
1345 |
* New symbol \<circle>, e.g. for temporal operator. |
|
1346 |
||
64073 | 1347 |
* New document and ML antiquotation @{locale} for locales, similar to |
1348 |
existing antiquotation @{class}. |
|
1349 |
||
63977 | 1350 |
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> -- |
1351 |
this allows special forms of document output. |
|
1352 |
||
1353 |
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control |
|
1354 |
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its |
|
1355 |
derivatives. |
|
1356 |
||
1357 |
* \<^raw:...> symbols are no longer supported. |
|
1358 |
||
1359 |
* Old 'header' command is no longer supported (legacy since |
|
1360 |
Isabelle2015). |
|
1361 |
||
1362 |
||
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
1363 |
*** Isar *** |
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
1364 |
|
63180 | 1365 |
* Many specification elements support structured statements with 'if' / |
1366 |
'for' eigen-context, e.g. 'axiomatization', 'abbreviation', |
|
1367 |
'definition', 'inductive', 'function'. |
|
1368 |
||
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
1369 |
* Toplevel theorem statements support eigen-context notation with 'if' / |
63284 | 1370 |
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the |
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
1371 |
traditional long statement form (in prefix). Local premises are called |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
1372 |
"that" or "assms", respectively. Empty premises are *not* bound in the |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
1373 |
context: INCOMPATIBILITY. |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
1374 |
|
63039 | 1375 |
* Command 'define' introduces a local (non-polymorphic) definition, with |
1376 |
optional abstraction over local parameters. The syntax resembles |
|
63043 | 1377 |
'definition' and 'obtain'. It fits better into the Isar language than |
1378 |
old 'def', which is now a legacy feature. |
|
63039 | 1379 |
|
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
1380 |
* Command 'obtain' supports structured statements with 'if' / 'for' |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
1381 |
context. |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
1382 |
|
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
1383 |
* Command '\<proof>' is an alias for 'sorry', with different |
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
1384 |
typesetting. E.g. to produce proof holes in examples and documentation. |
62216 | 1385 |
|
63977 | 1386 |
* The defining position of a literal fact \<open>prop\<close> is maintained more |
1387 |
carefully, and made accessible as hyperlink in the Prover IDE. |
|
1388 |
||
1389 |
* Commands 'finally' and 'ultimately' used to expose the result as |
|
1390 |
literal fact: this accidental behaviour has been discontinued. Rare |
|
1391 |
INCOMPATIBILITY, use more explicit means to refer to facts in Isar. |
|
1392 |
||
1393 |
* Command 'axiomatization' has become more restrictive to correspond |
|
ec0fb01c6d50
misc tuning for re |