author | wenzelm |
Wed, 04 Nov 2015 11:53:22 +0100 | |
changeset 61567 | e7d4dac7a79f |
parent 61566 | c3d6e570ccef |
child 61571 | 9c50eb3bff50 |
permissions | -rw-r--r-- |
57491 | 1 |
Isabelle NEWS -- history of user-relevant changes |
2 |
================================================= |
|
2553 | 3 |
|
60006 | 4 |
(Note: Isabelle/jEdit shows a tree-view of this file in Sidekick.) |
5 |
||
60331 | 6 |
|
60138 | 7 |
New in this Isabelle version |
8 |
---------------------------- |
|
9 |
||
61337 | 10 |
*** General *** |
11 |
||
12 |
* Toplevel theorem statements have been simplified as follows: |
|
13 |
||
14 |
theorems ~> lemmas |
|
15 |
schematic_lemma ~> schematic_goal |
|
16 |
schematic_theorem ~> schematic_goal |
|
17 |
schematic_corollary ~> schematic_goal |
|
18 |
||
19 |
Command-line tool "isabelle update_theorems" updates theory sources |
|
20 |
accordingly. |
|
21 |
||
61338 | 22 |
* Toplevel theorem statement 'proposition' is another alias for |
23 |
'theorem'. |
|
24 |
||
61337 | 25 |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
26 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
27 |
|
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
28 |
* Improved scheduling for urgent print tasks (e.g. command state output, |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
29 |
interactive queries) wrt. long-running background tasks. |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
30 |
|
60986 | 31 |
* IDE support for the source-level debugger of Poly/ML, to work with |
60984 | 32 |
Isabelle/ML and official Standard ML. Configuration option "ML_debugger" |
33 |
and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
|
34 |
'SML_file_no_debug' control compilation of sources with debugging |
|
35 |
information. The Debugger panel allows to set breakpoints (via context |
|
36 |
menu), step through stopped threads, evaluate local ML expressions etc. |
|
37 |
At least one Debugger view needs to be active to have any effect on the |
|
38 |
running ML program. |
|
39 |
||
61173 | 40 |
* The main Isabelle executable is managed as single-instance Desktop |
41 |
application uniformly on all platforms: Linux, Windows, Mac OS X. |
|
61170 | 42 |
|
61198 | 43 |
* The text overview column (status of errors, warnings etc.) is updated |
44 |
asynchronously, leading to much better editor reactivity. Moreover, the |
|
45 |
full document node content is taken into account. |
|
46 |
||
61218 | 47 |
* The State panel manages explicit proof state output, with jEdit action |
48 |
"isabelle.update-state" (shortcut S+ENTER) to trigger update according |
|
49 |
to cursor position. Option "editor_output_state" controls implicit proof |
|
50 |
state output in the Output panel: suppressing this reduces resource |
|
51 |
requirements of prover time and GUI space. |
|
61215 | 52 |
|
61483 | 53 |
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
54 |
emphasized text style; the effect is visible in document output, not in |
|
55 |
the editor. |
|
56 |
||
57 |
* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, |
|
58 |
instead of former C+e LEFT. |
|
59 |
||
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
60 |
* New command-line tool "isabelle jedit_client" allows to connect to |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
61 |
already running Isabelle/jEdit process. This achieves the effect of |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
62 |
single-instance applications seen on common GUI desktops. |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
63 |
|
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
64 |
* The command-line tool "isabelle jedit" and the isabelle.Main |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
65 |
application wrapper threat the default $USER_HOME/Scratch.thy more |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
66 |
uniformly, and allow the dummy file argument ":" to open an empty buffer |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
67 |
instead. |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
68 |
|
61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
69 |
* The default look-and-feel for Linux is the traditional "Metal", which |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
70 |
works better with GUI scaling for very high-resolution displays (e.g. |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
71 |
4K). Moreover, it is generally more robust than "Nimbus". |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
72 |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
73 |
|
61405 | 74 |
*** Document preparation *** |
75 |
||
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
76 |
* There is a new short form for antiquotations with a single argument |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
77 |
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
61501 | 78 |
\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The |
79 |
standard Isabelle fonts provide glyphs to render important control |
|
80 |
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
81 |
|
61537
f6bd97a587b7
clarified completion of Isabelle symbols within document source;
wenzelm
parents:
61529
diff
changeset
|
82 |
* System option "document_symbols" determines completion of Isabelle |
f6bd97a587b7
clarified completion of Isabelle symbols within document source;
wenzelm
parents:
61529
diff
changeset
|
83 |
symbols within document source. |
f6bd97a587b7
clarified completion of Isabelle symbols within document source;
wenzelm
parents:
61529
diff
changeset
|
84 |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
85 |
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
86 |
Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
61492 | 87 |
text. Command-line tool "isabelle update_cartouches -t" helps to update |
88 |
old sources, by approximative patching of the content of string and |
|
89 |
cartouche tokens seen in theory sources. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
90 |
|
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
91 |
* The @{text} antiquotation now ignores the antiquotation option |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
92 |
"source". The given text content is output unconditionally, without any |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
93 |
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the |
61494 | 94 |
argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial |
95 |
or terminal spaces are ignored. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
96 |
|
61471 | 97 |
* HTML presentation uses the standard IsabelleText font and Unicode |
98 |
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former |
|
61488 | 99 |
print mode "HTML" loses its special meaning. |
61471 | 100 |
|
61463 | 101 |
* Commands 'paragraph' and 'subparagraph' provide additional section |
102 |
headings. Thus there are 6 levels of standard headings, as in HTML. |
|
103 |
||
104 |
* Text is structured in paragraphs and nested lists, using notation that |
|
105 |
is similar to Markdown. The control symbols for list items are as |
|
106 |
follows: |
|
107 |
||
108 |
\<^item> itemize |
|
109 |
\<^enum> enumerate |
|
110 |
\<^descr> description |
|
111 |
||
112 |
* Text may contain control symbols for markup and formatting as follows: |
|
61405 | 113 |
|
61437 | 114 |
\<^noindent> \noindent |
61405 | 115 |
\<^smallskip> \smallskip |
116 |
\<^medskip> \medskip |
|
117 |
\<^bigskip> \bigskip |
|
118 |
||
61463 | 119 |
* Command 'text_raw' has been clarified: input text is processed as in |
120 |
'text' (with antiquotations and control symbols). The key difference is |
|
121 |
the lack of the surrounding isabelle markup environment in output. |
|
61405 | 122 |
|
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
123 |
* Document antiquotations @{emph} and @{bold} output LaTeX source |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
124 |
recursively, adding appropriate text style markup. These are typically |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
125 |
used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset
|
126 |
|
61405 | 127 |
|
60406 | 128 |
*** Isar *** |
129 |
||
130 |
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
|
131 |
proof body as well, abstracted over relevant parameters. |
|
132 |
||
60477
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset
|
133 |
* Improved type-inference for theorem statement 'obtains': separate |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset
|
134 |
parameter scope for of each clause. |
051b200f7578
improved treatment of Element.Obtains via Expression.prepare_stmt;
wenzelm
parents:
60460
diff
changeset
|
135 |
|
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset
|
136 |
* Term abbreviations via 'is' patterns also work for schematic |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset
|
137 |
statements: result is abstracted over unknowns. |
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60406
diff
changeset
|
138 |
|
60414 | 139 |
* Local goals ('have', 'show', 'hence', 'thus') allow structured |
140 |
statements like fixes/assumes/shows in theorem specifications, but the |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
141 |
notation is postfix with keywords 'if' (or 'when') and 'for'. For |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
142 |
example: |
60414 | 143 |
|
144 |
have result: "C x y" |
|
145 |
if "A x" and "B y" |
|
146 |
for x :: 'a and y :: 'a |
|
147 |
<proof> |
|
148 |
||
60449 | 149 |
The local assumptions are bound to the name "that". The result is |
150 |
exported from context of the statement as usual. The above roughly |
|
60414 | 151 |
corresponds to a raw proof block like this: |
152 |
||
153 |
{ |
|
154 |
fix x :: 'a and y :: 'a |
|
60449 | 155 |
assume that: "A x" "B y" |
60414 | 156 |
have "C x y" <proof> |
157 |
} |
|
158 |
note result = this |
|
60406 | 159 |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
160 |
The keyword 'when' may be used instead of 'if', to indicate 'presume' |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
161 |
instead of 'assume' above. |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
162 |
|
60595 | 163 |
* The meaning of 'show' with Pure rule statements has changed: premises |
164 |
are treated in the sense of 'assume', instead of 'presume'. This means, |
|
165 |
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows: |
|
166 |
||
167 |
show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
168 |
||
169 |
or: |
|
170 |
||
171 |
show "C x" if "A x" "B x" for x |
|
172 |
||
173 |
Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: |
|
174 |
||
175 |
show "C x" when "A x" "B x" for x |
|
176 |
||
60406 | 177 |
* New command 'supply' supports fact definitions during goal refinement |
178 |
('apply' scripts). |
|
179 |
||
60459 | 180 |
* New command 'consider' states rules for generalized elimination and |
181 |
case splitting. This is like a toplevel statement "theorem obtains" used |
|
182 |
within a proof body; or like a multi-branch 'obtain' without activation |
|
183 |
of the local context elements yet. |
|
184 |
||
60455 | 185 |
* Proof method "cases" allows to specify the rule as first entry of |
186 |
chained facts. This is particularly useful with 'consider': |
|
187 |
||
188 |
consider (a) A | (b) B | (c) C <proof> |
|
189 |
then have something |
|
190 |
proof cases |
|
191 |
case a |
|
192 |
then show ?thesis <proof> |
|
193 |
next |
|
194 |
case b |
|
195 |
then show ?thesis <proof> |
|
196 |
next |
|
197 |
case c |
|
198 |
then show ?thesis <proof> |
|
199 |
qed |
|
200 |
||
60565 | 201 |
* Command 'case' allows fact name and attribute specification like this: |
202 |
||
203 |
case a: (c xs) |
|
204 |
case a [attributes]: (c xs) |
|
205 |
||
206 |
Facts that are introduced by invoking the case context are uniformly |
|
207 |
qualified by "a"; the same name is used for the cumulative fact. The old |
|
208 |
form "case (c xs) [attributes]" is no longer supported. Rare |
|
209 |
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, |
|
210 |
and always put attributes in front. |
|
211 |
||
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
212 |
* The standard proof method of commands 'proof' and '..' is now called |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
213 |
"standard" to make semantically clear what it is; the old name "default" |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
214 |
is still available as legacy for some time. Documentation now explains |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
215 |
'..' more accurately as "by standard" instead of "by rule". |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
216 |
|
60631 | 217 |
* Command 'subgoal' allows to impose some structure on backward |
218 |
refinements, to avoid proof scripts degenerating into long of 'apply' |
|
219 |
sequences. Further explanations and examples are given in the isar-ref |
|
220 |
manual. |
|
221 |
||
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
222 |
* Proof method "goal_cases" turns the current subgoals into cases within |
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
223 |
the context; the conclusion is bound to variable ?case in each case. For |
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
224 |
example: |
60617 | 225 |
|
226 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
60622 | 227 |
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" |
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
228 |
proof goal_cases |
60622 | 229 |
case (1 x) |
230 |
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry |
|
231 |
next |
|
232 |
case (2 y z) |
|
233 |
then show ?case using \<open>U y\<close> \<open>V z\<close> sorry |
|
234 |
qed |
|
235 |
||
236 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
237 |
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" |
|
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
238 |
proof goal_cases |
60617 | 239 |
case prems: 1 |
240 |
then show ?case using prems sorry |
|
241 |
next |
|
242 |
case prems: 2 |
|
243 |
then show ?case using prems sorry |
|
244 |
qed |
|
60578 | 245 |
|
60581 | 246 |
* The undocumented feature of implicit cases goal1, goal2, goal3, etc. |
60617 | 247 |
is marked as legacy, and will be removed eventually. The proof method |
248 |
"goals" achieves a similar effect within regular Isar; often it can be |
|
249 |
done more adequately by other means (e.g. 'consider'). |
|
60581 | 250 |
|
60551 | 251 |
* Nesting of Isar goal structure has been clarified: the context after |
252 |
the initial backwards refinement is retained for the whole proof, within |
|
253 |
all its context sections (as indicated via 'next'). This is e.g. |
|
254 |
relevant for 'using', 'including', 'supply': |
|
255 |
||
256 |
have "A \<and> A" if a: A for A |
|
257 |
supply [simp] = a |
|
258 |
proof |
|
259 |
show A by simp |
|
260 |
next |
|
261 |
show A by simp |
|
262 |
qed |
|
263 |
||
60554 | 264 |
* Method "sleep" succeeds after a real-time delay (in seconds). This is |
265 |
occasionally useful for demonstration and testing purposes. |
|
266 |
||
60406 | 267 |
|
60331 | 268 |
*** Pure *** |
269 |
||
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
270 |
* Qualifiers in locale expressions default to mandatory ('!') |
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
271 |
regardless of the command. Previously, for 'locale' and 'sublocale' |
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
272 |
the default was optional ('?'). INCOMPATIBILITY |
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
273 |
|
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
274 |
* Keyword 'rewrites' identifies rewrite morphisms in interpretation |
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
275 |
commands. Previously, the keyword was 'where'. INCOMPATIBILITY |
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
276 |
|
61252 | 277 |
* Command 'print_definitions' prints dependencies of definitional |
278 |
specifications. This functionality used to be part of 'print_theory'. |
|
279 |
||
60489 | 280 |
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` |
281 |
as well, not just "by this" or "." as before. |
|
282 |
||
60331 | 283 |
* Configuration option rule_insts_schematic has been discontinued |
284 |
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. |
|
285 |
||
60347 | 286 |
* Abbreviations in type classes now carry proper sort constraint. |
287 |
Rare INCOMPATIBILITY in situations where the previous misbehaviour |
|
61228 | 288 |
has been exploited. |
60347 | 289 |
|
290 |
* Refinement of user-space type system in type classes: pseudo-local |
|
291 |
operations behave more similar to abbreviations. Potential |
|
292 |
INCOMPATIBILITY in exotic situations. |
|
293 |
||
294 |
||
60171 | 295 |
*** HOL *** |
296 |
||
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
297 |
* Combinator to represent case distinction on products is named "case_prod", |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
298 |
uniformly, discontinuing any input aliasses. Very popular theorem aliasses |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
299 |
have been retained. |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
300 |
Consolidated facts: |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
301 |
PairE ~> prod.exhaust |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
302 |
Pair_eq ~> prod.inject |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
303 |
pair_collapse ~> prod.collapse |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
304 |
Pair_fst_snd_eq ~> prod_eq_iff |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
305 |
split_twice ~> prod.case_distrib |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
306 |
split_weak_cong ~> prod.case_cong_weak |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
307 |
split_split ~> prod.split |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
308 |
split_split_asm ~> prod.split_asm |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
309 |
splitI ~> case_prodI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
310 |
splitD ~> case_prodD |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
311 |
splitI2 ~> case_prodI2 |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
312 |
splitI2' ~> case_prodI2' |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
313 |
splitE ~> case_prodE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
314 |
splitE' ~> case_prodE' |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
315 |
split_pair ~> case_prod_Pair |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
316 |
split_eta ~> case_prod_eta |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
317 |
split_comp ~> case_prod_comp |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
318 |
mem_splitI ~> mem_case_prodI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
319 |
mem_splitI2 ~> mem_case_prodI2 |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
320 |
mem_splitE ~> mem_case_prodE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
321 |
The_split ~> The_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
322 |
cond_split_eta ~> cond_case_prod_eta |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
323 |
Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
324 |
Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
325 |
in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
326 |
Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
327 |
Collect_split_Grp_inD ~> Collect_case_prod_Grp_in |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
328 |
Domain_Collect_split ~> Domain_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
329 |
Image_Collect_split ~> Image_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
330 |
Range_Collect_split ~> Range_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
331 |
Eps_split ~> Eps_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
332 |
Eps_split_eq ~> Eps_case_prod_eq |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
333 |
split_rsp ~> case_prod_rsp |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
334 |
curry_split ~> curry_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
335 |
split_curry ~> case_prod_curry |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
336 |
Changes in structure HOLogic: |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
337 |
split_const ~> case_prod_const |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
338 |
mk_split ~> mk_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
339 |
mk_psplits ~> mk_ptupleabs |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
340 |
strip_psplits ~> strip_ptupleabs |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
341 |
INCOMPATIBILITY. |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
342 |
|
61308 | 343 |
* Commands 'inductive' and 'inductive_set' work better when names for |
344 |
intro rules are omitted: the "cases" and "induct" rules no longer |
|
345 |
declare empty case_names, but no case_names at all. This allows to use |
|
346 |
numbered cases in proofs, without requiring method "goal_cases". |
|
347 |
||
61269
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
348 |
* The 'typedef' command has been upgraded from a partially checked |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
349 |
"axiomatization", to a full definitional specification that takes the |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
350 |
global collection of overloaded constant / type definitions into |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
351 |
account. Type definitions with open dependencies on overloaded |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
352 |
definitions need to be specified as "typedef (overloaded)". This |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
353 |
provides extra robustness in theory construction. Rare INCOMPATIBILITY. |
64a5bce1f498
documentation for "Semantic subtype definitions";
wenzelm
parents:
61268
diff
changeset
|
354 |
|
61118 | 355 |
* Qualification of various formal entities in the libraries is done more |
356 |
uniformly via "context begin qualified definition ... end" instead of |
|
357 |
old-style "hide_const (open) ...". Consequently, both the defined |
|
358 |
constant and its defining fact become qualified, e.g. Option.is_none and |
|
359 |
Option.is_none_def. Occasional INCOMPATIBILITY in applications. |
|
360 |
||
61069 | 361 |
* Some old and rarely used ASCII replacement syntax has been removed. |
362 |
INCOMPATIBILITY, standard syntax with symbols should be used instead. |
|
363 |
The subsequent commands help to reproduce the old forms, e.g. to |
|
364 |
simplify porting old theories: |
|
365 |
||
366 |
type_notation Map.map (infixr "~=>" 0) |
|
367 |
notation Map.map_comp (infixl "o'_m" 55) |
|
368 |
||
61384 | 369 |
type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) |
370 |
||
371 |
notation FuncSet.funcset (infixr "->" 60) |
|
372 |
notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) |
|
373 |
||
374 |
notation Omega_Words_Fun.conc (infixr "conc" 65) |
|
375 |
||
376 |
notation Preorder.equiv ("op ~~") |
|
377 |
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
|
378 |
||
61143 | 379 |
* The alternative notation "\<Colon>" for type and sort constraints has been |
380 |
removed: in LaTeX document output it looks the same as "::". |
|
381 |
INCOMPATIBILITY, use plain "::" instead. |
|
382 |
||
60841 | 383 |
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has |
384 |
been removed. INCOMPATIBILITY. |
|
385 |
||
60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset
|
386 |
* Quickcheck setup for finite sets. |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset
|
387 |
|
60171 | 388 |
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. |
60138 | 389 |
|
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
390 |
* Sledgehammer: |
61318 | 391 |
- The MaSh relevance filter has been sped up. |
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
392 |
- Proof reconstruction has been improved, to minimize the incidence of |
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
393 |
cases where Sledgehammer gives a proof that does not work. |
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
394 |
- Auto Sledgehammer now minimizes and preplays the results. |
61030 | 395 |
- Handle Vampire 4.0 proof output without raising exception. |
61043 | 396 |
- Eliminated "MASH" environment variable. Use the "MaSh" option in |
397 |
Isabelle/jEdit instead. INCOMPATIBILITY. |
|
61317 | 398 |
- Eliminated obsolete "blocking" option and related subcommands. |
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
399 |
|
60310 | 400 |
* Nitpick: |
61325
1cfc476198c9
avoid too aggressive optimization of 'finite' predicate
blanchet
parents:
61324
diff
changeset
|
401 |
- Fixed soundness bug in translation of "finite" predicate. |
61324
d4ec7594f558
avoid unsound simplification of (C (s x)) when s is a selector but not C's
blanchet
parents:
61318
diff
changeset
|
402 |
- Fixed soundness bug in "destroy_constrs" optimization. |
60310 | 403 |
- Removed "check_potential" and "check_genuine" options. |
61317 | 404 |
- Eliminated obsolete "blocking" option. |
60310 | 405 |
|
61345 | 406 |
* New (co)datatype package: |
407 |
- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
|
408 |
structure on the raw type to an abstract type defined using typedef. |
|
409 |
- Always generate "case_transfer" theorem. |
|
61551 | 410 |
- Allow discriminators and selectors with the same name as the type |
411 |
being defined. |
|
412 |
- Avoid various internal name clashes (e.g., 'datatype f = f'). |
|
60920 | 413 |
|
61370 | 414 |
* Transfer: |
61426
d53db136e8fd
new material on path_component_sets, inside, outside, etc. And more default simprules
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset
|
415 |
- new methods for interactive debugging of 'transfer' and |
61370 | 416 |
'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', |
417 |
'transfer_prover_start' and 'transfer_prover_end'. |
|
418 |
||
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
419 |
* Division on integers is bootstrapped directly from division on |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
420 |
naturals and uses generic numeral algorithm for computations. |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
421 |
Slight INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
422 |
former simprocs binary_int_div and binary_int_mod |
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
423 |
|
60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
424 |
* Tightened specification of class semiring_no_zero_divisors. Slight |
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
425 |
INCOMPATIBILITY. |
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
426 |
|
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
427 |
* Class algebraic_semidom introduces common algebraic notions of |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
428 |
integral (semi)domains, particularly units. Although |
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset
|
429 |
logically subsumed by fields, is is not a super class of these |
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset
|
430 |
in order not to burden fields with notions that are trivial there. |
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
431 |
|
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
432 |
* Class normalization_semidom specifies canonical representants |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
433 |
for equivalence classes of associated elements in an integral |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
434 |
(semi)domain. This formalizes associated elements as well. |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
435 |
|
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
436 |
* Abstract specification of gcd/lcm operations in classes semiring_gcd, |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
437 |
semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
438 |
and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
439 |
and gcd_int.assoc by gcd.assoc. |
60517
f16e4fb20652
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
haftmann
parents:
60516
diff
changeset
|
440 |
|
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset
|
441 |
* Former constants Fields.divide (_ / _) and Divides.div (_ div _) |
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
60347
diff
changeset
|
442 |
are logically unified to Rings.divide in syntactic type class |
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset
|
443 |
Rings.divide, with infix syntax (_ div _). Infix syntax (_ / _) |
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset
|
444 |
for field division is added later as abbreviation in class Fields.inverse. |
60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
445 |
INCOMPATIBILITY, instantiations must refer to Rings.divide rather |
60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset
|
446 |
than the former separate constants, hence infix syntax (_ / _) is usually |
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60418
diff
changeset
|
447 |
not available during instantiation. |
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
60347
diff
changeset
|
448 |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
449 |
* Library/Multiset: |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
450 |
- Renamed multiset inclusion operators: |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
451 |
< ~> <# |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
452 |
\<subset> ~> \<subset># |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
453 |
<= ~> <=# |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
454 |
\<le> ~> \<le># |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
455 |
\<subseteq> ~> \<subseteq># |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
456 |
INCOMPATIBILITY. |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
457 |
- "'a multiset" is no longer an instance of the "order", |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
458 |
"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff", |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
459 |
"semilattice_inf", and "semilattice_sup" type classes. The theorems |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
460 |
previously provided by these type classes (directly or indirectly) |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
461 |
are now available through the "subset_mset" interpretation |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
462 |
(e.g. add_mono ~> subset_mset.add_mono). |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
463 |
INCOMPATIBILITY. |
60497 | 464 |
- Renamed conversions: |
60515 | 465 |
multiset_of ~> mset |
466 |
multiset_of_set ~> mset_set |
|
60497 | 467 |
set_of ~> set_mset |
468 |
INCOMPATIBILITY |
|
60398 | 469 |
- Renamed lemmas: |
470 |
mset_le_def ~> subseteq_mset_def |
|
471 |
mset_less_def ~> subset_mset_def |
|
60400 | 472 |
less_eq_multiset.rep_eq ~> subseteq_mset_def |
473 |
INCOMPATIBILITY |
|
474 |
- Removed lemmas generated by lift_definition: |
|
475 |
less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer |
|
476 |
less_eq_multiset_def |
|
477 |
INCOMPATIBILITY |
|
60006 | 478 |
|
61520
8f85bb443d33
Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents:
61512
diff
changeset
|
479 |
* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's |
8f85bb443d33
Cauchy's integral formula, required lemmas, and a bit of reorganisation
paulson <lp15@cam.ac.uk>
parents:
61512
diff
changeset
|
480 |
integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light |
61426
d53db136e8fd
new material on path_component_sets, inside, outside, etc. And more default simprules
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset
|
481 |
|
d53db136e8fd
new material on path_component_sets, inside, outside, etc. And more default simprules
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset
|
482 |
* Multivariate_Analysis: Added topological concepts such as connected components |
d53db136e8fd
new material on path_component_sets, inside, outside, etc. And more default simprules
paulson <lp15@cam.ac.uk>
parents:
61424
diff
changeset
|
483 |
and the inside or outside of a set. |
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60802
diff
changeset
|
484 |
|
60523 | 485 |
* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
486 |
command. Minor INCOMPATIBILITY, use 'function' instead. |
|
487 |
||
61121
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
488 |
* Recursive function definitions ('fun', 'function', 'partial_function') |
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
489 |
no longer expose the low-level "_def" facts of the internal |
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
490 |
construction. INCOMPATIBILITY, enable option "function_defs" in the |
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
491 |
context for rare situations where these facts are really needed. |
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
492 |
|
61119 | 493 |
* Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
494 |
||
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset
|
495 |
* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. |
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset
|
496 |
|
60479 | 497 |
|
60793 | 498 |
*** ML *** |
499 |
||
61268 | 500 |
* The auxiliary module Pure/display.ML has been eliminated. Its |
501 |
elementary thm print operations are now in Pure/more_thm.ML and thus |
|
502 |
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. |
|
503 |
||
61144 | 504 |
* Simproc programming interfaces have been simplified: |
505 |
Simplifier.make_simproc and Simplifier.define_simproc supersede various |
|
506 |
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
|
507 |
term patterns for the left-hand sides are specified with implicitly |
|
508 |
fixed variables, like top-level theorem statements. INCOMPATIBILITY. |
|
509 |
||
60802 | 510 |
* Instantiation rules have been re-organized as follows: |
511 |
||
512 |
Thm.instantiate (*low-level instantiation with named arguments*) |
|
513 |
Thm.instantiate' (*version with positional arguments*) |
|
514 |
||
515 |
Drule.infer_instantiate (*instantiation with type inference*) |
|
516 |
Drule.infer_instantiate' (*version with positional arguments*) |
|
517 |
||
518 |
The LHS only requires variable specifications, instead of full terms. |
|
519 |
Old cterm_instantiate is superseded by infer_instantiate. |
|
520 |
INCOMPATIBILITY, need to re-adjust some ML names and types accordingly. |
|
521 |
||
60793 | 522 |
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been |
523 |
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. |
|
524 |
instead (with proper context). |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
525 |
|
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
526 |
* Thm.instantiate (and derivatives) no longer require the LHS of the |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
527 |
instantiation to be certified: plain variables are given directly. |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
528 |
|
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
529 |
* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
530 |
quasi-bound variables (like the Simplifier), instead of accidentally |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
531 |
named local fixes. This has the potential to improve stability of proof |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
532 |
tools, but can also cause INCOMPATIBILITY for tools that don't observe |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
533 |
the proof context discipline. |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
534 |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
535 |
|
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
536 |
*** System *** |
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
537 |
|
61174 | 538 |
* Property values in etc/symbols may contain spaces, if written with the |
539 |
replacement character "␣" (Unicode point 0x2324). For example: |
|
540 |
||
541 |
\<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
|
542 |
||
61216 | 543 |
* Command-line tool "isabelle update_then" expands old Isar command |
544 |
conflations: |
|
545 |
||
546 |
hence ~> then have |
|
547 |
thus ~> then show |
|
548 |
||
549 |
This syntax is more orthogonal and improves readability and |
|
550 |
maintainability of proofs. |
|
551 |
||
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset
|
552 |
* Poly/ML default platform architecture may be changed from 32bit to |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset
|
553 |
64bit via system option ML_system_64. A system restart (and rebuild) |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset
|
554 |
is required after change. |
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61149
diff
changeset
|
555 |
|
61074 | 556 |
* Poly/ML 5.5.3 runs natively on x86-windows and x86_64-windows, |
557 |
which both allow larger heap space than former x86-cygwin. |
|
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
558 |
|
60995
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
559 |
* Java runtime environment for x86_64-windows allows to use larger heap |
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
560 |
space. |
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
561 |
|
61135
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
562 |
* Java runtime options are determined separately for 32bit vs. 64bit |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
563 |
platforms as follows. |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
564 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
565 |
- Isabelle desktop application: platform-specific files that are |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
566 |
associated with the main app bundle |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
567 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
568 |
- isabelle jedit: settings |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
569 |
JEDIT_JAVA_SYSTEM_OPTIONS |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
570 |
JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64 |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
571 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
572 |
- isabelle build: settings |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
573 |
ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64 |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
574 |
|
61294 | 575 |
* Bash shell function "jvmpath" has been renamed to "platform_path": it |
576 |
is relevant both for Poly/ML and JVM processes. |
|
577 |
||
61567 | 578 |
* Heap images are 10-15% smaller due to less wasteful persistent theory |
579 |
content (using ML type theory_id instead of theory); |
|
580 |
||
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
581 |
|
60479 | 582 |
|
60009 | 583 |
New in Isabelle2015 (May 2015) |
584 |
------------------------------ |
|
57695 | 585 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
586 |
*** General *** |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
587 |
|
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset
|
588 |
* Local theory specification commands may have a 'private' or |
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
589 |
'qualified' modifier to restrict name space accesses to the local scope, |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset
|
590 |
as provided by some "context begin ... end" block. For example: |
59926 | 591 |
|
592 |
context |
|
593 |
begin |
|
594 |
||
595 |
private definition ... |
|
596 |
private lemma ... |
|
597 |
||
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
598 |
qualified definition ... |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
599 |
qualified lemma ... |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
600 |
|
59926 | 601 |
lemma ... |
602 |
theorem ... |
|
603 |
||
604 |
end |
|
605 |
||
59901 | 606 |
* Command 'experiment' opens an anonymous locale context with private |
607 |
naming policy. |
|
608 |
||
59951 | 609 |
* Command 'notepad' requires proper nesting of begin/end and its proof |
610 |
structure in the body: 'oops' is no longer supported here. Minor |
|
611 |
INCOMPATIBILITY, use 'sorry' instead. |
|
612 |
||
613 |
* Command 'named_theorems' declares a dynamic fact within the context, |
|
614 |
together with an attribute to maintain the content incrementally. This |
|
615 |
supersedes functor Named_Thms in Isabelle/ML, but with a subtle change |
|
616 |
of semantics due to external visual order vs. internal reverse order. |
|
617 |
||
618 |
* 'find_theorems': search patterns which are abstractions are |
|
619 |
schematically expanded before search. Search results match the naive |
|
620 |
expectation more closely, particularly wrt. abbreviations. |
|
621 |
INCOMPATIBILITY. |
|
59648 | 622 |
|
59569 | 623 |
* Commands 'method_setup' and 'attribute_setup' now work within a local |
624 |
theory context. |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
625 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
626 |
* Outer syntax commands are managed authentically within the theory |
59569 | 627 |
context, without implicit global state. Potential for accidental |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
628 |
INCOMPATIBILITY, make sure that required theories are really imported. |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
629 |
|
60115 | 630 |
* Historical command-line terminator ";" is no longer accepted (and |
631 |
already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle |
|
632 |
update_semicolons" to remove obsolete semicolons from old theory |
|
633 |
sources. |
|
634 |
||
59951 | 635 |
* Structural composition of proof methods (meth1; meth2) in Isar |
636 |
corresponds to (tac1 THEN_ALL_NEW tac2) in ML. |
|
59105 | 637 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
638 |
* The Eisbach proof method language allows to define new proof methods |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
639 |
by combining existing ones with their usual syntax. The "match" proof |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
640 |
method provides basic fact/term matching in addition to |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
641 |
premise/conclusion matching through Subgoal.focus, and binds fact names |
60288
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
642 |
from matches as well as term patterns within matches. The Isabelle |
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
643 |
documentation provides an entry "eisbach" for the Eisbach User Manual. |
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
644 |
Sources and various examples are in ~~/src/HOL/Eisbach/. |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
645 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
646 |
|
58524 | 647 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
648 |
||
59569 | 649 |
* Improved folding mode "isabelle" based on Isar syntax. Alternatively, |
650 |
the "sidekick" mode may be used for document structure. |
|
651 |
||
652 |
* Extended bracket matching based on Isar language structure. System |
|
653 |
option jedit_structure_limit determines maximum number of lines to scan |
|
654 |
in the buffer. |
|
58758 | 655 |
|
58540 | 656 |
* Support for BibTeX files: context menu, context-sensitive token |
657 |
marker, SideKick parser. |
|
58524 | 658 |
|
58551 | 659 |
* Document antiquotation @{cite} provides formal markup, which is |
60265 | 660 |
interpreted semi-formally based on .bib files that happen to be open in |
661 |
the editor (hyperlinks, completion etc.). |
|
58551 | 662 |
|
58785 | 663 |
* Less waste of vertical space via negative line spacing (see Global |
664 |
Options / Text Area). |
|
665 |
||
60089
8bd5999133d4
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
wenzelm
parents:
60085
diff
changeset
|
666 |
* Improved graphview panel with optional output of PNG or PDF, for |
60273
83de10e27007
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
wenzelm
parents:
60265
diff
changeset
|
667 |
display of 'thy_deps', 'class_deps' etc. |
60009 | 668 |
|
60115 | 669 |
* The commands 'thy_deps' and 'class_deps' allow optional bounds to |
670 |
restrict the visualized hierarchy. |
|
60093 | 671 |
|
60072 | 672 |
* Improved scheduling for asynchronous print commands (e.g. provers |
673 |
managed by the Sledgehammer panel) wrt. ongoing document processing. |
|
674 |
||
58524 | 675 |
|
59951 | 676 |
*** Document preparation *** |
677 |
||
678 |
* Document markup commands 'chapter', 'section', 'subsection', |
|
679 |
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any |
|
680 |
context, even before the initial 'theory' command. Obsolete proof |
|
681 |
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been |
|
682 |
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' |
|
683 |
instead. The old 'header' command is still retained for some time, but |
|
684 |
should be replaced by 'chapter', 'section' etc. (using "isabelle |
|
685 |
update_header"). Minor INCOMPATIBILITY. |
|
686 |
||
60009 | 687 |
* Official support for "tt" style variants, via \isatt{...} or |
688 |
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or |
|
689 |
verbatim environment of LaTeX is no longer used. This allows @{ML} etc. |
|
690 |
as argument to other macros (such as footnotes). |
|
691 |
||
692 |
* Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
|
693 |
style. |
|
694 |
||
695 |
* Discontinued obsolete option "document_graph": session_graph.pdf is |
|
696 |
produced unconditionally for HTML browser_info and PDF-LaTeX document. |
|
697 |
||
59951 | 698 |
* Diagnostic commands and document markup commands within a proof do not |
699 |
affect the command tag for output. Thus commands like 'thm' are subject |
|
700 |
to proof document structure, and no longer "stick out" accidentally. |
|
701 |
Commands 'text' and 'txt' merely differ in the LaTeX style, not their |
|
702 |
tags. Potential INCOMPATIBILITY in exotic situations. |
|
703 |
||
704 |
* System option "pretty_margin" is superseded by "thy_output_margin", |
|
705 |
which is also accessible via document antiquotation option "margin". |
|
706 |
Only the margin for document output may be changed, but not the global |
|
707 |
pretty printing: that is 76 for plain console output, and adapted |
|
708 |
dynamically in GUI front-ends. Implementations of document |
|
709 |
antiquotations need to observe the margin explicitly according to |
|
710 |
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. |
|
711 |
||
60299
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
712 |
* Specification of 'document_files' in the session ROOT file is |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
713 |
mandatory for document preparation. The legacy mode with implicit |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
714 |
copying of the document/ directory is no longer supported. Minor |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
715 |
INCOMPATIBILITY. |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
716 |
|
59951 | 717 |
|
58202 | 718 |
*** Pure *** |
719 |
||
59835
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
720 |
* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
721 |
etc.) allow an optional context of local variables ('for' declaration): |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
722 |
these variables become schematic in the instantiated theorem; this |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
723 |
behaviour is analogous to 'for' in attributes "where" and "of". |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
724 |
Configuration option rule_insts_schematic (default false) controls use |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
725 |
of schematic variables outside the context. Minor INCOMPATIBILITY, |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
726 |
declare rule_insts_schematic = true temporarily and update to use local |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
727 |
variable declarations or dummy patterns instead. |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
728 |
|
60009 | 729 |
* Explicit instantiation via attributes "where", "of", and proof methods |
730 |
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns |
|
731 |
("_") that stand for anonymous local variables. |
|
732 |
||
59951 | 733 |
* Generated schematic variables in standard format of exported facts are |
734 |
incremented to avoid material in the proof context. Rare |
|
735 |
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to |
|
736 |
different index. |
|
737 |
||
60010 | 738 |
* Lexical separation of signed and unsigned numerals: categories "num" |
739 |
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence |
|
740 |
of numeral signs, particularly in expressions involving infix syntax |
|
741 |
like "(- 1) ^ n". |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset
|
742 |
|
58421 | 743 |
* Old inner token category "xnum" has been discontinued. Potential |
744 |
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
|
745 |
token category instead. |
|
746 |
||
58202 | 747 |
|
57737 | 748 |
*** HOL *** |
749 |
||
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
750 |
* New (co)datatype package: |
58373 | 751 |
- The 'datatype_new' command has been renamed 'datatype'. The old |
752 |
command of that name is now called 'old_datatype' and is provided |
|
753 |
by "~~/src/HOL/Library/Old_Datatype.thy". See |
|
754 |
'isabelle doc datatypes' for information on porting. |
|
755 |
INCOMPATIBILITY. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
756 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
757 |
disc_corec ~> corec_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
758 |
disc_corec_iff ~> corec_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
759 |
disc_exclude ~> distinct_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
760 |
disc_exhaust ~> exhaust_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
761 |
disc_map_iff ~> map_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
762 |
sel_corec ~> corec_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
763 |
sel_exhaust ~> exhaust_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
764 |
sel_map ~> map_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
765 |
sel_set ~> set_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
766 |
sel_split ~> split_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
767 |
sel_split_asm ~> split_sel_asm |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
768 |
strong_coinduct ~> coinduct_strong |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
769 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
770 |
INCOMPATIBILITY. |
58192 | 771 |
- The "no_code" option to "free_constructors", "datatype_new", and |
772 |
"codatatype" has been renamed "plugins del: code". |
|
773 |
INCOMPATIBILITY. |
|
58044 | 774 |
- The rules "set_empty" have been removed. They are easy |
775 |
consequences of other set rules "by auto". |
|
776 |
INCOMPATIBILITY. |
|
777 |
- The rule "set_cases" is now registered with the "[cases set]" |
|
57990 | 778 |
attribute. This can influence the behavior of the "cases" proof |
779 |
method when more than one case rule is applicable (e.g., an |
|
780 |
assumption is of the form "w : set ws" and the method "cases w" |
|
781 |
is invoked). The solution is to specify the case rule explicitly |
|
782 |
(e.g. "cases w rule: widget.exhaust"). |
|
783 |
INCOMPATIBILITY. |
|
59675 | 784 |
- Renamed theories: |
785 |
BNF_Comp ~> BNF_Composition |
|
786 |
BNF_FP_Base ~> BNF_Fixpoint_Base |
|
787 |
BNF_GFP ~> BNF_Greatest_Fixpoint |
|
788 |
BNF_LFP ~> BNF_Least_Fixpoint |
|
789 |
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions |
|
790 |
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions |
|
791 |
INCOMPATIBILITY. |
|
60114 | 792 |
- Lifting and Transfer setup for basic HOL types sum and prod (also |
793 |
option) is now performed by the BNF package. Theories Lifting_Sum, |
|
794 |
Lifting_Product and Lifting_Option from Main became obsolete and |
|
795 |
were removed. Changed definitions of the relators rel_prod and |
|
796 |
rel_sum (using inductive). |
|
60111 | 797 |
INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead |
60114 | 798 |
of rel_prod_def and rel_sum_def. |
799 |
Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names |
|
800 |
changed (e.g. map_prod_transfer ~> prod.map_transfer). |
|
60261 | 801 |
- Parametricity theorems for map functions, relators, set functions, |
802 |
constructors, case combinators, discriminators, selectors and |
|
803 |
(co)recursors are automatically proved and registered as transfer |
|
804 |
rules. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
805 |
|
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
806 |
* Old datatype package: |
58310 | 807 |
- The old 'datatype' command has been renamed 'old_datatype', and |
58373 | 808 |
'rep_datatype' has been renamed 'old_rep_datatype'. They are |
809 |
provided by "~~/src/HOL/Library/Old_Datatype.thy". See |
|
58310 | 810 |
'isabelle doc datatypes' for information on porting. |
58373 | 811 |
INCOMPATIBILITY. |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
812 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
813 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
814 |
INCOMPATIBILITY. |
58373 | 815 |
- Renamed theory: |
816 |
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy |
|
817 |
INCOMPATIBILITY. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
818 |
|
59039 | 819 |
* Nitpick: |
60010 | 820 |
- Fixed soundness bug related to the strict and non-strict subset |
59039 | 821 |
operations. |
822 |
||
57737 | 823 |
* Sledgehammer: |
59511 | 824 |
- CVC4 is now included with Isabelle instead of CVC3 and run by |
825 |
default. |
|
59965 | 826 |
- Z3 is now always enabled by default, now that it is fully open |
827 |
source. The "z3_non_commercial" option is discontinued. |
|
57737 | 828 |
- Minimization is now always enabled by default. |
60010 | 829 |
Removed sub-command: |
57737 | 830 |
min |
59967 | 831 |
- Proof reconstruction, both one-liners and Isar, has been |
59039 | 832 |
dramatically improved. |
833 |
- Improved support for CVC4 and veriT. |
|
57737 | 834 |
|
58062 | 835 |
* Old and new SMT modules: |
58067 | 836 |
- The old 'smt' method has been renamed 'old_smt' and moved to |
59569 | 837 |
'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, |
838 |
until applications have been ported to use the new 'smt' method. For |
|
839 |
the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must |
|
840 |
be installed, and the environment variable "OLD_Z3_SOLVER" must |
|
841 |
point to it. |
|
58062 | 842 |
INCOMPATIBILITY. |
58067 | 843 |
- The 'smt2' method has been renamed 'smt'. |
58060 | 844 |
INCOMPATIBILITY. |
59569 | 845 |
- New option 'smt_reconstruction_step_timeout' to limit the |
846 |
reconstruction time of Z3 proof steps in the new 'smt' method. |
|
59216 | 847 |
- New option 'smt_statistics' to display statistics of the new 'smt' |
848 |
method, especially runtime statistics of Z3 proof reconstruction. |
|
58060 | 849 |
|
60261 | 850 |
* Lifting: command 'lift_definition' allows to execute lifted constants |
851 |
that have as a return type a datatype containing a subtype. This |
|
852 |
overcomes long-time limitations in the area of code generation and |
|
853 |
lifting, and avoids tedious workarounds. |
|
60258 | 854 |
|
60009 | 855 |
* Command and antiquotation "value" provide different evaluation slots |
856 |
(again), where the previous strategy (NBE after ML) serves as default. |
|
857 |
Minor INCOMPATIBILITY. |
|
858 |
||
859 |
* Add NO_MATCH-simproc, allows to check for syntactic non-equality. |
|
860 |
||
861 |
* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid |
|
862 |
non-termination in case of distributing a division. With this change |
|
863 |
field_simps is in some cases slightly less powerful, if it fails try to |
|
864 |
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. |
|
865 |
||
866 |
* Separate class no_zero_divisors has been given up in favour of fully |
|
867 |
algebraic semiring_no_zero_divisors. INCOMPATIBILITY. |
|
868 |
||
869 |
* Class linordered_semidom really requires no zero divisors. |
|
870 |
INCOMPATIBILITY. |
|
871 |
||
872 |
* Classes division_ring, field and linordered_field always demand |
|
873 |
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, |
|
874 |
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. |
|
875 |
||
876 |
* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit |
|
877 |
additive inverse operation. INCOMPATIBILITY. |
|
878 |
||
60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60010
diff
changeset
|
879 |
* Complex powers and square roots. The functions "ln" and "powr" are now |
60025 | 880 |
overloaded for types real and complex, and 0 powr y = 0 by definition. |
881 |
INCOMPATIBILITY: type constraints may be necessary. |
|
60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60010
diff
changeset
|
882 |
|
60009 | 883 |
* The functions "sin" and "cos" are now defined for any type of sort |
884 |
"{real_normed_algebra_1,banach}" type, so in particular on "real" and |
|
885 |
"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be |
|
886 |
needed. |
|
887 |
||
888 |
* New library of properties of the complex transcendental functions sin, |
|
889 |
cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. |
|
890 |
||
891 |
* The factorial function, "fact", now has type "nat => 'a" (of a sort |
|
892 |
that admits numeric types including nat, int, real and complex. |
|
893 |
INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type |
|
894 |
constraint, and the combination "real (fact k)" is likely to be |
|
895 |
unsatisfactory. If a type conversion is still necessary, then use |
|
896 |
"of_nat (fact k)" or "real_of_nat (fact k)". |
|
897 |
||
898 |
* Removed functions "natfloor" and "natceiling", use "nat o floor" and |
|
899 |
"nat o ceiling" instead. A few of the lemmas have been retained and |
|
900 |
adapted: in their names "natfloor"/"natceiling" has been replaced by |
|
901 |
"nat_floor"/"nat_ceiling". |
|
902 |
||
903 |
* Qualified some duplicated fact names required for boostrapping the |
|
904 |
type class hierarchy: |
|
905 |
ab_add_uminus_conv_diff ~> diff_conv_add_uminus |
|
906 |
field_inverse_zero ~> inverse_zero |
|
907 |
field_divide_inverse ~> divide_inverse |
|
908 |
field_inverse ~> left_inverse |
|
909 |
Minor INCOMPATIBILITY. |
|
910 |
||
911 |
* Eliminated fact duplicates: |
|
912 |
mult_less_imp_less_right ~> mult_right_less_imp_less |
|
913 |
mult_less_imp_less_left ~> mult_left_less_imp_less |
|
914 |
Minor INCOMPATIBILITY. |
|
915 |
||
916 |
* Fact consolidation: even_less_0_iff is subsumed by |
|
917 |
double_add_less_zero_iff_single_add_less_zero (simp by default anyway). |
|
918 |
||
919 |
* Generalized and consolidated some theorems concerning divsibility: |
|
920 |
dvd_reduce ~> dvd_add_triv_right_iff |
|
921 |
dvd_plus_eq_right ~> dvd_add_right_iff |
|
922 |
dvd_plus_eq_left ~> dvd_add_left_iff |
|
923 |
Minor INCOMPATIBILITY. |
|
924 |
||
925 |
* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" |
|
926 |
and part of theory Main. |
|
927 |
even_def ~> even_iff_mod_2_eq_zero |
|
928 |
INCOMPATIBILITY. |
|
929 |
||
930 |
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor |
|
931 |
INCOMPATIBILITY. |
|
932 |
||
933 |
* Bootstrap of listsum as special case of abstract product over lists. |
|
934 |
Fact rename: |
|
935 |
listsum_def ~> listsum.eq_foldr |
|
936 |
INCOMPATIBILITY. |
|
937 |
||
938 |
* Product over lists via constant "listprod". |
|
939 |
||
940 |
* Theory List: renamed drop_Suc_conv_tl and nth_drop' to |
|
941 |
Cons_nth_drop_Suc. |
|
58247
98d0f85d247f
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
nipkow
parents:
58202
diff
changeset
|
942 |
|
58626 | 943 |
* New infrastructure for compiling, running, evaluating and testing |
59569 | 944 |
generated code in target languages in HOL/Library/Code_Test. See |
945 |
HOL/Codegenerator_Test/Code_Test* for examples. |
|
58008 | 946 |
|
60009 | 947 |
* Library/Multiset: |
59813 | 948 |
- Introduced "replicate_mset" operation. |
949 |
- Introduced alternative characterizations of the multiset ordering in |
|
950 |
"Library/Multiset_Order". |
|
59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
951 |
- Renamed multiset ordering: |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
952 |
<# ~> #<# |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
953 |
<=# ~> #<=# |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
954 |
\<subset># ~> #\<subset># |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
955 |
\<subseteq># ~> #\<subseteq># |
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset
|
956 |
INCOMPATIBILITY. |
59986
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset
|
957 |
- Introduced abbreviations for ill-named multiset operations: |
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset
|
958 |
<#, \<subset># abbreviate < (strict subset) |
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset
|
959 |
<=#, \<le>#, \<subseteq># abbreviate <= (subset or equal) |
f38b94549dc8
introduced new abbreviations for multiset operations (in the hope of getting rid of the old names <, <=, etc.)
blanchet
parents:
59967
diff
changeset
|
960 |
INCOMPATIBILITY. |
59813 | 961 |
- Renamed |
962 |
in_multiset_of ~> in_multiset_in_set |
|
59998
c54d36be22ef
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents:
59991
diff
changeset
|
963 |
Multiset.fold ~> fold_mset |
c54d36be22ef
renamed Multiset.fold -> fold_mset, Multiset.filter -> filter_mset
nipkow
parents:
59991
diff
changeset
|
964 |
Multiset.filter ~> filter_mset |
59813 | 965 |
INCOMPATIBILITY. |
59949 | 966 |
- Removed mcard, is equal to size. |
59813 | 967 |
- Added attributes: |
968 |
image_mset.id [simp] |
|
969 |
image_mset_id [simp] |
|
970 |
elem_multiset_of_set [simp, intro] |
|
971 |
comp_fun_commute_plus_mset [simp] |
|
972 |
comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp] |
|
973 |
in_mset_fold_plus_iff [iff] |
|
974 |
set_of_Union_mset [simp] |
|
975 |
in_Union_mset_iff [iff] |
|
976 |
INCOMPATIBILITY. |
|
977 |
||
60009 | 978 |
* Library/Sum_of_Squares: simplified and improved "sos" method. Always |
979 |
use local CSDP executable, which is much faster than the NEOS server. |
|
980 |
The "sos_cert" functionality is invoked as "sos" with additional |
|
981 |
argument. Minor INCOMPATIBILITY. |
|
982 |
||
983 |
* HOL-Decision_Procs: New counterexample generator quickcheck |
|
984 |
[approximation] for inequalities of transcendental functions. Uses |
|
985 |
hardware floating point arithmetic to randomly discover potential |
|
60010 | 986 |
counterexamples. Counterexamples are certified with the "approximation" |
60009 | 987 |
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for |
988 |
examples. |
|
58990 | 989 |
|
59354 | 990 |
* HOL-Probability: Reworked measurability prover |
60010 | 991 |
- applies destructor rules repeatedly |
59354 | 992 |
- removed application splitting (replaced by destructor rule) |
59569 | 993 |
- added congruence rules to rewrite measure spaces under the sets |
994 |
projection |
|
995 |
||
60009 | 996 |
* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for |
997 |
single-step rewriting with subterm selection based on patterns. |
|
998 |
||
58630 | 999 |
|
58066 | 1000 |
*** ML *** |
1001 |
||
60009 | 1002 |
* Subtle change of name space policy: undeclared entries are now |
1003 |
considered inaccessible, instead of accessible via the fully-qualified |
|
1004 |
internal name. This mainly affects Name_Space.intern (and derivatives), |
|
1005 |
which may produce an unexpected Long_Name.hidden prefix. Note that |
|
60010 | 1006 |
contemporary applications use the strict Name_Space.check (and |
60009 | 1007 |
derivatives) instead, which is not affected by the change. Potential |
1008 |
INCOMPATIBILITY in rare applications of Name_Space.intern. |
|
59951 | 1009 |
|
60094 | 1010 |
* Subtle change of error semantics of Toplevel.proof_of: regular user |
1011 |
ERROR instead of internal Toplevel.UNDEF. |
|
1012 |
||
59951 | 1013 |
* Basic combinators map, fold, fold_map, split_list, apply are available |
1014 |
as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. |
|
1015 |
||
1016 |
* Renamed "pairself" to "apply2", in accordance to @{apply 2}. |
|
1017 |
INCOMPATIBILITY. |
|
1018 |
||
1019 |
* Former combinators NAMED_CRITICAL and CRITICAL for central critical |
|
1020 |
sections have been discontinued, in favour of the more elementary |
|
1021 |
Multithreading.synchronized and its high-level derivative |
|
1022 |
Synchronized.var (which is usually sufficient in applications). Subtle |
|
1023 |
INCOMPATIBILITY: synchronized access needs to be atomic and cannot be |
|
1024 |
nested. |
|
1025 |
||
60009 | 1026 |
* Synchronized.value (ML) is actually synchronized (as in Scala): subtle |
1027 |
change of semantics with minimal potential for INCOMPATIBILITY. |
|
59899 | 1028 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset
|
1029 |
* The main operations to certify logical entities are Thm.ctyp_of and |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset
|
1030 |
Thm.cterm_of with a local context; old-style global theory variants are |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset
|
1031 |
available as Thm.global_ctyp_of and Thm.global_cterm_of. |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset
|
1032 |
INCOMPATIBILITY. |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset
|
1033 |
|
59582 | 1034 |
* Elementary operations in module Thm are no longer pervasive. |
1035 |
INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, |
|
1036 |
Thm.term_of etc. |
|
1037 |
||
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58957
diff
changeset
|
1038 |
* Proper context for various elementary tactics: assume_tac, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset
|
1039 |
resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59480
diff
changeset
|
1040 |
compose_tac, Splitter.split_tac etc. INCOMPATIBILITY. |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58928
diff
changeset
|
1041 |
|
58066 | 1042 |
* Tactical PARALLEL_ALLGOALS is the most common way to refer to |
1043 |
PARALLEL_GOALS. |
|
1044 |
||
59564
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset
|
1045 |
* Goal.prove_multi is superseded by the fully general Goal.prove_common, |
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset
|
1046 |
which also allows to specify a fork priority. |
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset
|
1047 |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset
|
1048 |
* Antiquotation @{command_spec "COMMAND"} is superseded by |
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset
|
1049 |
@{command_keyword COMMAND} (usually without quotes and with PIDE |
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset
|
1050 |
markup). Minor INCOMPATIBILITY. |
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset
|
1051 |
|
60009 | 1052 |
* Cartouches within ML sources are turned into values of type |
1053 |
Input.source (with formal position information). |
|
1054 |
||
58066 | 1055 |
|
58610 | 1056 |
*** System *** |
1057 |
||
59951 | 1058 |
* The Isabelle tool "update_cartouches" changes theory files to use |
1059 |
cartouches instead of old-style {* verbatim *} or `alt_string` tokens. |
|
1060 |
||
60106 | 1061 |
* The Isabelle tool "build" provides new options -X, -k, -x. |
59951 | 1062 |
|
1063 |
* Discontinued old-fashioned "codegen" tool. Code generation can always |
|
1064 |
be externally triggered using an appropriate ROOT file plus a |
|
1065 |
corresponding theory. Parametrization is possible using environment |
|
1066 |
variables, or ML snippets in the most extreme cases. Minor |
|
1067 |
INCOMPATIBILITY. |
|
58842 | 1068 |
|
59200 | 1069 |
* JVM system property "isabelle.threads" determines size of Scala thread |
1070 |
pool, like Isabelle system option "threads" for ML. |
|
1071 |
||
59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset
|
1072 |
* JVM system property "isabelle.laf" determines the default Swing |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset
|
1073 |
look-and-feel, via internal class name or symbolic name as in the jEdit |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset
|
1074 |
menu Global Options / Appearance. |
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset
|
1075 |
|
59951 | 1076 |
* Support for Proof General and Isar TTY loop has been discontinued. |
60009 | 1077 |
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead. |
59891
9ce697050455
added isabelle build option -k, for fast off-line checking of theory sources;
wenzelm
parents:
59849
diff
changeset
|
1078 |
|
58610 | 1079 |
|
57695 | 1080 |
|
57452 | 1081 |
New in Isabelle2014 (August 2014) |
1082 |
--------------------------------- |
|
54055 | 1083 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
1084 |
*** General *** |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
1085 |
|
57452 | 1086 |
* Support for official Standard ML within the Isabelle context. |
1087 |
Command 'SML_file' reads and evaluates the given Standard ML file. |
|
1088 |
Toplevel bindings are stored within the theory context; the initial |
|
1089 |
environment is restricted to the Standard ML implementation of |
|
1090 |
Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' |
|
1091 |
and 'SML_export' allow to exchange toplevel bindings between the two |
|
1092 |
separate environments. See also ~~/src/Tools/SML/Examples.thy for |
|
1093 |
some examples. |
|
56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56450
diff
changeset
|
1094 |
|
57504 | 1095 |
* Standard tactics and proof methods such as "clarsimp", "auto" and |
1096 |
"safe" now preserve equality hypotheses "x = expr" where x is a free |
|
1097 |
variable. Locale assumptions and chained facts containing "x" |
|
1098 |
continue to be useful. The new method "hypsubst_thin" and the |
|
1099 |
configuration option "hypsubst_thin" (within the attribute name space) |
|
1100 |
restore the previous behavior. INCOMPATIBILITY, especially where |
|
1101 |
induction is done after these methods or when the names of free and |
|
1102 |
bound variables clash. As first approximation, old proofs may be |
|
1103 |
repaired by "using [[hypsubst_thin = true]]" in the critical spot. |
|
1104 |
||
56232 | 1105 |
* More static checking of proof methods, which allows the system to |
1106 |
form a closure over the concrete syntax. Method arguments should be |
|
1107 |
processed in the original proof context as far as possible, before |
|
1108 |
operating on the goal state. In any case, the standard discipline for |
|
1109 |
subgoal-addressing needs to be observed: no subgoals or a subgoal |
|
1110 |
number that is out of range produces an empty result sequence, not an |
|
1111 |
exception. Potential INCOMPATIBILITY for non-conformant tactical |
|
1112 |
proof tools. |
|
1113 |
||
57452 | 1114 |
* Lexical syntax (inner and outer) supports text cartouches with |
1115 |
arbitrary nesting, and without escapes of quotes etc. The Prover IDE |
|
1116 |
supports input via ` (backquote). |
|
1117 |
||
1118 |
* The outer syntax categories "text" (for formal comments and document |
|
1119 |
markup commands) and "altstring" (for literal fact references) allow |
|
1120 |
cartouches as well, in addition to the traditional mix of quotations. |
|
1121 |
||
1122 |
* Syntax of document antiquotation @{rail} now uses \<newline> instead |
|
1123 |
of "\\", to avoid the optical illusion of escaped backslash within |
|
57491 | 1124 |
string token. General renovation of its syntax using text cartouches. |
57452 | 1125 |
Minor INCOMPATIBILITY. |
1126 |
||
1127 |
* Discontinued legacy_isub_isup, which was a temporary workaround for |
|
1128 |
Isabelle/ML in Isabelle2013-1. The prover process no longer accepts |
|
1129 |
old identifier syntax with \<^isub> or \<^isup>. Potential |
|
1130 |
INCOMPATIBILITY. |
|
1131 |
||
1132 |
* Document antiquotation @{url} produces markup for the given URL, |
|
1133 |
which results in an active hyperlink within the text. |
|
1134 |
||
1135 |
* Document antiquotation @{file_unchecked} is like @{file}, but does |
|
1136 |
not check existence within the file-system. |
|
1137 |
||
1138 |
* Updated and extended manuals: codegen, datatypes, implementation, |
|
1139 |
isar-ref, jedit, system. |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1140 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset
|
1141 |
|
54533 | 1142 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
1143 |
||
57650 | 1144 |
* Improved Document panel: simplified interaction where every single |
57452 | 1145 |
mouse click (re)opens document via desktop environment or as jEdit |
1146 |
buffer. |
|
1147 |
||
1148 |
* Support for Navigator plugin (with toolbar buttons), with connection |
|
1149 |
to PIDE hyperlinks. |
|
1150 |
||
1151 |
* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. |
|
1152 |
Open text buffers take precedence over copies within the file-system. |
|
1153 |
||
1154 |
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for |
|
1155 |
auxiliary ML files. |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1156 |
|
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1157 |
* Improved syntactic and semantic completion mechanism, with simple |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1158 |
templates, completion language context, name-space completion, |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1159 |
file-name completion, spell-checker completion. |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1160 |
|
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1161 |
* Refined GUI popup for completion: more robust key/mouse event |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1162 |
handling and propagation to enclosing text area -- avoid loosing |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1163 |
keystrokes with slow / remote graphics displays. |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1164 |
|
57833
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
1165 |
* Completion popup supports both ENTER and TAB (default) to select an |
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
1166 |
item, depending on Isabelle options. |
2c2bae3da1c2
completion popup supports both ENTER and TAB (default);
wenzelm
parents:
57826
diff
changeset
|
1167 |
|
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1168 |
* Refined insertion of completion items wrt. jEdit text: multiple |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1169 |
selections, rectangular selections, rectangular selection as "tall |
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1170 |
caret". |
56342 | 1171 |
|
56580 | 1172 |
* Integrated spell-checker for document text, comments etc. with |
57423
96f970d1522b
updated NEWS -- removed material that is already in the manual;
wenzelm
parents:
57418
diff
changeset
|
1173 |
completion popup and context-menu. |
56554 | 1174 |
|
56879
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
1175 |
* More general "Query" panel supersedes "Find" panel, with GUI access |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
1176 |
to commands 'find_theorems' and 'find_consts', as well as print |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
1177 |
operations for the context. Minor incompatibility in keyboard |
ee2b61f37ad9
renamed "Find" to "Query", with more general operations;
wenzelm
parents:
56851
diff
changeset
|
1178 |
shortcuts etc.: replace action isabelle-find by isabelle-query. |
56761 | 1179 |
|
56901 | 1180 |
* Search field for all output panels ("Output", "Query", "Info" etc.) |
1181 |
to highlight text via regular expression. |
|
1182 |
||
54881 | 1183 |
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle / |
1184 |
General") allows to specify additional print modes for the prover |
|
1185 |
process, without requiring old-fashioned command-line invocation of |
|
1186 |
"isabelle jedit -m MODE". |
|
1187 |
||
56505 | 1188 |
* More support for remote files (e.g. http) using standard Java |
1189 |
networking operations instead of jEdit virtual file-systems. |
|
1190 |
||
57822 | 1191 |
* Empty editors buffers that are no longer required (e.g.\ via theory |
1192 |
imports) are automatically removed from the document model. |
|
1193 |
||
57869 | 1194 |
* Improved monitor panel. |
1195 |
||
56838 | 1196 |
* Improved Console/Scala plugin: more uniform scala.Console output, |
1197 |
more robust treatment of threads and interrupts. |
|
1198 |
||
56939 | 1199 |
* Improved management of dockable windows: clarified keyboard focus |
1200 |
and window placement wrt. main editor view; optional menu item to |
|
1201 |
"Detach" a copy where this makes sense. |
|
1202 |
||
57452 | 1203 |
* New Simplifier Trace panel provides an interactive view of the |
57591
8c095aef6769
clarified "simp_trace_new" and corresponding isar-ref section;
wenzelm
parents:
57532
diff
changeset
|
1204 |
simplification process, enabled by the "simp_trace_new" attribute |
57452 | 1205 |
within the context. |
1206 |
||
1207 |
||
55001 | 1208 |
*** Pure *** |
1209 |
||
57504 | 1210 |
* Low-level type-class commands 'classes', 'classrel', 'arities' have |
1211 |
been discontinued to avoid the danger of non-trivial axiomatization |
|
1212 |
that is not immediately visible. INCOMPATIBILITY, use regular |
|
1213 |
'instance' command with proof. The required OFCLASS(...) theorem |
|
1214 |
might be postulated via 'axiomatization' beforehand, or the proof |
|
1215 |
finished trivially if the underlying class definition is made vacuous |
|
1216 |
(without any assumptions). See also Isabelle/ML operations |
|
1217 |
Axclass.class_axiomatization, Axclass.classrel_axiomatization, |
|
1218 |
Axclass.arity_axiomatization. |
|
1219 |
||
56245 | 1220 |
* Basic constants of Pure use more conventional names and are always |
1221 |
qualified. Rare INCOMPATIBILITY, but with potentially serious |
|
1222 |
consequences, notably for tools in Isabelle/ML. The following |
|
1223 |
renaming needs to be applied: |
|
1224 |
||
1225 |
== ~> Pure.eq |
|
1226 |
==> ~> Pure.imp |
|
1227 |
all ~> Pure.all |
|
1228 |
TYPE ~> Pure.type |
|
1229 |
dummy_pattern ~> Pure.dummy_pattern |
|
1230 |
||
1231 |
Systematic porting works by using the following theory setup on a |
|
1232 |
*previous* Isabelle version to introduce the new name accesses for the |
|
1233 |
old constants: |
|
1234 |
||
1235 |
setup {* |
|
1236 |
fn thy => thy |
|
1237 |
|> Sign.root_path |
|
1238 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "==" |
|
1239 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>" |
|
1240 |
|> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all" |
|
1241 |
|> Sign.restore_naming thy |
|
1242 |
*} |
|
1243 |
||
1244 |
Thus ML antiquotations like @{const_name Pure.eq} may be used already. |
|
1245 |
Later the application is moved to the current Isabelle version, and |
|
1246 |
the auxiliary aliases are deleted. |
|
1247 |
||
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
1248 |
* Attributes "where" and "of" allow an optional context of local |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
1249 |
variables ('for' declaration): these variables become schematic in the |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
1250 |
instantiated theorem. |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55139
diff
changeset
|
1251 |
|
55152 | 1252 |
* Obsolete attribute "standard" has been discontinued (legacy since |
1253 |
Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context |
|
1254 |
where instantiations with schematic variables are intended (for |
|
1255 |
declaration commands like 'lemmas' or attributes like "of"). The |
|
1256 |
following temporary definition may help to port old applications: |
|
1257 |
||
1258 |
attribute_setup standard = |
|
1259 |
"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" |
|
1260 |
||
55001 | 1261 |
* More thorough check of proof context for goal statements and |
55006 | 1262 |
attributed fact expressions (concerning background theory, declared |
1263 |
hyps). Potential INCOMPATIBILITY, tools need to observe standard |
|
1264 |
context discipline. See also Assumption.add_assumes and the more |
|
1265 |
primitive Thm.assume_hyps. |
|
55001 | 1266 |
|
55108
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
1267 |
* Inner syntax token language allows regular quoted strings "..." |
0b7a0c1fdf7e
inner syntax token language allows regular quoted strings;
wenzelm
parents:
55049
diff
changeset
|
1268 |
(only makes sense in practice, if outer syntax is delimited |
57452 | 1269 |
differently, e.g. via cartouches). |
1270 |
||
57504 | 1271 |
* Command 'print_term_bindings' supersedes 'print_binds' for clarity, |
1272 |
but the latter is retained some time as Proof General legacy. |
|
1273 |
||
57452 | 1274 |
* Code generator preprocessor: explicit control of simp tracing on a |
1275 |
per-constant basis. See attribute "code_preproc". |
|
57430
020cea57eaa4
tracing facilities for the code generator preprocessor
haftmann
parents:
57423
diff
changeset
|
1276 |
|
55001 | 1277 |
|
54227
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
1278 |
*** HOL *** |
63b441f49645
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
haftmann
parents:
54055
diff
changeset
|
1279 |
|
57504 | 1280 |
* Code generator: enforce case of identifiers only for strict target |
1281 |
language requirements. INCOMPATIBILITY. |
|
1282 |
||
1283 |
* Code generator: explicit proof contexts in many ML interfaces. |
|
1284 |
INCOMPATIBILITY. |
|
1285 |
||
1286 |
* Code generator: minimize exported identifiers by default. Minor |
|
1287 |
INCOMPATIBILITY. |
|
1288 |
||
1289 |
* Code generation for SML and OCaml: dropped arcane "no_signatures" |
|
1290 |
option. Minor INCOMPATIBILITY. |
|
1291 |
||
1292 |
* "declare [[code abort: ...]]" replaces "code_abort ...". |
|
1293 |
INCOMPATIBILITY. |
|
1294 |
||
1295 |
* "declare [[code drop: ...]]" drops all code equations associated |
|
1296 |
with the given constants. |
|
1297 |
||
1298 |
* Code generations are provided for make, fields, extend and truncate |
|
1299 |
operations on records. |
|
57437 | 1300 |
|
57452 | 1301 |
* Command and antiquotation "value" are now hardcoded against nbe and |
1302 |
ML. Minor INCOMPATIBILITY. |
|
1303 |
||
57504 | 1304 |
* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY. |
1305 |
||
1306 |
* The symbol "\<newline>" may be used within char or string literals |
|
1307 |
to represent (Char Nibble0 NibbleA), i.e. ASCII newline. |
|
1308 |
||
1309 |
* Qualified String.implode and String.explode. INCOMPATIBILITY. |
|
56923 | 1310 |
|
57452 | 1311 |
* Simplifier: Enhanced solver of preconditions of rewrite rules can |
1312 |
now deal with conjunctions. For help with converting proofs, the old |
|
1313 |
behaviour of the simplifier can be restored like this: declare/using |
|
1314 |
[[simp_legacy_precond]]. This configuration option will disappear |
|
1315 |
again in the future. INCOMPATIBILITY. |
|
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
56072
diff
changeset
|
1316 |
|
55139 | 1317 |
* Simproc "finite_Collect" is no longer enabled by default, due to |
1318 |
spurious crashes and other surprises. Potential INCOMPATIBILITY. |
|
1319 |
||
57452 | 1320 |
* Moved new (co)datatype package and its dependencies from session |
1321 |
"HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors', |
|
1322 |
'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now |
|
1323 |
part of theory "Main". |
|
1324 |
||
55098 | 1325 |
Theory renamings: |
1326 |
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy) |
|
1327 |
Library/Wfrec.thy ~> Wfrec.thy |
|
1328 |
Library/Zorn.thy ~> Zorn.thy |
|
1329 |
Cardinals/Order_Relation.thy ~> Order_Relation.thy |
|
1330 |
Library/Order_Union.thy ~> Cardinals/Order_Union.thy |
|
1331 |
Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy |
|
1332 |
Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy |
|
1333 |
Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy |
|
1334 |
Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy |
|
1335 |
Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy |
|
1336 |
BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy |
|
1337 |
BNF/Basic_BNFs.thy ~> Basic_BNFs.thy |
|
1338 |
BNF/BNF_Comp.thy ~> BNF_Comp.thy |
|
1339 |
BNF/BNF_Def.thy ~> BNF_Def.thy |
|
1340 |
BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy |
|
1341 |
BNF/BNF_GFP.thy ~> BNF_GFP.thy |
|
1342 |
BNF/BNF_LFP.thy ~> BNF_LFP.thy |
|
1343 |
BNF/BNF_Util.thy ~> BNF_Util.thy |
|
1344 |
BNF/Coinduction.thy ~> Coinduction.thy |
|
1345 |
BNF/More_BNFs.thy ~> Library/More_BNFs.thy |
|
1346 |
BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy |
|
1347 |
BNF/Examples/* ~> BNF_Examples/* |
|
57452 | 1348 |
|
55098 | 1349 |
New theories: |
1350 |
Wellorder_Extension.thy (split from Zorn.thy) |
|
1351 |
Library/Cardinal_Notations.thy |
|
56942 | 1352 |
Library/BNF_Axomatization.thy |
55098 | 1353 |
BNF_Examples/Misc_Primcorec.thy |
1354 |
BNF_Examples/Stream_Processor.thy |
|
57452 | 1355 |
|
55519 | 1356 |
Discontinued theories: |
55098 | 1357 |
BNF/BNF.thy |
1358 |
BNF/Equiv_Relations_More.thy |
|
57452 | 1359 |
|
1360 |
INCOMPATIBILITY. |
|
55098 | 1361 |
|
56118
d3967fdc800a
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
blanchet
parents:
56076
diff
changeset
|
1362 |
* New (co)datatype package: |
57452 | 1363 |
- Command 'primcorec' is fully implemented. |
1364 |
- Command 'datatype_new' generates size functions ("size_xxx" and |
|
1365 |
"size") as required by 'fun'. |
|
1366 |
- BNFs are integrated with the Lifting tool and new-style |
|
1367 |
(co)datatypes with Transfer. |
|
1368 |
- Renamed commands: |
|
55875 | 1369 |
datatype_new_compat ~> datatype_compat |
1370 |
primrec_new ~> primrec |
|
1371 |
wrap_free_constructors ~> free_constructors |
|
1372 |
INCOMPATIBILITY. |
|
57452 | 1373 |
- The generated constants "xxx_case" and "xxx_rec" have been renamed |
55875 | 1374 |
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod"). |
1375 |
INCOMPATIBILITY. |
|
57452 | 1376 |
- The constant "xxx_(un)fold" and related theorems are no longer |
1377 |
generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually |
|
1378 |
using "prim(co)rec". |
|
55875 | 1379 |
INCOMPATIBILITY. |
57452 | 1380 |
- No discriminators are generated for nullary constructors by |
1381 |
default, eliminating the need for the odd "=:" syntax. |
|
57091 | 1382 |
INCOMPATIBILITY. |
57452 | 1383 |
- No discriminators or selectors are generated by default by |
57094
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
1384 |
"datatype_new", unless custom names are specified or the new |
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
1385 |
"discs_sels" option is passed. |
589ec121ce1a
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents:
57091
diff
changeset
|
1386 |
INCOMPATIBILITY. |
55875 | 1387 |
|
55643 | 1388 |
* Old datatype package: |
57452 | 1389 |
- The generated theorems "xxx.cases" and "xxx.recs" have been |
1390 |
renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> |
|
1391 |
"sum.case"). INCOMPATIBILITY. |
|
1392 |
- The generated constants "xxx_case", "xxx_rec", and "xxx_size" have |
|
1393 |
been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g., |
|
1394 |
"prod_case" ~> "case_prod"). INCOMPATIBILITY. |
|
1395 |
||
1396 |
* The types "'a list" and "'a option", their set and map functions, |
|
1397 |
their relators, and their selectors are now produced using the new |
|
1398 |
BNF-based datatype package. |
|
1399 |
||
55519 | 1400 |
Renamed constants: |
1401 |
Option.set ~> set_option |
|
1402 |
Option.map ~> map_option |
|
55525 | 1403 |
option_rel ~> rel_option |
57452 | 1404 |
|
55519 |