author | wenzelm |
Tue, 11 Feb 2020 17:03:14 +0100 | |
changeset 71438 | 22158ebde77f |
parent 71436 | 2e1b0ee920f5 |
child 71446 | 91340a6bf401 |
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 |
|
70265 | 7 |
New in this Isabelle version |
8 |
---------------------------- |
|
9 |
||
70562 | 10 |
*** General *** |
11 |
||
70677 | 12 |
* Session ROOT files need to specify explicit 'directories' for import |
70681 | 13 |
of theory files. Directories cannot be shared by different sessions. |
14 |
(Recall that import of theories from other sessions works via |
|
15 |
session-qualified theory names, together with suitable 'sessions' |
|
16 |
declarations in the ROOT.) |
|
70677 | 17 |
|
70562 | 18 |
* Internal derivations record dependencies on oracles and other theorems |
19 |
accurately, including the implicit type-class reasoning wrt. proven |
|
20 |
class relations and type arities. In particular, the formal tagging with |
|
21 |
"Pure.skip_proofs" of results stemming from "instance ... sorry" is now |
|
22 |
propagated properly to theorems depending on such type instances. |
|
23 |
||
24 |
* Command 'sorry' (oracle "Pure.skip_proofs") is more precise about the |
|
25 |
actual proposition that is assumed in the goal and proof context. This |
|
26 |
requires at least Proofterm.proofs = 1 to show up in theorem |
|
27 |
dependencies. |
|
28 |
||
29 |
* Command 'thm_oracles' prints all oracles used in given theorems, |
|
30 |
covering the full graph of transitive dependencies. |
|
31 |
||
70605 | 32 |
* Command 'thm_deps' prints immediate theorem dependencies of the given |
33 |
facts. The former graph visualization has been discontinued, because it |
|
34 |
was hardly usable. |
|
35 |
||
70562 | 36 |
|
70522 | 37 |
*** Isar *** |
38 |
||
39 |
* The proof method combinator (subproofs m) applies the method |
|
40 |
expression m consecutively to each subgoal, constructing individual |
|
41 |
subproofs internally. This impacts the internal construction of proof |
|
42 |
terms: it makes a cascade of let-expressions within the derivation tree |
|
43 |
and may thus improve scalability. |
|
44 |
||
71427 | 45 |
* Attribute "trace_locales" activates tracing of locale instances during |
46 |
roundup. It replaces the diagnostic command 'print_dependencies', which |
|
47 |
has been discontinued. |
|
70608 | 48 |
|
70522 | 49 |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
50 |
*** Isabelle/jEdit Prover IDE *** |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
51 |
|
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
52 |
* Prover IDE startup is now much faster, because theory dependencies are |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
53 |
no longer explored in advance. The overall session structure with its |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
54 |
declarations of 'directories' is sufficient to locate theory files. Thus |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
55 |
the "session focus" of option "isabelle jedit -S" has become obsolete |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
56 |
(likewise for "isabelle vscode_server -S"). Existing option "-R" is both |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
57 |
sufficient and more convenient to start editing a particular session. |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
58 |
|
71430 | 59 |
* Support more brackets: \<llangle> \<rrangle> (intended for implicit argument syntax). |
60 |
||
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70681
diff
changeset
|
61 |
|
70337
48609a6af1a0
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
70300
diff
changeset
|
62 |
*** HOL *** |
48609a6af1a0
removed relics of ASCII syntax for indexed big operators
haftmann
parents:
70300
diff
changeset
|
63 |
|
71427 | 64 |
* Improvements of the 'lift_bnf' command: |
71264 | 65 |
- Add support for quotient types. |
71427 | 66 |
- Generate transfer rules for the lifted map/set/rel/pred constants |
67 |
(theorems "<type>.<constant>_transfer_raw"). |
|
71264 | 68 |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
69 |
* Term_XML.Encode/Decode.term uses compact representation of Const |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
70 |
"typargs" from the given declaration environment. This also makes more |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
71 |
sense for translations to lambda-calculi with explicit polymorphism. |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
72 |
INCOMPATIBILITY, use Term_XML.Encode/Decode.term_raw in special |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
73 |
applications. |
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
74 |
|
70524 | 75 |
* ASCII membership syntax concerning big operators for infimum and |
71427 | 76 |
supremum has been discontinued. INCOMPATIBILITY. |
70524 | 77 |
|
78 |
* Clear distinction between types for bits (False / True) and Z2 (0 / |
|
71427 | 79 |
1): theory HOL-Library.Bit has been renamed accordingly. |
80 |
INCOMPATIBILITY. |
|
81 |
||
82 |
* Dynamic facts "algebra_split_simps" and "field_split_simps" correspond |
|
70817
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset
|
83 |
to algebra_simps and field_simps but contain more aggressive rules |
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset
|
84 |
potentially splitting goals; algebra_split_simps roughly replaces |
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset
|
85 |
sign_simps and field_split_simps can be used instead of divide_simps. |
dd675800469d
dedicated fact collections for algebraic simplification rules potentially splitting goals
haftmann
parents:
70784
diff
changeset
|
86 |
INCOMPATIBILITY. |
70524 | 87 |
|
71428 | 88 |
* Theory HOL.Complete_Lattices: |
89 |
renamed Inf_Sup -> Inf_eq_Sup and Sup_Inf -> Sup_eq_Inf |
|
90 |
||
71434 | 91 |
* Theory HOL-Library.Monad_Syntax: infix operation "bind" (\<bind>) |
70524 | 92 |
associates to the left now as is customary. |
93 |
||
71259
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset
|
94 |
* Theory HOL-Library.Ramsey: full finite Ramsey's theorem with |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset
|
95 |
multiple colours and arbitrary exponents. |
09aee7f5b447
Ramsey with multiple colours and arbitrary exponents
paulson <lp15@cam.ac.uk>
parents:
71166
diff
changeset
|
96 |
|
71147 | 97 |
* Session HOL-Analysis: proof method "metric" implements a decision |
98 |
procedure for simple linear statements in metric spaces. |
|
99 |
||
71438 | 100 |
* Session HOL-Word: bitwise NOT-operator has proper prefix syntax. Minor |
101 |
INCOMPATIBILITY. |
|
102 |
||
103 |
* Session HOL-Proofs: build faster thanks to better treatment of proof |
|
104 |
terms in Isabelle/Pure. |
|
71149 | 105 |
|
71150 | 106 |
|
70525 | 107 |
*** ML *** |
108 |
||
109 |
* Theory construction may be forked internally, the operation |
|
110 |
Theory.join_theory recovers a single result theory. See also the example |
|
111 |
in theory "HOL-ex.Join_Theory". |
|
112 |
||
70565 | 113 |
* Antiquotation @{oracle_name} inlines a formally checked oracle name. |
114 |
||
71436 | 115 |
* Minimal support for a soft-type system within the Isabelle logical |
116 |
framework (module Soft_Type_System). |
|
117 |
||
118 |
* Former Proof_Context.auto_fixes has been replaced by slightly more |
|
119 |
general Proof_Context.augment: it is subject to an optional soft-type |
|
120 |
system of the underlying object-logic. Minor INCOMPATIBILITY. |
|
121 |
||
71438 | 122 |
* More scalable Export.export using XML.tree to avoid premature string |
123 |
allocations, with convenient shortcut XML.blob. Minor INCOMPATIBILITY. |
|
124 |
||
70525 | 125 |
|
70599 | 126 |
*** System *** |
127 |
||
71433 | 128 |
* Standard rendering for more Isabelle symbols: \<llangle> \<rrangle> \<bbar> \<sqdot> |
129 |
||
71378
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset
|
130 |
* The command-line tool "isabelle scala_project" creates a Gradle |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset
|
131 |
project configuration for Isabelle/Scala/jEdit, to support Scala IDEs |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset
|
132 |
such as IntelliJ IDEA. |
820cf124dced
added "isabelle scala_project" to support e.g. IntelliJ IDEA;
wenzelm
parents:
71343
diff
changeset
|
133 |
|
71293 | 134 |
* The command-line tool "isabelle phabricator_setup" facilitates |
135 |
self-hosting of the Phabricator software-development platform, with |
|
136 |
support for Git, Mercurial, Subversion repositories. This helps to avoid |
|
137 |
monoculture and to escape the gravity of centralized version control by |
|
138 |
Github and/or Bitbucket. For further documentation, see chapter |
|
139 |
"Phabricator server administration" in the "system" manual. A notable |
|
140 |
example installation is https://isabelle-dev.sketis.net/. |
|
71134 | 141 |
|
71325 | 142 |
* The command-line tool "isabelle hg_setup" simplifies the setup of |
143 |
Mercurial repositories, with hosting via Phabricator or SSH file server |
|
144 |
access. |
|
145 |
||
70686
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset
|
146 |
* The command-line tool "isabelle imports" has been discontinued: strict |
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset
|
147 |
checking of session directories enforces session-qualified theory names |
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset
|
148 |
in applications -- users are responsible to specify session ROOT entries |
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset
|
149 |
properly. |
9cde8c4ea5a5
discontinued obsolete "isabelle imports" and all_known data;
wenzelm
parents:
70683
diff
changeset
|
150 |
|
71429 | 151 |
* The command-line tool "isabelle dump" and its underlying |
152 |
Isabelle/Scala module isabelle.Dump has become more scalable, by |
|
153 |
splitting sessions and supporting a base logic image. Minor |
|
154 |
INCOMPATIBILITY in options and parameters. |
|
155 |
||
71438 | 156 |
* Isabelle/Scala support for the Linux platform (Ubuntu): packages, |
157 |
users, system services. |
|
158 |
||
159 |
* Isabelle/Scala support for proof terms (with full type/term |
|
160 |
information) in module isabelle.Term. |
|
161 |
||
70599 | 162 |
* Theory export via Isabelle/Scala has been reworked. The former "fact" |
163 |
name space is now split into individual "thm" items: names are |
|
164 |
potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
|
165 |
"bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
|
166 |
exported as well: this spans an overall dependency graph of internal |
|
167 |
inferences; it might help to reconstruct the formal structure of theory |
|
168 |
libraries. See also the module Export_Theory in Isabelle/Scala. |
|
169 |
||
71428 | 170 |
* Old settings variables ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM |
171 |
have been discontinued -- deprecated since Isabelle2018. |
|
172 |
||
71438 | 173 |
* More complete x86_64 platform support on macOS, notably Catalina where |
174 |
old x86 has been discontinued. |
|
175 |
||
176 |
* Update to GHC stack 2.1.3 with stackage lts-13.19/ghc-8.6.4. |
|
177 |
||
178 |
* Update to OCaml Opam 2.0.6 (using ocaml 4.05.0 as before). |
|
179 |
||
70265 | 180 |
|
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70686
diff
changeset
|
181 |
|
70023 | 182 |
New in Isabelle2019 (June 2019) |
183 |
------------------------------- |
|
68683 | 184 |
|
69042 | 185 |
*** General *** |
186 |
||
70032 | 187 |
* The font collection "Isabelle DejaVu" is systematically derived from |
188 |
the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif" |
|
69343
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
"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
|
193 |
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
|
194 |
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
|
195 |
"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
|
196 |
|
395c4fb15ea2
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
wenzelm
parents:
69316
diff
changeset
|
197 |
* 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
|
198 |
|
69042 | 199 |
* Old-style inner comments (* ... *) within the term language are no |
200 |
longer supported (legacy feature in Isabelle2018). |
|
201 |
||
70023 | 202 |
* Old-style {* verbatim *} tokens are explicitly marked as legacy |
203 |
feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g. |
|
204 |
via "isabelle update_cartouches -t" (available since Isabelle2015). |
|
205 |
||
70297 | 206 |
* Infix operators that begin or end with a "*" are now parenthesized |
207 |
without additional spaces, e.g. "(*)" instead of "( * )". Minor |
|
70023 | 208 |
INCOMPATIBILITY. |
69066 | 209 |
|
69580 | 210 |
* Mixfix annotations may use cartouches instead of old-style double |
69586
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset
|
211 |
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
|
212 |
mixfix_cartouches" allows to update existing theory sources |
9171d1ce5a35
support for "isabelle update -u mixfix_cartouches";
wenzelm
parents:
69585
diff
changeset
|
213 |
automatically. |
69580 | 214 |
|
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
|
215 |
* 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
|
216 |
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
|
217 |
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
|
218 |
|
70057 | 219 |
* Commands 'generate_file', 'export_generated_files', and |
220 |
'compile_generated_files' support a stateless (PIDE-conformant) model |
|
221 |
for generated sources and compiled binaries of other languages. The |
|
70060 | 222 |
compilation process is managed in Isabelle/ML, and results exported to |
70057 | 223 |
the session database for further use (e.g. with "isabelle export" or |
224 |
"isabelle build -e"). |
|
225 |
||
69042 | 226 |
|
69189 | 227 |
*** Isabelle/jEdit Prover IDE *** |
228 |
||
70023 | 229 |
* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle |
230 |
DejaVu" collection by default, which provides uniform rendering quality |
|
231 |
with the usual Isabelle symbols. Line spacing no longer needs to be |
|
232 |
adjusted: properties for the old IsabelleText font had "Global Options / |
|
70069 | 233 |
Text Area / Extra vertical line spacing (in pixels): -2", it now |
234 |
defaults to 1, but 0 works as well. |
|
70023 | 235 |
|
69780 | 236 |
* The jEdit File Browser is more prominent in the default GUI layout of |
237 |
Isabelle/jEdit: various virtual file-systems provide access to Isabelle |
|
238 |
resources, notably via "favorites:" (or "Edit Favorites"). |
|
239 |
||
70061 | 240 |
* Further markup and rendering for "plain text" (e.g. informal prose) |
241 |
and "raw text" (e.g. verbatim sources). This improves the visual |
|
242 |
appearance of formal comments inside the term language, or in general |
|
243 |
for repeated alternation of formal and informal text. |
|
244 |
||
69643 | 245 |
* Action "isabelle-export-browser" points the File Browser to the theory |
69764 | 246 |
exports of the current buffer, based on the "isabelle-export:" virtual |
247 |
file-system. The directory view needs to be reloaded manually to follow |
|
248 |
ongoing document processing. |
|
249 |
||
250 |
* Action "isabelle-session-browser" points the File Browser to session |
|
251 |
information, based on the "isabelle-session:" virtual file-system. Its |
|
252 |
entries are structured according to chapter / session names, the open |
|
253 |
operation is redirected to the session ROOT file. |
|
69643 | 254 |
|
69273 | 255 |
* 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
|
256 |
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
|
257 |
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
|
258 |
Isabelle component). |
69273 | 259 |
|
70023 | 260 |
* System option "jedit_text_overview" allows to disable the text |
261 |
overview column. |
|
262 |
||
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
263 |
* 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
|
264 |
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
|
265 |
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
|
266 |
separated from option "-s". |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
267 |
|
70105 | 268 |
* The Isabelle/jEdit desktop application uses the same options as |
269 |
"isabelle jedit" for its internal "isabelle build" process: the implicit |
|
270 |
option "-o system_heaps" (or "-s") has been discontinued. This reduces |
|
271 |
the potential for surprise wrt. command-line tools. |
|
272 |
||
273 |
* The official download of the Isabelle/jEdit application already |
|
274 |
contains heap images for Isabelle/HOL within its main directory: thus |
|
275 |
the first encounter becomes faster and more robust (e.g. when run from a |
|
276 |
read-only directory). |
|
277 |
||
70072 | 278 |
* Isabelle DejaVu fonts are available with hinting by default, which is |
279 |
relevant for low-resolution displays. This may be disabled via system |
|
280 |
option "isabelle_fonts_hinted = false" in |
|
70075 | 281 |
$ISABELLE_HOME_USER/etc/preferences -- it occasionally yields better |
70072 | 282 |
results. |
283 |
||
70031 | 284 |
* OpenJDK 11 has quite different font rendering, with better glyph |
285 |
shapes and improved sub-pixel anti-aliasing. In some situations results |
|
70072 | 286 |
might be *worse* than Oracle Java 8, though -- a proper HiDPI / UHD |
287 |
display is recommended. |
|
70023 | 288 |
|
70258 | 289 |
* OpenJDK 11 supports GTK version 2.2 and 3 (according to system |
290 |
property jdk.gtk.version). The factory default is version 3, but |
|
291 |
ISABELLE_JAVA_SYSTEM_OPTIONS includes "-Djdk.gtk.version=2.2" to make |
|
292 |
this more conservative (as in Java 8). Depending on the GTK theme |
|
293 |
configuration, "-Djdk.gtk.version=3" might work better or worse. |
|
294 |
||
69189 | 295 |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
296 |
*** Document preparation *** |
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
297 |
|
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
298 |
* Document markers are formal comments of the form \<^marker>\<open>marker_body\<close> that |
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
299 |
are stripped from document output: the effect is to modify the semantic |
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
300 |
presentation context or to emit markup to the PIDE document. Some |
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
301 |
predefined markers are taken from the Dublin Core Metadata Initiative, |
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
302 |
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that |
70281 | 303 |
can be retrieved from the document database. |
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
304 |
|
70140 | 305 |
* Old-style command tags %name are re-interpreted as markers with |
306 |
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as |
|
307 |
before. Potential INCOMPATIBILITY: multiple markers are composed in |
|
308 |
canonical order, resulting in a reversed list of tags in the |
|
309 |
presentation context. |
|
310 |
||
311 |
* Marker \<^marker>\<open>tag name\<close> does not apply to the proof of a top-level goal |
|
312 |
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change |
|
313 |
of semantics wrt. old-style %name. |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
314 |
|
70143 | 315 |
* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>" |
316 |
template. |
|
317 |
||
70121 | 318 |
* Document antiquotation option "cartouche" indicates if the output |
319 |
should be delimited as cartouche; this takes precedence over the |
|
320 |
analogous option "quotes". |
|
321 |
||
70122
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
322 |
* Many document antiquotations are internally categorized as "embedded" |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
323 |
and expect one cartouche argument, which is typically used with the |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
324 |
\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
325 |
delimiters are stripped in output of the source (antiquotation option |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
326 |
"source"), but it is possible to enforce delimiters via option |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
327 |
"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}. |
a0b21b4b7a4a
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
wenzelm
parents:
70121
diff
changeset
|
328 |
|
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69960
diff
changeset
|
329 |
|
68879 | 330 |
*** Isar *** |
331 |
||
69045 | 332 |
* Implicit cases goal1, goal2, goal3, etc. have been discontinued |
333 |
(legacy feature since Isabelle2016). |
|
334 |
||
70023 | 335 |
* More robust treatment of structural errors: begin/end blocks take |
336 |
precedence over goal/proof. This is particularly relevant for the |
|
337 |
headless PIDE session and server. |
|
338 |
||
339 |
* Command keywords of kind thy_decl / thy_goal may be more specifically |
|
340 |
fit into the traditional document model of "definition-statement-proof" |
|
341 |
via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. |
|
342 |
||
69045 | 343 |
|
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
344 |
*** HOL *** |
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
345 |
|
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset
|
346 |
* Command 'export_code' produces output as logical files within the |
70011 | 347 |
theory context, as well as formal session exports that can be |
348 |
materialized via command-line tools "isabelle export" or "isabelle build |
|
349 |
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also |
|
350 |
provides a virtual file-system "isabelle-export:" that can be explored |
|
351 |
in the regular file-browser. A 'file_prefix' argument allows to specify |
|
352 |
an explicit name prefix for the target file (SML, OCaml, Scala) or |
|
353 |
directory (Haskell); the default is "export" with a consecutive number |
|
354 |
within each theory. |
|
70009
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset
|
355 |
|
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset
|
356 |
* Command 'export_code': the 'file' argument is now legacy and will be |
435fb018e8ee
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
wenzelm
parents:
69962
diff
changeset
|
357 |
removed soon: writing to the physical file-system is not well-defined in |
70011 | 358 |
a reactive/parallel application like Isabelle. The empty 'file' argument |
359 |
has been discontinued already: it is superseded by the file-browser in |
|
360 |
Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY. |
|
69624 | 361 |
|
70022
49e178cbf923
'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents:
70011
diff
changeset
|
362 |
* Command 'code_reflect' no longer supports the 'file' argument: it has |
49e178cbf923
'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents:
70011
diff
changeset
|
363 |
been superseded by 'file_prefix' for stateless file management as in |
49e178cbf923
'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents:
70011
diff
changeset
|
364 |
'export_code'. Minor INCOMPATIBILITY. |
49e178cbf923
'code_reflect' only supports new-style 'file_prefix';
wenzelm
parents:
70011
diff
changeset
|
365 |
|
69743 | 366 |
* Code generation for OCaml: proper strings are used for literals. |
367 |
Minor INCOMPATIBILITY. |
|
368 |
||
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
369 |
* Code generation for OCaml: Zarith supersedes Nums as library for |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
370 |
proper integer arithmetic. The library is located via standard |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
371 |
invocations of "ocamlfind" (via ISABELLE_OCAMLFIND settings variable). |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
372 |
The environment provided by "isabelle ocaml_setup" already contains this |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
373 |
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
|
374 |
|
69690 | 375 |
* Code generation for Haskell: code includes for Haskell must contain |
376 |
proper module frame, nothing is added magically any longer. |
|
377 |
INCOMPATIBILITY. |
|
378 |
||
70023 | 379 |
* Code generation: slightly more conventional syntax for 'code_stmts' |
380 |
antiquotation. Minor INCOMPATIBILITY. |
|
381 |
||
382 |
* Theory List: the precedence of the list_update operator has changed: |
|
383 |
"f a [n := x]" now needs to be written "(f a)[n := x]". |
|
384 |
||
385 |
* The functions \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (not the corresponding binding operators) |
|
386 |
now have the same precedence as any other prefix function symbol. Minor |
|
387 |
INCOMPATIBILITY. |
|
69861
62e47f06d22c
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
haftmann
parents:
69854
diff
changeset
|
388 |
|
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
389 |
* 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
|
390 |
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
|
391 |
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
|
392 |
SUPREMUM, UNION, INTER should now rarely occur in output and are just |
70237 | 393 |
retained as migration auxiliary. Abbreviations MINIMUM and MAXIMUM |
394 |
are gone INCOMPATIBILITY. |
|
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
395 |
|
70023 | 396 |
* The simplifier uses image_cong_simp as a congruence rule. The historic |
397 |
and not really well-formed congruence rules INF_cong*, SUP_cong*, are |
|
398 |
not used by default any longer. INCOMPATIBILITY; consider using declare |
|
399 |
image_cong_simp [cong del] in extreme situations. |
|
400 |
||
401 |
* INF_image and SUP_image are no default simp rules any longer. |
|
402 |
INCOMPATIBILITY, prefer image_comp as simp rule if needed. |
|
68938 | 403 |
|
69164 | 404 |
* 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
|
405 |
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
|
406 |
rules produced for mappers by the datatype package. INCOMPATIBILITY. |
69164 | 407 |
|
70023 | 408 |
* Retired lemma card_Union_image; use the simpler card_UN_disjoint |
409 |
instead. INCOMPATIBILITY. |
|
410 |
||
411 |
* Facts sum_mset.commute and prod_mset.commute have been renamed to |
|
412 |
sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap. |
|
413 |
INCOMPATIBILITY. |
|
414 |
||
415 |
* ML structure Inductive: slightly more conventional naming schema. |
|
416 |
Minor INCOMPATIBILITY. |
|
417 |
||
418 |
* ML: Various _global variants of specification tools have been removed. |
|
419 |
Minor INCOMPATIBILITY, prefer combinators |
|
420 |
Named_Target.theory_map[_result] to lift specifications to the global |
|
421 |
theory level. |
|
422 |
||
423 |
* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports |
|
424 |
overlapping and non-exhaustive patterns and handles arbitrarily nested |
|
425 |
patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which |
|
426 |
assumes sequential left-to-right pattern matching. The generated |
|
69568
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
427 |
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
|
428 |
INCOMPATIBILITY. |
de09a7261120
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
Andreas Lochbihler
parents:
69506
diff
changeset
|
429 |
|
70297 | 430 |
* Theory HOL-Library.Multiset: the \<Union># operator now has the same |
70023 | 431 |
precedence as any other prefix function symbol. |
432 |
||
70080 | 433 |
* Theory HOL-Library.Cardinal_Notations has been discontinued in favor |
70168 | 434 |
of the bundle cardinal_syntax (available in theory Main). Minor |
435 |
INCOMPATIBILITY. |
|
70080 | 436 |
|
70023 | 437 |
* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring, |
438 |
used for computing powers in class "monoid_mult" and modular |
|
439 |
exponentiation. |
|
440 |
||
441 |
* Session HOL-Computational_Algebra: Formal Laurent series and overhaul |
|
442 |
of Formal power series. |
|
443 |
||
444 |
* Session HOL-Number_Theory: More material on residue rings in |
|
445 |
Carmichael's function, primitive roots, more properties for "ord". |
|
446 |
||
70125
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset
|
447 |
* Session HOL-Analysis: Better organization and much more material |
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset
|
448 |
at the level of abstract topological spaces. |
b601c2c87076
type instantiations for poly_mapping as a real_normed_vector
paulson <lp15@cam.ac.uk>
parents:
70106
diff
changeset
|
449 |
|
70164
1f163f772da3
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
paulson <lp15@cam.ac.uk>
parents:
70143
diff
changeset
|
450 |
* Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light; |
70215
8371a25ca177
Algebraic closure: moving more theorems into their rightful places
paulson <lp15@cam.ac.uk>
parents:
70175
diff
changeset
|
451 |
algebraic closure of a field by de Vilhena and Baillon. |
70032 | 452 |
|
70168 | 453 |
* Session HOL-Homology has been added. It is a port of HOL Light's |
454 |
homology library, with new proofs of "invariance of domain" and related |
|
455 |
results. |
|
456 |
||
69099
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
457 |
* 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
|
458 |
file-system, but exported to the session database. Results may be |
70026 | 459 |
retrieved via "isabelle build -e HOL-SPARK-Examples" on the |
460 |
command-line. |
|
69099
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69094
diff
changeset
|
461 |
|
70023 | 462 |
* Sledgehammer: |
463 |
- The URL for SystemOnTPTP, which is used by remote provers, has been |
|
464 |
updated. |
|
465 |
- The machine-learning-based filter MaSh has been optimized to take |
|
466 |
less time (in most cases). |
|
467 |
||
468 |
* SMT: reconstruction is now possible using the SMT solver veriT. |
|
469 |
||
70174 | 470 |
* Session HOL-Word: |
471 |
* New theory More_Word as comprehensive entrance point. |
|
70175 | 472 |
* Merged type class bitss into type class bits. |
70174 | 473 |
INCOMPATIBILITY. |
474 |
||
68796
9ca183045102
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
haftmann
parents:
68770
diff
changeset
|
475 |
|
68803 | 476 |
*** ML *** |
477 |
||
70023 | 478 |
* Command 'generate_file' allows to produce sources for other languages, |
479 |
with antiquotations in the Isabelle context (only the control-cartouche |
|
480 |
form). The default "cartouche" antiquotation evaluates an ML expression |
|
481 |
of type string and inlines the result as a string literal of the target |
|
482 |
language. For example, this works for Haskell as follows: |
|
483 |
||
484 |
generate_file "Pure.hs" = \<open> |
|
485 |
module Isabelle.Pure where |
|
486 |
allConst, impConst, eqConst :: String |
|
487 |
allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close> |
|
488 |
impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close> |
|
489 |
eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close> |
|
490 |
\<close> |
|
491 |
||
70082
4f936de6d9b8
tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents:
70080
diff
changeset
|
492 |
See also commands 'export_generated_files' and 'compile_generated_files' |
4f936de6d9b8
tuned -- prefer Isar command 'compile_generated_files';
wenzelm
parents:
70080
diff
changeset
|
493 |
to use the results. |
68803 | 494 |
|
70260 | 495 |
* ML evaluation (notably via command 'ML' or 'ML_file') is subject to |
68824 | 496 |
option ML_environment to select a named environment, such as "Isabelle" |
70260 | 497 |
for Isabelle/ML, or "SML" for official Standard ML. |
68803 | 498 |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
499 |
* 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
|
500 |
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
|
501 |
|
69470 | 502 |
* ML antiquotation @{verbatim} inlines its argument as string literal, |
503 |
preserving newlines literally. The short form \<^verbatim>\<open>abc\<close> is particularly |
|
504 |
useful. |
|
505 |
||
70023 | 506 |
* Local_Theory.reset is no longer available in user space. Regular |
507 |
definitional packages should use balanced blocks of |
|
508 |
Local_Theory.open_target versus Local_Theory.close_target instead, or |
|
509 |
the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. |
|
510 |
||
511 |
* Original PolyML.pointerEq is retained as a convenience for tools that |
|
512 |
don't use Isabelle/ML (where this is called "pointer_eq"). |
|
69381
4c9b4e2c5460
more general command 'generate_file' for registered file types, notably Haskell;
wenzelm
parents:
69377
diff
changeset
|
513 |
|
69282 | 514 |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
515 |
*** System *** |
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
516 |
|
70031 | 517 |
* Update to OpenJDK 11: the current long-term support version of Java. |
70023 | 518 |
|
519 |
* Update to Poly/ML 5.8 allows to use the native x86_64 platform without |
|
520 |
the full overhead of 64-bit values everywhere. This special x86_64_32 |
|
521 |
mode provides up to 16GB ML heap, while program code and stacks are |
|
522 |
allocated elsewhere. Thus approx. 5 times more memory is available for |
|
523 |
applications compared to old x86 mode (which is no longer used by |
|
524 |
Isabelle). The switch to the x86_64 CPU architecture also avoids |
|
525 |
compatibility problems with Linux and macOS, where 32-bit applications |
|
526 |
are gradually phased out. |
|
527 |
||
528 |
* System option "checkpoint" has been discontinued: obsolete thanks to |
|
529 |
improved memory management in Poly/ML. |
|
530 |
||
531 |
* System option "system_heaps" determines where to store the session |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
532 |
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
|
533 |
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
|
534 |
INCOMPATIBILITY in command-line syntax. |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69829
diff
changeset
|
535 |
|
70023 | 536 |
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some |
537 |
source modules for Isabelle tools implemented in Haskell, notably for |
|
538 |
Isabelle/PIDE. |
|
539 |
||
540 |
* The command-line tool "isabelle build -e" retrieves theory exports |
|
541 |
from the session build database, using 'export_files' in session ROOT |
|
542 |
entries. |
|
543 |
||
69585 | 544 |
* The command-line tool "isabelle update" uses Isabelle/PIDE in |
545 |
batch-mode to update theory sources based on semantic markup produced in |
|
69609 | 546 |
Isabelle/ML. Actual updates depend on system options that may be enabled |
69588 | 547 |
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options |
548 |
section "Theory update". Theory sessions are specified as in "isabelle |
|
69585 | 549 |
dump". |
550 |
||
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
551 |
* The command-line tool "isabelle update -u control_cartouches" changes |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
552 |
antiquotations into control-symbol format (where possible): @{NAME} |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
553 |
becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>. |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69588
diff
changeset
|
554 |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
555 |
* 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
|
556 |
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
|
557 |
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
|
558 |
component). |
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
69273
diff
changeset
|
559 |
|
70023 | 560 |
* Isabelle Server command "use_theories" supports "nodes_status_delay" |
69044 | 561 |
for continuous output of node status information. The time interval is |
562 |
specified in seconds; a negative value means it is disabled (default). |
|
563 |
||
564 |
* 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
|
565 |
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
|
566 |
is no longer required. |
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
567 |
|
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
568 |
* OCaml tools and libraries are now accesed via ISABELLE_OCAMLFIND, |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
569 |
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
|
570 |
OPAM, see below). INCOMPATIBILITY: settings variables ISABELLE_OCAML and |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
571 |
ISABELLE_OCAMLC are no longer supported. |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
572 |
|
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
|
573 |
* 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
|
574 |
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
|
575 |
|
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
|
576 |
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
|
577 |
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
|
578 |
|
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
|
579 |
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
|
580 |
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
|
581 |
|
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
|
582 |
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
|
583 |
(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
|
584 |
|
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
|
585 |
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
|
586 |
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
|
587 |
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
|
588 |
|
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
|
589 |
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
|
590 |
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
|
591 |
|
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
|
592 |
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
|
593 |
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
|
594 |
|
69269 | 595 |
ISABELLE_GHC |
596 |
||
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
597 |
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
|
598 |
|
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
|
599 |
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
|
600 |
be recovered by purging the directories ISABELLE_STACK_ROOT / |
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
601 |
ISABELLE_OPAM_ROOT, or by resetting these variables in |
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69914
diff
changeset
|
602 |
$ISABELLE_HOME_USER/etc/settings. |
69189 | 603 |
|
69822
8c587dd44f51
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
wenzelm
parents:
69811
diff
changeset
|
604 |
|
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68879
diff
changeset
|
605 |
|
68391 | 606 |
New in Isabelle2018 (August 2018) |
607 |
--------------------------------- |
|
66651 | 608 |
|
66712 | 609 |
*** General *** |
610 |
||
68393 | 611 |
* Session-qualified theory names are mandatory: it is no longer possible |
612 |
to refer to unqualified theories from the parent session. |
|
613 |
INCOMPATIBILITY for old developments that have not been updated to |
|
614 |
Isabelle2017 yet (using the "isabelle imports" tool). |
|
615 |
||
616 |
* Only the most fundamental theory names are global, usually the entry |
|
617 |
points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL, |
|
618 |
FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for |
|
619 |
formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". |
|
620 |
||
68558
7aae213d9e69
discontinued pending_shyps: too much complication due to lazy facts;
wenzelm
parents:
68548
diff
changeset
|
621 |
* 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
|
622 |
Rare INCOMPATIBILITY. |
68540 | 623 |
|
68661 | 624 |
* Facts stemming from locale interpretation are subject to lazy |
625 |
evaluation for improved performance. Rare INCOMPATIBILITY: errors |
|
626 |
stemming from interpretation morphisms might be deferred and thus |
|
627 |
difficult to locate; enable system option "strict_facts" temporarily to |
|
628 |
avoid this. |
|
629 |
||
67446 | 630 |
* Marginal comments need to be written exclusively in the new-style form |
631 |
"\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
|
632 |
supported. INCOMPATIBILITY, use the command-line tool "isabelle |
|
633 |
update_comments" to update existing theory files. |
|
634 |
||
67507 | 635 |
* Old-style inner comments (* ... *) within the term language are legacy |
636 |
and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>" |
|
637 |
instead. |
|
638 |
||
67402 | 639 |
* The "op <infix-op>" syntax for infix operators has been replaced by |
67400 | 640 |
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to |
641 |
be a space between the "*" and the corresponding parenthesis. |
|
68543 | 642 |
INCOMPATIBILITY, use the command-line tool "isabelle update_op" to |
643 |
convert theory and ML files to the new syntax. Because it is based on |
|
644 |
regular expression matching, the result may need a bit of manual |
|
645 |
postprocessing. Invoking "isabelle update_op" converts all files in the |
|
646 |
current directory (recursively). In case you want to exclude conversion |
|
647 |
of ML files (because the tool frequently also converts ML's "op" |
|
648 |
syntax), use option "-m". |
|
67398 | 649 |
|
67013
335a7dce7cb3
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents:
66994
diff
changeset
|
650 |
* 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
|
651 |
INCOMPATIBILITY. |
335a7dce7cb3
more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
wenzelm
parents:
66994
diff
changeset
|
652 |
|
66757 | 653 |
* Command 'external_file' declares the formal dependency on the given |
654 |
file name, such that the Isabelle build process knows about it, but |
|
655 |
without specific Prover IDE management. |
|
656 |
||
66759 | 657 |
* Session ROOT entries no longer allow specification of 'files'. Rare |
658 |
INCOMPATIBILITY, use command 'external_file' within a proper theory |
|
659 |
context. |
|
660 |
||
66764
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
661 |
* 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
|
662 |
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
|
663 |
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
|
664 |
-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
|
665 |
|
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
666 |
isabelle build -D '~~/src/ZF' |
006deaf5c3dc
process ROOT files only once, which allows duplicate (or overlapping) session root directories;
wenzelm
parents:
66759
diff
changeset
|
667 |
|
67263 | 668 |
* The command 'display_drafts' has been discontinued. INCOMPATIBILITY, |
669 |
use action "isabelle.draft" (or "print") in Isabelle/jEdit instead. |
|
670 |
||
68393 | 671 |
* In HTML output, the Isabelle symbol "\<hyphen>" is rendered as explicit |
672 |
Unicode hyphen U+2010, to avoid unclear meaning of the old "soft hyphen" |
|
673 |
U+00AD. Rare INCOMPATIBILITY, e.g. copy-paste of historic Isabelle HTML |
|
674 |
output. |
|
67305
ecb74607063f
more robust hyphen (see also "Soft hyphen (SHY) – a hard problem?" http://jkorpela.fi/shy.html);
wenzelm
parents:
67304
diff
changeset
|
675 |
|
66712 | 676 |
|
67261 | 677 |
*** Isabelle/jEdit Prover IDE *** |
66768 | 678 |
|
68393 | 679 |
* The command-line tool "isabelle jedit" provides more flexible options |
680 |
for session management: |
|
681 |
||
68472 | 682 |
- option -R builds an auxiliary logic image with all theories from |
683 |
other sessions that are not already present in its parent |
|
68393 | 684 |
|
685 |
- option -S is like -R, with a focus on the selected session and its |
|
686 |
descendants (this reduces startup time for big projects like AFP) |
|
687 |
||
68472 | 688 |
- option -A specifies an alternative ancestor session for options -R |
689 |
and -S |
|
690 |
||
68541 | 691 |
- option -i includes additional sessions into the name-space of |
692 |
theories |
|
693 |
||
68393 | 694 |
Examples: |
695 |
isabelle jedit -R HOL-Number_Theory |
|
696 |
isabelle jedit -R HOL-Number_Theory -A HOL |
|
697 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL |
|
698 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis |
|
68541 | 699 |
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis -i CryptHOL |
68393 | 700 |
|
701 |
* PIDE markup for session ROOT files: allows to complete session names, |
|
702 |
follow links to theories and document files etc. |
|
703 |
||
704 |
* Completion supports theory header imports, using theory base name. |
|
705 |
E.g. "Prob" may be completed to "HOL-Probability.Probability". |
|
706 |
||
707 |
* Named control symbols (without special Unicode rendering) are shown as |
|
708 |
bold-italic keyword. This is particularly useful for the short form of |
|
709 |
antiquotations with control symbol: \<^name>\<open>argument\<close>. The action |
|
710 |
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1 |
|
711 |
arguments into this format. |
|
712 |
||
713 |
* Completion provides templates for named symbols with arguments, |
|
714 |
e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>". |
|
715 |
||
68368 | 716 |
* Slightly more parallel checking, notably for high priority print |
717 |
functions (e.g. State output). |
|
718 |
||
68080 | 719 |
* The view title is set dynamically, according to the Isabelle |
720 |
distribution and the logic session name. The user can override this via |
|
721 |
set-view-title (stored persistently in $JEDIT_SETTINGS/perspective.xml). |
|
722 |
||
67395
b39d596b77ce
more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents:
67381
diff
changeset
|
723 |
* 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
|
724 |
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
|
725 |
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
|
726 |
|
67248
68177abb2988
isabelle.preview presents bibtex database files as well;
wenzelm
parents:
67246
diff
changeset
|
727 |
* Action "isabelle.preview" is able to present more file formats, |
67266 | 728 |
notably bibtex database files and ML files. |
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67224
diff
changeset
|
729 |
|
67262 | 730 |
* Action "isabelle.draft" is similar to "isabelle.preview", but shows a |
68067 | 731 |
plain-text document draft. Both are available via the menu "Plugins / |
732 |
Isabelle". |
|
67262 | 733 |
|
67304
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
734 |
* 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
|
735 |
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
|
736 |
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
|
737 |
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
|
738 |
Unicode content when saving the file. |
3cf05d7cf174
more robust treatment of conflicts with existing Unicode text;
wenzelm
parents:
67303
diff
changeset
|
739 |
|
68545 | 740 |
* Bibtex database files (.bib) are semantically checked. |
741 |
||
67993 | 742 |
* Update to jedit-5.5.0, the latest release. |
743 |
||
67246
4cedf44f2af1
isabelle.preview presents auxiliary text files as well;
wenzelm
parents:
67224
diff
changeset
|
744 |
|
67261 | 745 |
*** Isabelle/VSCode Prover IDE *** |
746 |
||
747 |
* HTML preview of theories and other file-formats similar to |
|
748 |
Isabelle/jEdit. |
|
749 |
||
68690
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
750 |
* Command-line tool "isabelle vscode_server" accepts the same options |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
751 |
-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
|
752 |
relevant for isabelle.args configuration settings in VSCode. The former |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
753 |
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
|
754 |
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
|
755 |
spot in the session structure. INCOMPATIBILITY. |
354c04092cd0
more flexible session selection as in "isabelle jedit";
wenzelm
parents:
68681
diff
changeset
|
756 |
|
66768 | 757 |
|
67140 | 758 |
*** Document preparation *** |
759 |
||
67448 | 760 |
* Formal comments work uniformly in outer syntax, inner syntax (term |
761 |
language), Isabelle/ML and some other embedded languages of Isabelle. |
|
762 |
See also "Document comments" in the isar-ref manual. The following forms |
|
763 |
are supported: |
|
764 |
||
765 |
- marginal text comment: \<comment> \<open>\<dots>\<close> |
|
766 |
- canceled source: \<^cancel>\<open>\<dots>\<close> |
|
767 |
- raw LaTeX: \<^latex>\<open>\<dots>\<close> |
|
67413 | 768 |
|
67381 | 769 |
* Outside of the inner theory body, the default presentation context is |
770 |
theory Pure. Thus elementary antiquotations may be used in markup |
|
771 |
commands (e.g. 'chapter', 'section', 'text') and formal comments. |
|
772 |
||
68513 | 773 |
* System option "document_tags" specifies alternative command tags. This |
774 |
is occasionally useful to control the global visibility of commands via |
|
775 |
session options (e.g. in ROOT). |
|
67140 | 776 |
|
777 |
* Document markup commands ('section', 'text' etc.) are implicitly |
|
778 |
tagged as "document" and visible by default. This avoids the application |
|
779 |
of option "document_tags" to these commands. |
|
780 |
||
67145 | 781 |
* Isabelle names are mangled into LaTeX macro names to allow the full |
782 |
identifier syntax with underscore, prime, digits. This is relevant for |
|
783 |
antiquotations in control symbol notation, e.g. \<^const_name> becomes |
|
784 |
\isactrlconstUNDERSCOREname. |
|
785 |
||
68393 | 786 |
* Document preparation with skip_proofs option now preserves the content |
787 |
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
|
788 |
|
68484 | 789 |
* Document antiquotation @{theory name} requires the long |
790 |
session-qualified theory name: this is what users reading the text |
|
791 |
normally need to import. |
|
792 |
||
67219 | 793 |
* Document antiquotation @{session name} checks and prints the given |
794 |
session name verbatim. |
|
795 |
||
68393 | 796 |
* Document antiquotation @{cite} now checks the given Bibtex entries |
797 |
against the Bibtex database files -- only in batch-mode session builds. |
|
67157 | 798 |
|
67176
13b5c3ff1954
re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;
wenzelm
parents:
67173
diff
changeset
|
799 |
* 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
|
800 |
Isabelle/Scala, with simplified arguments and explicit errors from the |
67203 | 801 |
latex and bibtex process. Minor INCOMPATIBILITY. |
67173 | 802 |
|
68393 | 803 |
* Session ROOT entry: empty 'document_files' means there is no document |
804 |
for this session. There is no need to specify options [document = false] |
|
805 |
anymore. |
|
806 |
||
67140 | 807 |
|
67702
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
808 |
*** Isar *** |
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
809 |
|
2d9918f5b33c
command 'interpret' no longer exposes resulting theorems as literal facts;
wenzelm
parents:
67616
diff
changeset
|
810 |
* 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
|
811 |
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
|
812 |
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
|
813 |
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
|
814 |
(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
|
815 |
|
68393 | 816 |
* The old 'def' command has been discontinued (legacy since |
817 |
Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with |
|
818 |
object-logic equality or equivalence. |
|
819 |
||
68543 | 820 |
|
821 |
*** Pure *** |
|
822 |
||
823 |
* The inner syntax category "sort" now includes notation "_" for the |
|
824 |
dummy sort: it is effectively ignored in type-inference. |
|
825 |
||
67740 | 826 |
* Rewrites clauses (keyword 'rewrites') were moved into the locale |
68393 | 827 |
expression syntax, where they are part of locale instances. In |
828 |
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
|
829 |
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
|
830 |
rewriting may need to be pulled up into the surrounding theory. |
68393 | 831 |
|
832 |
* For 'rewrites' clauses, if activating a locale instance fails, fall |
|
833 |
back to reading the clause first. This helps avoid qualification of |
|
67764 | 834 |
locale instances where the qualifier's sole purpose is avoiding |
835 |
duplicate constant declarations. |
|
67741
d5a7f2c54655
Fall back to reading rewrite morphism first if activation fails without it.
ballarin
parents:
67740
diff
changeset
|
836 |
|
68543 | 837 |
* Proof method "simp" now supports a new modifier "flip:" followed by a |
838 |
list of theorems. Each of these theorems is removed from the simpset |
|
839 |
(without warning if it is not there) and the symmetric version of the |
|
840 |
theorem (i.e. lhs and rhs exchanged) is added to the simpset. For "auto" |
|
841 |
and friends the modifier is "simp flip:". |
|
67718 | 842 |
|
843 |
||
66661 | 844 |
*** HOL *** |
845 |
||
68568 | 846 |
* Sledgehammer: bundled version of "vampire" (for non-commercial users) |
847 |
helps to avoid fragility of "remote_vampire" service. |
|
848 |
||
68028 | 849 |
* Clarified relationship of characters, strings and code generation: |
850 |
||
68393 | 851 |
- Type "char" is now a proper datatype of 8-bit values. |
852 |
||
853 |
- Conversions "nat_of_char" and "char_of_nat" are gone; use more |
|
854 |
general conversions "of_char" and "char_of" with suitable type |
|
855 |
constraints instead. |
|
856 |
||
857 |
- The zero character is just written "CHR 0x00", not "0" any longer. |
|
858 |
||
859 |
- Type "String.literal" (for code generation) is now isomorphic to |
|
860 |
lists of 7-bit (ASCII) values; concrete values can be written as |
|
861 |
"STR ''...''" for sequences of printable characters and "STR 0x..." |
|
862 |
for one single ASCII code point given as hexadecimal numeral. |
|
863 |
||
864 |
- Type "String.literal" supports concatenation "... + ..." for all |
|
865 |
standard target languages. |
|
866 |
||
867 |
- Theory HOL-Library.Code_Char is gone; study the explanations |
|
868 |
concerning "String.literal" in the tutorial on code generation to |
|
869 |
get an idea how target-language string literals can be converted to |
|
870 |
HOL string values and vice versa. |
|
871 |
||
872 |
- Session Imperative-HOL: operation "raise" directly takes a value of |
|
873 |
type "String.literal" as argument, not type "string". |
|
874 |
||
875 |
INCOMPATIBILITY. |
|
876 |
||
877 |
* Code generation: Code generation takes an explicit option |
|
878 |
"case_insensitive" to accomodate case-insensitive file systems. |
|
879 |
||
880 |
* Abstract bit operations as part of Main: push_bit, take_bit, drop_bit. |
|
881 |
||
882 |
* New, more general, axiomatization of complete_distrib_lattice. The |
|
883 |
former axioms: |
|
884 |
||
885 |
"sup x (Inf X) = Inf (sup x ` X)" and "inf x (Sup X) = Sup (inf x ` X)" |
|
886 |
||
887 |
are replaced by: |
|
888 |
||
889 |
"Inf (Sup ` A) <= Sup (Inf ` {f ` A | f . (! Y \<in> A . f Y \<in> Y)})" |
|
890 |
||
891 |
The instantiations of sets and functions as complete_distrib_lattice are |
|
892 |
moved to Hilbert_Choice.thy because their proofs need the Hilbert choice |
|
893 |
operator. The dual of this property is also proved in theory |
|
894 |
HOL.Hilbert_Choice. |
|
67831
07f5588f2735
Removed stray 'sledgehammer' invocation
Manuel Eberl <eberlm@in.tum.de>
parents:
67830
diff
changeset
|
895 |
|
67999
1b05f74f2e5f
tidying up including contributions from Paulo EmÃlio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
67993
diff
changeset
|
896 |
* New syntax for the minimum/maximum of a function over a finite set: |
68393 | 897 |
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
|
898 |
|
67525
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
899 |
* Clarifed theorem names: |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
900 |
|
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
901 |
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
|
902 |
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
|
903 |
|
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
904 |
Minor INCOMPATIBILITY. |
5d04d7bcd5f6
avoid concrete (anti)mono in theorem names since it could be the other way round
haftmann
parents:
67510
diff
changeset
|
905 |
|
66661 | 906 |
* SMT module: |
68393 | 907 |
|
66661 | 908 |
- The 'smt_oracle' option is now necessary when using the 'smt' method |
66662 | 909 |
with a solver other than Z3. INCOMPATIBILITY. |
68393 | 910 |
|
66844 | 911 |
- The encoding to first-order logic is now more complete in the |
912 |
presence of higher-order quantifiers. An 'smt_explicit_application' |
|
913 |
option has been added to control this. INCOMPATIBILITY. |
|
914 |
||
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66803
diff
changeset
|
915 |
* Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to |
66844 | 916 |
sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on |
917 |
interpretation of abstract locales. INCOMPATIBILITY. |
|
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66803
diff
changeset
|
918 |
|
68393 | 919 |
* Predicate coprime is now a real definition, not a mere abbreviation. |
920 |
INCOMPATIBILITY. |
|
921 |
||
66803 | 922 |
* Predicate pairwise_coprime abolished, use "pairwise coprime" instead. |
923 |
INCOMPATIBILITY. |
|
924 |
||
68373 | 925 |
* The relator rel_filter on filters has been strengthened to its |
68393 | 926 |
canonical categorical definition with better properties. |
927 |
INCOMPATIBILITY. |
|
67616
1d005f514417
strengthen filter relator to canonical categorical definition with better properties
Andreas Lochbihler
parents:
67591
diff
changeset
|
928 |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67999
diff
changeset
|
929 |
* 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
|
930 |
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
|
931 |
Renamed: |
68393 | 932 |
|
933 |
span_inc ~> span_superset |
|
934 |
span_superset ~> span_base |
|
935 |
span_eq ~> span_eq_iff |
|
936 |
||
937 |
INCOMPATIBILITY. |
|
66844 | 938 |
|
66937 | 939 |
* Class linordered_semiring_1 covers zero_less_one also, ruling out |
940 |
pathologic instances. Minor INCOMPATIBILITY. |
|
941 |
||
68393 | 942 |
* Theory HOL.List: functions "sorted_wrt" and "sorted" now compare every |
943 |
element in a list to all following elements, not just the next one. |
|
944 |
||
945 |
* Theory HOL.List syntax: |
|
946 |
||
947 |
- filter-syntax "[x <- xs. P]" is no longer output syntax, but only |
|
948 |
input syntax |
|
949 |
||
950 |
- 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
|
951 |
|
68450 | 952 |
* Theory Map: "empty" must now be qualified as "Map.empty". |
953 |
||
67051 | 954 |
* Removed nat-int transfer machinery. Rare INCOMPATIBILITY. |
955 |
||
68100 | 956 |
* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid |
957 |
clash with fact mod_mult_self4 (on more generic semirings). |
|
958 |
INCOMPATIBILITY. |
|
959 |
||
960 |
* Eliminated some theorem aliasses: |
|
961 |
even_times_iff ~> even_mult_iff |
|
962 |
mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1 |
|
963 |
even_of_nat ~> even_int_iff |
|
964 |
||
965 |
INCOMPATIBILITY. |
|
966 |
||
68157 | 967 |
* Eliminated some theorem duplicate variations: |
68393 | 968 |
|
969 |
- dvd_eq_mod_eq_0_numeral can be replaced by dvd_eq_mod_eq_0 |
|
970 |
- mod_Suc_eq_Suc_mod can be replaced by mod_Suc |
|
971 |
- mod_Suc_eq_Suc_mod [symmetrict] can be replaced by mod_simps |
|
972 |
- mod_eq_0_iff can be replaced by mod_eq_0_iff_dvd and dvd_def |
|
973 |
- the witness of mod_eqD can be given directly as "_ div _" |
|
68157 | 974 |
|
975 |
INCOMPATIBILITY. |
|
976 |
||
68260 | 977 |
* Classical setup: Assumption "m mod d = 0" (for m d :: nat) is no |
68393 | 978 |
longer aggresively destroyed to "\<exists>q. m = d * q". INCOMPATIBILITY, adding |
979 |
"elim!: dvd" to classical proof methods in most situations restores |
|
980 |
broken proofs. |
|
981 |
||
982 |
* Theory HOL-Library.Conditional_Parametricity provides command |
|
983 |
'parametric_constant' for proving parametricity of non-recursive |
|
984 |
definitions. For constants that are not fully parametric the command |
|
985 |
will infer conditions on relations (e.g., bi_unique, bi_total, or type |
|
986 |
class conditions such as "respects 0") sufficient for parametricity. See |
|
987 |
theory HOL-ex.Conditional_Parametricity_Examples for some examples. |
|
988 |
||
989 |
* Theory HOL-Library.Code_Lazy provides a new preprocessor for the code |
|
990 |
generator to generate code for algebraic types with lazy evaluation |
|
68639 | 991 |
semantics even in call-by-value target languages. See the theories |
68647 | 992 |
HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some |
993 |
examples. |
|
68393 | 994 |
|
995 |
* Theory HOL-Library.Landau_Symbols has been moved here from AFP. |
|
996 |
||
997 |
* Theory HOL-Library.Old_Datatype no longer provides the legacy command |
|
998 |
'old_datatype'. INCOMPATIBILITY. |
|
999 |
||
1000 |
* Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide |
|
1001 |
instances of rat, real, complex as factorial rings etc. Import |
|
1002 |
HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. |
|
1003 |
INCOMPATIBILITY. |
|
1004 |
||
1005 |
* Session HOL-Algebra: renamed (^) to [^] to avoid conflict with new |
|
1006 |
infix/prefix notation. |
|
1007 |
||
68543 | 1008 |
* Session HOL-Algebra: revamped with much new material. The set of |
1009 |
isomorphisms between two groups is now denoted iso rather than iso_set. |
|
1010 |
INCOMPATIBILITY. |
|
1011 |
||
1012 |
* Session HOL-Analysis: the Arg function now respects the same interval |
|
1013 |
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
|
1014 |
INCOMPATIBILITY. |
d4312962161a
Rationalisation of complex transcendentals, esp the Arg function
paulson <lp15@cam.ac.uk>
parents:
68484
diff
changeset
|
1015 |
|
68548 | 1016 |
* Session HOL-Analysis: the functions zorder, zer_poly, porder and |
1017 |
pol_poly have been redefined. All related lemmas have been reworked. |
|
68531 | 1018 |
INCOMPATIBILITY. |
1019 |
||
68393 | 1020 |
* Session HOL-Analysis: infinite products, Moebius functions, the |
1021 |
Riemann mapping theorem, the Vitali covering theorem, |
|
1022 |
change-of-variables results for integration and measures. |
|
68260 | 1023 |
|
68647 | 1024 |
* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics |
1025 |
or real-valued functions (limits, "Big-O", etc.) automatically. |
|
68681 | 1026 |
See also ~~/src/HOL/Real_Asymp/Manual for some documentation. |
68647 | 1027 |
|
68545 | 1028 |
* Session HOL-Types_To_Sets: more tool support (unoverload_type combines |
1029 |
internalize_sorts and unoverload) and larger experimental application |
|
1030 |
(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
|
1031 |
|
66651 | 1032 |
|
68116 | 1033 |
*** ML *** |
1034 |
||
1035 |
* Operation Export.export emits theory exports (arbitrary blobs), which |
|
69960 | 1036 |
are stored persistently in the session build database. |
68116 | 1037 |
|
68276 | 1038 |
* Command 'ML_export' exports ML toplevel bindings to the global |
1039 |
bootstrap environment of the ML process. This allows ML evaluation |
|
1040 |
without a formal theory context, e.g. in command-line tools like |
|
1041 |
"isabelle process". |
|
1042 |
||
68116 | 1043 |
|
66729 | 1044 |
*** System *** |
1045 |
||
67088 | 1046 |
* Mac OS X 10.10 Yosemite is now the baseline version; Mavericks is no |
1047 |
longer supported. |
|
1048 |
||
68393 | 1049 |
* Linux and Windows/Cygwin is for x86_64 only, old 32bit platform |
1050 |
support has been discontinued. |
|
1051 |
||
66906 | 1052 |
* Java runtime is for x86_64 only. Corresponding Isabelle settings have |
1053 |
been renamed to ISABELLE_TOOL_JAVA_OPTIONS and JEDIT_JAVA_OPTIONS, |
|
1054 |
instead of former 32/64 variants. INCOMPATIBILITY. |
|
1055 |
||
68003 | 1056 |
* Old settings ISABELLE_PLATFORM and ISABELLE_WINDOWS_PLATFORM should be |
1057 |
phased out due to unclear preference of 32bit vs. 64bit architecture. |
|
1058 |
Explicit GNU bash expressions are now preferred, for example (with |
|
1059 |
quotes): |
|
1060 |
||
1061 |
#Posix executables (Unix or Cygwin), with preference for 64bit |
|
1062 |
"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}" |
|
1063 |
||
1064 |
#native Windows or Unix executables, with preference for 64bit |
|
1065 |
"${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}}" |
|
1066 |
||
1067 |
#native Windows (32bit) or Unix executables (preference for 64bit) |
|
1068 |
"${ISABELLE_WINDOWS_PLATFORM32:-${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}}" |
|
1069 |
||
66745 | 1070 |
* Command-line tool "isabelle build" supports new options: |
1071 |
- option -B NAME: include session NAME and all descendants |
|
1072 |
- option -S: only observe changes of sources, not heap images |
|
66841 | 1073 |
- option -f: forces a fresh build |
66737
2edc0c42c883
option -B for "isabelle build" and "isabelle imports";
wenzelm
parents:
66729
diff
changeset
|
1074 |
|
68734
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
1075 |
* 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
|
1076 |
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
|
1077 |
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
|
1078 |
only. |
c14a2cc9b5ef
isabelle build options -c -x -B refer to imports_graph;
wenzelm
parents:
68690
diff
changeset
|
1079 |
|
66843 | 1080 |
* Command-line tool "isabelle build" takes "condition" options with the |
1081 |
corresponding environment values into account, when determining the |
|
1082 |
up-to-date status of a session. |
|
1083 |
||
68393 | 1084 |
* The command-line tool "dump" dumps information from the cumulative |
1085 |
PIDE session database: many sessions may be loaded into a given logic |
|
1086 |
image, results from all loaded theories are written to the output |
|
1087 |
directory. |
|
1088 |
||
66851
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66844
diff
changeset
|
1089 |
* 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
|
1090 |
imports. This helps to minimize the session dependency graph. |
c75769065548
more informative Imports.Report with actual session imports (minimized);
wenzelm
parents:
66844
diff
changeset
|
1091 |
|
69960 | 1092 |
* The command-line tool "export" and 'export_files' in session ROOT |
1093 |
entries retrieve theory exports from the session build database. |
|
68393 | 1094 |
|
1095 |
* The command-line tools "isabelle server" and "isabelle client" provide |
|
1096 |
access to the Isabelle Server: it supports responsive session management |
|
1097 |
and concurrent use of theories, based on Isabelle/PIDE infrastructure. |
|
1098 |
See also the "system" manual. |
|
1099 |
||
1100 |
* The command-line tool "isabelle update_comments" normalizes formal |
|
1101 |
comments in outer syntax as follows: \<comment> \<open>text\<close> (whith a single space to |
|
1102 |
approximate the appearance in document output). This is more specific |
|
1103 |
than former "isabelle update_cartouches -c": the latter tool option has |
|
1104 |
been discontinued. |
|
1105 |
||
1106 |
* The command-line tool "isabelle mkroot" now always produces a document |
|
1107 |
outline: its options have been adapted accordingly. INCOMPATIBILITY. |
|
1108 |
||
1109 |
* The command-line tool "isabelle mkroot -I" initializes a Mercurial |
|
1110 |
repository for the generated session files. |
|
1111 |
||
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1112 |
* Settings ISABELLE_HEAPS + ISABELLE_BROWSER_INFO (or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1113 |
ISABELLE_HEAPS_SYSTEM + ISABELLE_BROWSER_INFO_SYSTEM in "system build |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1114 |
mode") determine the directory locations of the main build artefacts -- |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1115 |
instead of hard-wired directories in ISABELLE_HOME_USER (or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1116 |
ISABELLE_HOME). |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1117 |
|
68393 | 1118 |
* Settings ISABELLE_PATH and ISABELLE_OUTPUT have been discontinued: |
1119 |
heap images and session databases are always stored in |
|
68523
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1120 |
$ISABELLE_HEAPS/$ML_IDENTIFIER (command-line default) or |
ccacc84e0251
clarified settings -- avoid hard-wired directories;
wenzelm
parents:
68522
diff
changeset
|
1121 |
$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER (main Isabelle application or |
68393 | 1122 |
"isabelle jedit -s" or "isabelle build -s"). |
67099 | 1123 |
|
67199 | 1124 |
* ISABELLE_LATEX and ISABELLE_PDFLATEX now include platform-specific |
1125 |
options for improved error reporting. Potential INCOMPATIBILITY with |
|
1126 |
unusual LaTeX installations, may have to adapt these settings. |
|
1127 |
||
68393 | 1128 |
* Update to Poly/ML 5.7.1 with slightly improved performance and PIDE |
1129 |
markup for identifier bindings. It now uses The GNU Multiple Precision |
|
67591 | 1130 |
Arithmetic Library (libgmp) on all platforms, notably Mac OS X with |
1131 |
32/64 bit. |
|
1132 |
||
67099 | 1133 |
|
66729 | 1134 |
|
66472 | 1135 |
New in Isabelle2017 (October 2017) |
1136 |
---------------------------------- |
|
64439 | 1137 |
|
64986 | 1138 |
*** General *** |
1139 |
||
66238 | 1140 |
* Experimental support for Visual Studio Code (VSCode) as alternative |
1141 |
Isabelle/PIDE front-end, see also |
|
66599 | 1142 |
https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2017 |
66238 | 1143 |
|
1144 |
VSCode is a new type of application that continues the concepts of |
|
1145 |
"programmer's editor" and "integrated development environment" towards |
|
1146 |
fully semantic editing and debugging -- in a relatively light-weight |
|
1147 |
manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure. |
|
1148 |
Technically, VSCode is based on the Electron application framework |
|
1149 |
(Node.js + Chromium browser + V8), which is implemented in JavaScript |
|
1150 |
and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala |
|
1151 |
modules around a Language Server implementation. |
|
1152 |
||
65504 | 1153 |
* Theory names are qualified by the session name that they belong to. |
66454 | 1154 |
This affects imports, but not the theory name space prefix (which is |
1155 |
just the theory base name as before). |
|
1156 |
||
1157 |
In order to import theories from other sessions, the ROOT file format |
|
1158 |
provides a new 'sessions' keyword. In contrast, a theory that is |
|
1159 |
imported in the old-fashioned manner via an explicit file-system path |
|
66472 | 1160 |
belongs to the current session, and might cause theory name conflicts |
66454 | 1161 |
later on. Theories that are imported from other sessions are excluded |
1162 |
from the current session document. The command-line tool "isabelle |
|
1163 |
imports" helps to update theory imports. |
|
1164 |
||
65451 | 1165 |
* The main theory entry points for some non-HOL sessions have changed, |
1166 |
to avoid confusion with the global name "Main" of the session HOL. This |
|
1167 |
leads to the follow renamings: |
|
1168 |
||
1169 |
CTT/Main.thy ~> CTT/CTT.thy |
|
1170 |
ZF/Main.thy ~> ZF/ZF.thy |
|
1171 |
ZF/Main_ZF.thy ~> ZF/ZF.thy |
|
1172 |
ZF/Main_ZFC.thy ~> ZF/ZFC.thy |
|
1173 |
ZF/ZF.thy ~> ZF/ZF_Base.thy |
|
1174 |
||
1175 |
INCOMPATIBILITY. |
|
1176 |
||
66472 | 1177 |
* Commands 'alias' and 'type_alias' introduce aliases for constants and |
1178 |
type constructors, respectively. This allows adhoc changes to name-space |
|
1179 |
accesses within global or local theory contexts, e.g. within a 'bundle'. |
|
1180 |
||
64986 | 1181 |
* Document antiquotations @{prf} and @{full_prf} output proof terms |
1182 |
(again) in the same way as commands 'prf' and 'full_prf'. |
|
1183 |
||
65055 | 1184 |
* Computations generated by the code generator can be embedded directly |
1185 |
into ML, alongside with @{code} antiquotations, using the following |
|
1186 |
antiquotations: |
|
1187 |
||
1188 |
@{computation ... terms: ... datatypes: ...} : |
|
1189 |
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a |
|
1190 |
@{computation_conv ... terms: ... datatypes: ...} : |
|
1191 |
(Proof.context -> 'ml -> conv) -> Proof.context -> conv |
|
65045
b69ef432438d
avoid Unicode that conflicts with Isabelle symbol rendering;
wenzelm
parents:
65042
diff
changeset
|
1192 |
@{computation_check terms: ... datatypes: ...} : Proof.context -> conv |
65041 | 1193 |
|
65055 | 1194 |
See src/HOL/ex/Computations.thy, |
1195 |
src/HOL/Decision_Procs/Commutative_Ring.thy and |
|
1196 |
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the |
|
1197 |
tutorial on code generation. |
|
65041 | 1198 |
|
64986 | 1199 |
|
64602 | 1200 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
1201 |
||
66472 | 1202 |
* Session-qualified theory imports allow the Prover IDE to process |
1203 |
arbitrary theory hierarchies independently of the underlying logic |
|
1204 |
session image (e.g. option "isabelle jedit -l"), but the directory |
|
1205 |
structure needs to be known in advance (e.g. option "isabelle jedit -d" |
|
1206 |
or a line in the file $ISABELLE_HOME_USER/ROOTS). |
|
64602 | 1207 |
|
64842 | 1208 |
* The PIDE document model maintains file content independently of the |
1209 |
status of jEdit editor buffers. Reloading jEdit buffers no longer causes |
|
1210 |
changes of formal document content. Theory dependencies are always |
|
1211 |
resolved internally, without the need for corresponding editor buffers. |
|
1212 |
The system option "jedit_auto_load" has been discontinued: it is |
|
1213 |
effectively always enabled. |
|
1214 |
||
64867 | 1215 |
* The Theories dockable provides a "Purge" button, in order to restrict |
1216 |
the document model to theories that are required for open editor |
|
1217 |
buffers. |
|
1218 |
||
66424 | 1219 |
* The Theories dockable indicates the overall status of checking of each |
1220 |
entry. When all forked tasks of a theory are finished, the border is |
|
1221 |
painted with thick lines; remaining errors in this situation are |
|
1222 |
represented by a different border color. |
|
1223 |
||
66472 | 1224 |
* Automatic indentation is more careful to avoid redundant spaces in |
1225 |
intermediate situations. Keywords are indented after input (via typed |
|
1226 |
characters or completion); see also option "jedit_indent_input". |
|
1227 |
||
1228 |
* Action "isabelle.preview" opens an HTML preview of the current theory |
|
1229 |
document in the default web browser. |
|
1230 |
||
66574
e16b27bd3f76
reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
wenzelm
parents:
66563
diff
changeset
|
1231 |
* 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
|
1232 |
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
|
1233 |
used for formal checking. |
66472 | 1234 |
|
66462 | 1235 |
* The main Isabelle/jEdit plugin may be restarted manually (using the |
1236 |
jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains |
|
1237 |
enabled at all times. |
|
1238 |
||
66472 | 1239 |
* Update to current jedit-5.4.0. |
65329 | 1240 |
|
64602 | 1241 |
|
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
1242 |
*** Pure *** |
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
1243 |
|
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
1244 |
* 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
|
1245 |
[code del] results in function with no equations (runtime abort) rather |
66472 | 1246 |
than an unimplemented function (generation time abort). Use explicit |
66665 | 1247 |
[[code drop:]] to enforce the latter. Minor INCOMPATIBILITY. |
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
1248 |
|
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
|
1249 |
* Proper concept of code declarations in code.ML: |
66472 | 1250 |
- Regular code declarations act only on the global theory level, being |
1251 |
ignored with warnings if syntactically malformed. |
|
1252 |
- Explicitly global code declarations yield errors if syntactically |
|
1253 |
malformed. |
|
1254 |
- Default code declarations are silently ignored if syntactically |
|
1255 |
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
|
1256 |
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
|
1257 |
|
66472 | 1258 |
* Clarified and standardized internal data bookkeeping of code |
1259 |
declarations: history of serials allows to track potentially |
|
1260 |
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
|
1261 |
|
66149
4bf16fb7c14d
deleting a code equation never leads to unimplemented function
haftmann
parents:
66135
diff
changeset
|
1262 |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1263 |
*** HOL *** |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1264 |
|
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
66599
diff
changeset
|
1265 |
* 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
|
1266 |
|
66472 | 1267 |
* SMT module: |
1268 |
- A new option, 'smt_nat_as_int', has been added to translate 'nat' to |
|
1269 |
'int' and benefit from the SMT solver's theory reasoning. It is |
|
1270 |
disabled by default. |
|
1271 |
- The legacy module "src/HOL/Library/Old_SMT.thy" has been removed. |
|
1272 |
- Several small issues have been rectified in the 'smt' command. |
|
1273 |
||
1274 |
* (Co)datatype package: The 'size_gen_o_map' lemma is no longer |
|
1275 |
generated for datatypes with type class annotations. As a result, the |
|
1276 |
tactic that derives it no longer fails on nested datatypes. Slight |
|
1277 |
INCOMPATIBILITY. |
|
66450
a8299195ed82
NEWS: Removed constant subseq; subsumed by strict_mono
eberlm <eberlm@in.tum.de>
parents:
66449
diff
changeset
|
1278 |
|
66345
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
66310
diff
changeset
|
1279 |
* Command and antiquotation "value" with modified default strategy: |
882abe912da9
do not fall back on nbe if plain evaluation fails
haftmann
parents:
66310
diff
changeset
|
1280 |
terms without free variables are always evaluated using plain evaluation |
66472 | 1281 |
only, with no fallback on normalization by evaluation. Minor |
1282 |
INCOMPATIBILITY. |
|
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65841
diff
changeset
|
1283 |
|
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
65544
diff
changeset
|
1284 |
* Theories "GCD" and "Binomial" are already included in "Main" (instead |
65575 | 1285 |
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
|
1286 |
|
65170
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1287 |
* Constant "surj" is a full input/output abbreviation (again). |
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1288 |
Minor INCOMPATIBILITY. |
53675f36820d
restored surj as output abbreviation, amending 6af79184bef3
haftmann
parents:
65099
diff
changeset
|
1289 |
|
64632 | 1290 |
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. |
1291 |
INCOMPATIBILITY. |
|
1292 |
||
66472 | 1293 |
* Renamed ii to imaginary_unit in order to free up ii as a variable |
1294 |
name. The syntax \<i> remains available. INCOMPATIBILITY. |
|
1295 |
||
1296 |
* Dropped abbreviations transP, antisymP, single_valuedP; use constants |
|
1297 |
transp, antisymp, single_valuedp instead. INCOMPATIBILITY. |
|
1298 |
||
1299 |
* Constant "subseq" in Topological_Spaces has been removed -- it is |
|
1300 |
subsumed by "strict_mono". Some basic lemmas specific to "subseq" have |
|
1301 |
been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc. |
|
1302 |
||
1303 |
* Theory List: "sublist" renamed to "nths" in analogy with "nth", and |
|
1304 |
"sublisteq" renamed to "subseq". Minor INCOMPATIBILITY. |
|
1305 |
||
1306 |
* Theory List: new generic function "sorted_wrt". |
|
1307 |
||
1308 |
* Named theorems mod_simps covers various congruence rules concerning |
|
1309 |
mod, replacing former zmod_simps. INCOMPATIBILITY. |
|
64787 | 1310 |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1311 |
* Swapped orientation of congruence rules mod_add_left_eq, |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1312 |
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
|
1313 |
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, |
66472 | 1314 |
mod_diff_eq. INCOMPATIBILITY. |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1315 |
|
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1316 |
* Generalized some facts: |
64876 | 1317 |
measure_induct_rule |
1318 |
measure_induct |
|
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1319 |
zminus_zmod ~> mod_minus_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1320 |
zdiff_zmod_left ~> mod_diff_left_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1321 |
zdiff_zmod_right ~> mod_diff_right_eq |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1322 |
zmod_eq_dvd_iff ~> mod_eq_dvd_iff |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1323 |
INCOMPATIBILITY. |
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64555
diff
changeset
|
1324 |
|
66472 | 1325 |
* Algebraic type class hierarchy of euclidean (semi)rings in HOL: |
1326 |
euclidean_(semi)ring, euclidean_(semi)ring_cancel, |
|
1327 |
unique_euclidean_(semi)ring; instantiation requires provision of a |
|
1328 |
euclidean size. |
|
1329 |
||
1330 |
* Theory "HOL-Number_Theory.Euclidean_Algorithm" has been reworked: |
|
1331 |
- Euclidean induction is available as rule eucl_induct. |
|
1332 |
- Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm, |
|
1333 |
Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow |
|
1334 |
easy instantiation of euclidean (semi)rings as GCD (semi)rings. |
|
1335 |
- Coefficients obtained by extended euclidean algorithm are |
|
1336 |
available as "bezout_coefficients". |
|
1337 |
INCOMPATIBILITY. |
|
1338 |
||
1339 |
* Theory "Number_Theory.Totient" introduces basic notions about Euler's |
|
1340 |
totient function previously hidden as solitary example in theory |
|
1341 |
Residues. Definition changed so that "totient 1 = 1" in agreement with |
|
1342 |
the literature. Minor INCOMPATIBILITY. |
|
1343 |
||
66542 | 1344 |
* New styles in theory "HOL-Library.LaTeXsugar": |
66541 | 1345 |
- "dummy_pats" for printing equations with "_" on the lhs; |
1346 |
- "eta_expand" for printing eta-expanded terms. |
|
1347 |
||
66472 | 1348 |
* Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has |
1349 |
been renamed to bij_swap_compose_bij. INCOMPATIBILITY. |
|
1350 |
||
66643
f7e38b8583a0
Correction of typos and a bit of streamlining
paulson <lp15@cam.ac.uk>
parents:
66641
diff
changeset
|
1351 |
* 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
|
1352 |
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
|
1353 |
|
66480
4b8d1df8933b
HOL-Analysis: Convergent FPS and infinite sums
Manuel Eberl <eberlm@in.tum.de>
parents:
66474
diff
changeset
|
1354 |
* 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
|
1355 |
renamed to fps_X/fps_exp/fps_ln/fps_hypergeo to avoid polluting the name |
66472 | 1356 |
space. INCOMPATIBILITY. |
1357 |
||
1358 |
* Theory "HOL-Library.FinFun" has been moved to AFP (again). |
|
1359 |
INCOMPATIBILITY. |
|
1360 |
||
1361 |
* Theory "HOL-Library.FuncSet": some old and rarely used ASCII |
|
1362 |
replacement syntax has been removed. INCOMPATIBILITY, standard syntax |
|
1363 |
with symbols should be used instead. The subsequent commands help to |
|
1364 |
reproduce the old forms, e.g. to simplify porting old theories: |
|
1365 |
||
1366 |
syntax (ASCII) |
|
1367 |
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PIE _:_./ _)" 10) |
|
1368 |
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10) |
|
1369 |
"_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(3%_:_./ _)" [0,0,3] 3) |
|
1370 |
||
1371 |
* Theory "HOL-Library.Multiset": the simprocs on subsets operators of |
|
1372 |
multisets have been renamed: |
|
1373 |
||
1374 |
msetless_cancel_numerals ~> msetsubset_cancel |
|
1375 |
msetle_cancel_numerals ~> msetsubset_eq_cancel |
|
1376 |
||
1377 |
INCOMPATIBILITY. |
|
1378 |
||
66481
d35f7a9f92e2
output syntax for pattern aliases
Lars Hupel <lars.hupel@mytum.de>
parents:
66480
diff
changeset
|
1379 |
* 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
|
1380 |
for pattern aliases as known from Haskell, Scala and ML. |
65515 | 1381 |
|
66563 | 1382 |
* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs. |
1383 |
||
64898 | 1384 |
* Session HOL-Analysis: more material involving arcs, paths, covering |
66650 | 1385 |
spaces, innessential maps, retracts, infinite products, simplicial |
1386 |
complexes. Baire Category theorem. Major results include the Jordan |
|
1387 |
Curve Theorem and the Great Picard Theorem. |
|
66472 | 1388 |
|
1389 |
* Session HOL-Algebra has been extended by additional lattice theory: |
|
1390 |
the Knaster-Tarski fixed point theorem and Galois Connections. |
|
1391 |
||
1392 |
* Sessions HOL-Computational_Algebra and HOL-Number_Theory: new notions |
|
1393 |
of squarefreeness, n-th powers, and prime powers. |
|
1394 |
||