author  wenzelm 
Sun, 14 Feb 2016 16:30:27 +0100  
changeset 62312  5e5a881ebc12 
parent 62284  1fd4831e9f93 
child 62327  112eefe85ff0 
permissions  rwrr 
57491  1 
Isabelle NEWS  history of userrelevant changes 
2 
================================================= 

2553  3 

62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
62111
diff
changeset

4 
(Note: Isabelle/jEdit shows a treeview of the NEWS file in Sidekick.) 
60006  5 

60331  6 

62216  7 
New in this Isabelle version 
8 
 

9 

62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

10 
*** Isar *** 
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

11 

5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

12 
* Command '\<proof>' is an alias for 'sorry', with different 
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset

13 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  14 

15 

62031  16 
New in Isabelle2016 (February 2016) 
62016  17 
 
60138  18 

61337  19 
*** General *** 
20 

62168
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

21 
* Eisbach is now based on Pure instead of HOL. Objectslogics may import 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

22 
either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

23 
~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

24 
the HOLEisbach session located in ~~/src/HOL/Eisbach/ contains further 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

25 
examples that do require HOL. 
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset

26 

62157  27 
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for 
28 
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage. 

29 

62017  30 
* Former "xsymbols" syntax with Isabelle symbols is used by default, 
31 
without any special print mode. Important ASCII replacement syntax 

32 
remains available under print mode "ASCII", but less important syntax 

33 
has been removed (see below). 

34 

62109  35 
* Support for more arrow symbols, with rendering in LaTeX and Isabelle 
36 
fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>. 

62017  37 

62108
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

38 
* Special notation \<struct> for the first implicit 'structure' in the 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

39 
context has been discontinued. Rare INCOMPATIBILITY, use explicit 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

40 
structure name instead, notably in indexed notation with blocksubscript 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

41 
(e.g. \<odot>\<^bsub>A\<^esub>). 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

42 

0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

43 
* The glyph for \<diamond> in the IsabelleText font now corresponds better to its 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

44 
counterpart \<box> as quantifierlike symbol. A small diamond is available as 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

45 
\<diamondop>; the old symbol \<struct> loses this rendering and any special 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

46 
meaning. 
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset

47 

62017  48 
* Syntax for formal comments " text" now also supports the symbolic 
49 
form "\<comment> text". Commandline tool "isabelle update_cartouches c" helps 

50 
to update old sources. 

51 

61337  52 
* Toplevel theorem statements have been simplified as follows: 
53 

54 
theorems ~> lemmas 

55 
schematic_lemma ~> schematic_goal 

56 
schematic_theorem ~> schematic_goal 

57 
schematic_corollary ~> schematic_goal 

58 

59 
Commandline tool "isabelle update_theorems" updates theory sources 

60 
accordingly. 

61 

61338  62 
* Toplevel theorem statement 'proposition' is another alias for 
63 
'theorem'. 

64 

62169  65 
* The old 'defs' command has been removed (legacy since Isabelle2014). 
66 
INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or 

67 
deferred definitions require a surrounding 'overloading' block. 

68 

61337  69 

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

70 
*** 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

71 

60986  72 
* IDE support for the sourcelevel debugger of Poly/ML, to work with 
62253  73 
Isabelle/ML and official Standard ML. Option "ML_debugger" and commands 
74 
'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', 

75 
'SML_file_no_debug' control compilation of sources with or without 

76 
debugging information. The Debugger panel allows to set breakpoints (via 

77 
context menu), step through stopped threads, evaluate local ML 

78 
expressions etc. At least one Debugger view needs to be active to have 

79 
any effect on the running ML program. 

60984  80 

61803  81 
* The State panel manages explicit proof state output, with dynamic 
82 
autoupdate according to cursor movement. Alternatively, the jEdit 

83 
action "isabelle.updatestate" (shortcut S+ENTER) triggers manual 

84 
update. 

61729  85 

86 
* The Output panel no longer shows proof state output by default, to 

87 
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or 

88 
enable option "editor_output_state". 

61215  89 

61803  90 
* The text overview column (status of errors, warnings etc.) is updated 
91 
asynchronously, leading to much better editor reactivity. Moreover, the 

92 
full document node content is taken into account. The width of the 

93 
column is scaled according to the main text area font, for improved 

94 
visibility. 

95 

96 
* The main text area no longer changes its color hue in outdated 

97 
situations. The text overview column takes over the role to indicate 

98 
unfinished edits in the PIDE pipeline. This avoids flashing text display 

99 
due to adhoc updates by auxiliary GUI components, such as the State 

100 
panel. 

101 

62254
81cbea2babd9
tuned NEWS: longrunning tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset

102 
* Slightly improved scheduling for urgent print tasks (e.g. command 
81cbea2babd9
tuned NEWS: longrunning tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset

103 
state output, interactive queries) wrt. longrunning background tasks. 
62017  104 

105 
* Completion of symbols via prefix of \<name> or \<^name> or \name is 

106 
always possible, independently of the language context. It is never 

107 
implicit: a popup will show up unconditionally. 

108 

109 
* Additional abbreviations for syntactic completion may be specified in 

110 
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with 

111 
support for simple templates using ASCII 007 (bell) as placeholder. 

112 

62234
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

113 
* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

114 
completion like "+o", "*o", ".o" etc.  due to conflicts with other 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

115 
ASCII syntax. INCOMPATIBILITY, use plain backslashcompletion or define 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

116 
suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs. 
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset

117 

61483  118 
* Action "isabelleemph" (with keyboard shortcut C+e LEFT) controls 
119 
emphasized text style; the effect is visible in document output, not in 

120 
the editor. 

121 

122 
* Action "isabellereset" now uses keyboard shortcut C+e BACK_SPACE, 

123 
instead of former C+e LEFT. 

124 

61512
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

125 
* The commandline tool "isabelle jedit" and the isabelle.Main 
62027  126 
application wrapper treat the default $USER_HOME/Scratch.thy more 
61512
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

127 
uniformly, and allow the dummy file argument ":" to open an empty buffer 
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

128 
instead. 
933463440449
more uniform commandline for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset

129 

62017  130 
* New commandline tool "isabelle jedit_client" allows to connect to an 
131 
already running Isabelle/jEdit process. This achieves the effect of 

132 
singleinstance applications seen on common GUI desktops. 

133 

61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

134 
* The default lookandfeel 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

135 
works better with GUI scaling for very highresolution displays (e.g. 
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset

136 
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

137 

62163  138 
* Update to jedit5.3.0, with improved GUI scaling and support of 
139 
highresolution displays (e.g. 4K). 

140 

62034  141 
* The main Isabelle executable is managed as singleinstance Desktop 
142 
application uniformly on all platforms: Linux, Windows, Mac OS X. 

143 

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

144 

61405  145 
*** Document preparation *** 
146 

62017  147 
* Commands 'paragraph' and 'subparagraph' provide additional section 
148 
headings. Thus there are 6 levels of standard headings, as in HTML. 

149 

150 
* Command 'text_raw' has been clarified: input text is processed as in 

151 
'text' (with antiquotations and control symbols). The key difference is 

152 
the lack of the surrounding isabelle markup environment in output. 

153 

154 
* Text is structured in paragraphs and nested lists, using notation that 

155 
is similar to Markdown. The control symbols for list items are as 

156 
follows: 

157 

158 
\<^item> itemize 

159 
\<^enum> enumerate 

160 
\<^descr> description 

161 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

162 
* 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

163 
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and 
61595  164 
\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. 
165 
\<^name> without following cartouche is equivalent to @{name}. The 

61501  166 
standard Isabelle fonts provide glyphs to render important control 
167 
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

168 

61595  169 
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with 
170 
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using 

171 
standard LaTeX macros of the same names. 

172 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

173 
* 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

174 
Consequently, \<open>...\<close> without any decoration prints literal quasiformal 
61492  175 
text. Commandline tool "isabelle update_cartouches t" helps to update 
176 
old sources, by approximative patching of the content of string and 

177 
cartouche tokens seen in theory sources. 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

178 

97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

179 
* The @{text} antiquotation now ignores the antiquotation option 
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

180 
"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

181 
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the 
61494  182 
argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial 
183 
or terminal spaces are ignored. 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset

184 

62017  185 
* Antiquotations @{emph} and @{bold} output LaTeX source recursively, 
186 
adding appropriate text style markup. These may be used in the short 

187 
form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. 

188 

189 
* Document antiquotation @{footnote} outputs LaTeX source recursively, 

190 
marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. 

191 

192 
* Antiquotation @{verbatim [display]} supports option "indent". 

193 

194 
* Antiquotation @{theory_text} prints uninterpreted theory source text 

62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset

195 
(Isar outer syntax with command keywords etc.). This may be used in the 
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset

196 
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". 
62017  197 

198 
* Antiquotation @{doc ENTRY} provides a reference to the given 

199 
documentation, with a hyperlink in the Prover IDE. 

200 

201 
* Antiquotations @{command}, @{method}, @{attribute} print checked 

202 
entities of the Isar language. 

203 

61471  204 
* HTML presentation uses the standard IsabelleText font and Unicode 
205 
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former 

61488  206 
print mode "HTML" loses its special meaning. 
61471  207 

61405  208 

60406  209 
*** Isar *** 
210 

62205  211 
* Local goals ('have', 'show', 'hence', 'thus') allow structured rule 
212 
statements like fixes/assumes/shows in theorem specifications, but the 

213 
notation is postfix with keywords 'if' (or 'when') and 'for'. For 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

214 
example: 
60414  215 

216 
have result: "C x y" 

217 
if "A x" and "B y" 

218 
for x :: 'a and y :: 'a 

219 
<proof> 

220 

60449  221 
The local assumptions are bound to the name "that". The result is 
222 
exported from context of the statement as usual. The above roughly 

60414  223 
corresponds to a raw proof block like this: 
224 

225 
{ 

226 
fix x :: 'a and y :: 'a 

60449  227 
assume that: "A x" "B y" 
60414  228 
have "C x y" <proof> 
229 
} 

230 
note result = this 

60406  231 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

232 
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

233 
instead of 'assume' above. 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset

234 

61733  235 
* Assumptions ('assume', 'presume') allow structured rule statements 
236 
using 'if' and 'for', similar to 'have' etc. above. For example: 

61658  237 

238 
assume result: "C x y" 

239 
if "A x" and "B y" 

240 
for x :: 'a and y :: 'a 

241 

242 
This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general 

243 
result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y". 

244 

245 
Vacuous quantification in assumptions is omitted, i.e. a forcontext 

246 
only effects propositions according to actual use of variables. For 

247 
example: 

248 

249 
assume "A x" and "B y" for x and y 

250 

251 
is equivalent to: 

252 

253 
assume "\<And>x. A x" and "\<And>y. B y" 

254 

60595  255 
* The meaning of 'show' with Pure rule statements has changed: premises 
256 
are treated in the sense of 'assume', instead of 'presume'. This means, 

62205  257 
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as 
258 
follows: 

60595  259 

260 
show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

261 

262 
or: 

263 

264 
show "C x" if "A x" "B x" for x 

265 

266 
Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: 

267 

268 
show "C x" when "A x" "B x" for x 

269 

60459  270 
* New command 'consider' states rules for generalized elimination and 
271 
case splitting. This is like a toplevel statement "theorem obtains" used 

272 
within a proof body; or like a multibranch 'obtain' without activation 

273 
of the local context elements yet. 

274 

60455  275 
* Proof method "cases" allows to specify the rule as first entry of 
276 
chained facts. This is particularly useful with 'consider': 

277 

278 
consider (a) A  (b) B  (c) C <proof> 

279 
then have something 

280 
proof cases 

281 
case a 

282 
then show ?thesis <proof> 

283 
next 

284 
case b 

285 
then show ?thesis <proof> 

286 
next 

287 
case c 

288 
then show ?thesis <proof> 

289 
qed 

290 

60565  291 
* Command 'case' allows fact name and attribute specification like this: 
292 

293 
case a: (c xs) 

294 
case a [attributes]: (c xs) 

295 

296 
Facts that are introduced by invoking the case context are uniformly 

297 
qualified by "a"; the same name is used for the cumulative fact. The old 

298 
form "case (c xs) [attributes]" is no longer supported. Rare 

299 
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, 

300 
and always put attributes in front. 

301 

60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset

302 
* 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

303 
"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

304 
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

305 
'..' 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

306 

62017  307 
* Nesting of Isar goal structure has been clarified: the context after 
308 
the initial backwards refinement is retained for the whole proof, within 

309 
all its context sections (as indicated via 'next'). This is e.g. 

310 
relevant for 'using', 'including', 'supply': 

311 

312 
have "A \<and> A" if a: A for A 

313 
supply [simp] = a 

314 
proof 

315 
show A by simp 

316 
next 

317 
show A by simp 

318 
qed 

319 

320 
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the 

321 
proof body as well, abstracted over relevant parameters. 

322 

323 
* Improved typeinference for theorem statement 'obtains': separate 

324 
parameter scope for of each clause. 

325 

326 
* Term abbreviations via 'is' patterns also work for schematic 

327 
statements: result is abstracted over unknowns. 

328 

60631  329 
* Command 'subgoal' allows to impose some structure on backward 
330 
refinements, to avoid proof scripts degenerating into long of 'apply' 

331 
sequences. Further explanations and examples are given in the isarref 

332 
manual. 

333 

62017  334 
* Command 'supply' supports fact definitions during goal refinement 
335 
('apply' scripts). 

336 

61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

337 
* 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

338 
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

339 
example: 
60617  340 

341 
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

60622  342 
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

343 
proof goal_cases 
60622  344 
case (1 x) 
345 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

346 
next 

347 
case (2 y z) 

348 
then show ?case using \<open>U y\<close> \<open>V z\<close> sorry 

349 
qed 

350 

351 
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" 

352 
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

353 
proof goal_cases 
60617  354 
case prems: 1 
355 
then show ?case using prems sorry 

356 
next 

357 
case prems: 2 

358 
then show ?case using prems sorry 

359 
qed 

60578  360 

60581  361 
* The undocumented feature of implicit cases goal1, goal2, goal3, etc. 
60617  362 
is marked as legacy, and will be removed eventually. The proof method 
363 
"goals" achieves a similar effect within regular Isar; often it can be 

364 
done more adequately by other means (e.g. 'consider'). 

60581  365 

62017  366 
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` 
367 
as well, not just "by this" or "." as before. 

60551  368 

60554  369 
* Method "sleep" succeeds after a realtime delay (in seconds). This is 
370 
occasionally useful for demonstration and testing purposes. 

371 

60406  372 

60331  373 
*** Pure *** 
374 

61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset

375 
* Qualifiers in locale expressions default to mandatory ('!') regardless 
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset

376 
of the command. Previously, for 'locale' and 'sublocale' the default was 
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset

377 
optional ('?'). The old synatx '!' has been discontinued. 
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset

378 
INCOMPATIBILITY, remove '!' and add '?' as required. 
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset

379 

61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset

380 
* Keyword 'rewrites' identifies rewrite morphisms in interpretation 
62017  381 
commands. Previously, the keyword was 'where'. INCOMPATIBILITY. 
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset

382 

61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

383 
* More gentle suppression of syntax along locale morphisms while 
62017  384 
printing terms. Previously 'abbreviation' and 'notation' declarations 
385 
would be suppressed for morphisms except term identity. Now 

61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

386 
'abbreviation' is also kept for morphims that only change the involved 
62017  387 
parameters, and only 'notation' is suppressed. This can be of great help 
388 
when working with complex locale hierarchies, because proof states are 

389 
displayed much more succinctly. It also means that only notation needs 

390 
to be redeclared if desired, as illustrated by this example: 

61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

391 

e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

392 
locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65) 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

393 
begin 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

394 
definition derived (infixl "\<odot>" 65) where ... 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

395 
end 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

396 

e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

397 
locale morphism = 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

398 
left: struct composition + right: struct composition' 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

399 
for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65) 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

400 
begin 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

401 
notation right.derived ("\<odot>''") 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

402 
end 
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset

403 

61895  404 
* Command 'global_interpretation' issues interpretations into global 
405 
theories, with optional rewrite definitions following keyword 'defines'. 

406 

407 
* Command 'sublocale' accepts optional rewrite definitions after keyword 

61675  408 
'defines'. 
409 

61895  410 
* Command 'permanent_interpretation' has been discontinued. Use 
411 
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. 

61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61660
diff
changeset

412 

61252  413 
* Command 'print_definitions' prints dependencies of definitional 
414 
specifications. This functionality used to be part of 'print_theory'. 

415 

60331  416 
* Configuration option rule_insts_schematic has been discontinued 
62017  417 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 
60331  418 

62205  419 
* Abbreviations in type classes now carry proper sort constraint. Rare 
420 
INCOMPATIBILITY in situations where the previous misbehaviour has been 

421 
exploited. 

60347  422 

423 
* Refinement of userspace type system in type classes: pseudolocal 

62205  424 
operations behave more similar to abbreviations. Potential 
60347  425 
INCOMPATIBILITY in exotic situations. 
426 

427 

60171  428 
*** HOL *** 
429 

62017  430 
* The 'typedef' command has been upgraded from a partially checked 
431 
"axiomatization", to a full definitional specification that takes the 

432 
global collection of overloaded constant / type definitions into 

433 
account. Type definitions with open dependencies on overloaded 

434 
definitions need to be specified as "typedef (overloaded)". This 

435 
provides extra robustness in theory construction. Rare INCOMPATIBILITY. 

436 

437 
* Qualification of various formal entities in the libraries is done more 

438 
uniformly via "context begin qualified definition ... end" instead of 

439 
oldstyle "hide_const (open) ...". Consequently, both the defined 

440 
constant and its defining fact become qualified, e.g. Option.is_none and 

441 
Option.is_none_def. Occasional INCOMPATIBILITY in applications. 

442 

443 
* Some old and rarely used ASCII replacement syntax has been removed. 

444 
INCOMPATIBILITY, standard syntax with symbols should be used instead. 

445 
The subsequent commands help to reproduce the old forms, e.g. to 

446 
simplify porting old theories: 

447 

448 
notation iff (infixr "<>" 25) 

449 

450 
notation Times (infixr "<*>" 80) 

451 

452 
type_notation Map.map (infixr "~=>" 0) 

453 
notation Map.map_comp (infixl "o'_m" 55) 

454 

455 
type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) 

456 

457 
notation FuncSet.funcset (infixr ">" 60) 

458 
notation FuncSet.extensional_funcset (infixr ">\<^sub>E" 60) 

459 

460 
notation Omega_Words_Fun.conc (infixr "conc" 65) 

461 

462 
notation Preorder.equiv ("op ~~") 

463 
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) 

464 

465 
notation (in topological_space) tendsto (infixr ">" 55) 

466 
notation (in topological_space) LIMSEQ ("((_)/ > (_))" [60, 60] 60) 

467 
notation LIM ("((_)/  (_)/ > (_))" [60, 0, 60] 60) 

468 

469 
notation NSA.approx (infixl "@=" 50) 

470 
notation NSLIMSEQ ("((_)/ NS> (_))" [60, 60] 60) 

471 
notation NSLIM ("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) 

472 

473 
* The alternative notation "\<Colon>" for type and sort constraints has been 

474 
removed: in LaTeX document output it looks the same as "::". 

475 
INCOMPATIBILITY, use plain "::" instead. 

476 

477 
* Commands 'inductive' and 'inductive_set' work better when names for 

478 
intro rules are omitted: the "cases" and "induct" rules no longer 

479 
declare empty case_names, but no case_names at all. This allows to use 

480 
numbered cases in proofs, without requiring method "goal_cases". 

481 

482 
* Inductive definitions ('inductive', 'coinductive', etc.) expose 

483 
lowlevel facts of the internal construction only if the option 

62093  484 
"inductive_internals" is enabled. This refers to the internal predicate 
62017  485 
definition and its monotonicity result. Rare INCOMPATIBILITY. 
486 

487 
* Recursive function definitions ('fun', 'function', 'partial_function') 

488 
expose lowlevel facts of the internal construction only if the option 

62205  489 
"function_internals" is enabled. Its internal inductive definition is 
490 
also subject to "inductive_internals". Rare INCOMPATIBILITY. 

62093  491 

492 
* BNF datatypes ('datatype', 'codatatype', etc.) expose lowlevel facts 

493 
of the internal construction only if the option "bnf_internals" is 

494 
enabled. This supersedes the former option "bnf_note_all". Rare 

495 
INCOMPATIBILITY. 

62017  496 

497 
* Combinator to represent case distinction on products is named 

498 
"case_prod", uniformly, discontinuing any input aliasses. Very popular 

499 
theorem aliasses have been retained. 

500 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

501 
Consolidated facts: 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

502 
PairE ~> prod.exhaust 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

503 
Pair_eq ~> prod.inject 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

504 
pair_collapse ~> prod.collapse 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

505 
Pair_fst_snd_eq ~> prod_eq_iff 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

506 
split_twice ~> prod.case_distrib 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

507 
split_weak_cong ~> prod.case_cong_weak 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

508 
split_split ~> prod.split 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

509 
split_split_asm ~> prod.split_asm 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

510 
splitI ~> case_prodI 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

511 
splitD ~> case_prodD 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

512 
splitI2 ~> case_prodI2 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

513 
splitI2' ~> case_prodI2' 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

514 
splitE ~> case_prodE 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

515 
splitE' ~> case_prodE' 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

516 
split_pair ~> case_prod_Pair 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

517 
split_eta ~> case_prod_eta 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

518 
split_comp ~> case_prod_comp 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

519 
mem_splitI ~> mem_case_prodI 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

520 
mem_splitI2 ~> mem_case_prodI2 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

521 
mem_splitE ~> mem_case_prodE 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

522 
The_split ~> The_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

523 
cond_split_eta ~> cond_case_prod_eta 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

524 
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

525 
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

526 
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

527 
Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

528 
Collect_split_Grp_inD ~> Collect_case_prod_Grp_in 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

529 
Domain_Collect_split ~> Domain_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

530 
Image_Collect_split ~> Image_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

531 
Range_Collect_split ~> Range_Collect_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

532 
Eps_split ~> Eps_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

533 
Eps_split_eq ~> Eps_case_prod_eq 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

534 
split_rsp ~> case_prod_rsp 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

535 
curry_split ~> curry_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

536 
split_curry ~> case_prod_curry 
62017  537 

61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

538 
Changes in structure HOLogic: 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

539 
split_const ~> case_prod_const 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

540 
mk_split ~> mk_case_prod 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

541 
mk_psplits ~> mk_ptupleabs 
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset

542 
strip_psplits ~> strip_ptupleabs 
62017  543 

544 
INCOMPATIBILITY. 

545 

546 
* The coercions to type 'real' have been reorganised. The function 

547 
'real' is no longer overloaded, but has type 'nat => real' and 

548 
abbreviates of_nat for that type. Also 'real_of_int :: int => real' 

549 
abbreviates of_int for that type. Other overloaded instances of 'real' 

550 
have been replaced by 'real_of_ereal' and 'real_of_float'. 

551 

61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

552 
Consolidated facts (among others): 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

553 
real_of_nat_le_iff > of_nat_le_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

554 
real_of_nat_numeral of_nat_numeral 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

555 
real_of_int_zero of_int_0 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

556 
real_of_nat_zero of_nat_0 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

557 
real_of_one of_int_1 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

558 
real_of_int_add of_int_add 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

559 
real_of_nat_add of_nat_add 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

560 
real_of_int_diff of_int_diff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

561 
real_of_nat_diff of_nat_diff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

562 
floor_subtract floor_diff_of_int 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

563 
real_of_int_inject of_int_eq_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

564 
real_of_int_gt_zero_cancel_iff of_int_0_less_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

565 
real_of_int_ge_zero_cancel_iff of_int_0_le_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

566 
real_of_nat_ge_zero of_nat_0_le_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

567 
real_of_int_ceiling_ge le_of_int_ceiling 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

568 
ceiling_less_eq ceiling_less_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

569 
ceiling_le_eq ceiling_le_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

570 
less_floor_eq less_floor_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

571 
floor_less_eq floor_less_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

572 
floor_divide_eq_div floor_divide_of_int_eq 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

573 
real_of_int_zero_cancel of_nat_eq_0_iff 
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset

574 
ceiling_real_of_int ceiling_of_int 
62017  575 

576 
INCOMPATIBILITY. 

61143  577 

60841  578 
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has 
579 
been removed. INCOMPATIBILITY. 

580 

60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset

581 
* Quickcheck setup for finite sets. 
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset

582 

60171  583 
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. 
60138  584 

60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

585 
* Sledgehammer: 
61318  586 
 The MaSh relevance filter has been sped up. 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

587 
 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

588 
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

589 
 Auto Sledgehammer now minimizes and preplays the results. 
61030  590 
 Handle Vampire 4.0 proof output without raising exception. 
61043  591 
 Eliminated "MASH" environment variable. Use the "MaSh" option in 
592 
Isabelle/jEdit instead. INCOMPATIBILITY. 

61317  593 
 Eliminated obsolete "blocking" option and related subcommands. 
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset

594 

60310  595 
* Nitpick: 
61325
1cfc476198c9
avoid too aggressive optimization of 'finite' predicate
blanchet
parents:
61324
diff
changeset

596 
 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

597 
 Fixed soundness bug in "destroy_constrs" optimization. 
62080  598 
 Fixed soundness bug in translation of "rat" type. 
60310  599 
 Removed "check_potential" and "check_genuine" options. 
61317  600 
 Eliminated obsolete "blocking" option. 
60310  601 

62027  602 
* (Co)datatype package: 
61345  603 
 New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF 
604 
structure on the raw type to an abstract type defined using typedef. 

605 
 Always generate "case_transfer" theorem. 

62235  606 
 For mutual types, generate slightly stronger "rel_induct", 
607 
"rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY. 

61551  608 
 Allow discriminators and selectors with the same name as the type 
609 
being defined. 

610 
 Avoid various internal name clashes (e.g., 'datatype f = f'). 

60920  611 

62098  612 
* Transfer: new methods for interactive debugging of 'transfer' and 
613 
'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', 

614 
'transfer_prover_start' and 'transfer_prover_end'. 

61370  615 

62118  616 
* New diagnostic command print_record for displaying record definitions. 
617 

60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset

618 
* Division on integers is bootstrapped directly from division on 
62017  619 
naturals and uses generic numeral algorithm for computations. Slight 
620 
INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former 

621 
simprocs binary_int_div and binary_int_mod 

622 

623 
* Tightened specification of class semiring_no_zero_divisors. Minor 

60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

624 
INCOMPATIBILITY. 
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset

625 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

626 
* Class algebraic_semidom introduces common algebraic notions of 
62017  627 
integral (semi)domains, particularly units. Although logically subsumed 
628 
by fields, is is not a super class of these in order not to burden 

629 
fields with notions that are trivial there. 

630 

631 
* Class normalization_semidom specifies canonical representants for 

632 
equivalence classes of associated elements in an integral (semi)domain. 

633 
This formalizes associated elements as well. 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

634 

01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset

635 
* Abstract specification of gcd/lcm operations in classes semiring_gcd, 
62017  636 
semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute 
637 
and gcd_int.commute are subsumed by gcd.commute, as well as 

638 
gcd_nat.assoc and gcd_int.assoc by gcd.assoc. 

639 

640 
* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are 

641 
logically unified to Rings.divide in syntactic type class Rings.divide, 

642 
with infix syntax (_ div _). Infix syntax (_ / _) for field division is 

643 
added later as abbreviation in class Fields.inverse. INCOMPATIBILITY, 

644 
instantiations must refer to Rings.divide rather than the former 

645 
separate constants, hence infix syntax (_ / _) is usually not available 

646 
during instantiation. 

647 

648 
* New cancellation simprocs for boolean algebras to cancel complementary 

649 
terms for sup and inf. For example, "sup x (sup y ( x))" simplifies to 

650 
"top". INCOMPATIBILITY. 

61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61623
diff
changeset

651 

62101  652 
* Class uniform_space introduces uniform spaces btw topological spaces 
653 
and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be 

62205  654 
introduced in the form of an uniformity. Some constants are more general 
655 
now, it may be necessary to add type class constraints. 

62101  656 

657 
open_real_def \<leadsto> open_dist 

658 
open_complex_def \<leadsto> open_dist 

659 

62026  660 
* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY. 
661 

60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

662 
* Library/Multiset: 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

663 
 Renamed multiset inclusion operators: 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

664 
< ~> <# 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset

665 
> ~> ># 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

666 
<= ~> <=# 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset

667 
>= ~> >=# 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

668 
\<le> ~> \<le># 
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset

669 
\<ge> ~> \<ge># 
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

670 
INCOMPATIBILITY. 
62209  671 
 Added multiset inclusion operator syntax: 
672 
\<subset># 

673 
\<subseteq># 

674 
\<supset># 

675 
\<supseteq># 

60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

676 
 "'a multiset" is no longer an instance of the "order", 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

677 
"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff", 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

678 
"semilattice_inf", and "semilattice_sup" type classes. The theorems 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

679 
previously provided by these type classes (directly or indirectly) 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

680 
are now available through the "subset_mset" interpretation 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

681 
(e.g. add_mono ~> subset_mset.add_mono). 
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
60390
diff
changeset

682 
INCOMPATIBILITY. 
60497  683 
 Renamed conversions: 
60515  684 
multiset_of ~> mset 
685 
multiset_of_set ~> mset_set 

60497  686 
set_of ~> set_mset 
687 
INCOMPATIBILITY 

60398  688 
 Renamed lemmas: 
689 
mset_le_def ~> subseteq_mset_def 

690 
mset_less_def ~> subset_mset_def 

60400  691 
less_eq_multiset.rep_eq ~> subseteq_mset_def 
692 
INCOMPATIBILITY 

693 
 Removed lemmas generated by lift_definition: 

62235  694 
less_eq_multiset.abs_eq, less_eq_multiset.rsp, 
695 
less_eq_multiset.transfer, less_eq_multiset_def 

60400  696 
INCOMPATIBILITY 
60006  697 

62017  698 
* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a. 
699 

700 
* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the 

701 
BourbakiWitt fixpoint theorem for increasing functions in 

702 
chaincomplete partial orders. 

703 

704 
* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. 

705 
Minor INCOMPATIBILITY, use 'function' instead. 

706 

62064  707 
* Library/Periodic_Fun: a locale that provides convenient lemmas for 
708 
periodic functions. 

62060
b75764fc4c35
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
eberlm
parents:
62034
diff
changeset

709 

62098  710 
* Library/Formal_Power_Series: proper definition of division (with 
711 
remainder) for formal power series; instances for Euclidean Ring and 

712 
GCD. 

62086
1c0246456ab9
Added formal power series updates to NEWS/CONTRIBUTORS
Manuel Eberl <eberlm@in.tum.de>
parents:
62084
diff
changeset

713 

62084  714 
* HOLImperative_HOL: obsolete theory Legacy_Mrec has been removed. 
715 

716 
* HOLStatespace: command 'statespace' uses mandatory qualifier for 

717 
import of parent, as for general 'locale' expressions. INCOMPATIBILITY, 

718 
remove '!' and add '?' as required. 

719 

62237  720 
* HOLDecision_Procs: The "approximation" method works with "powr" 
721 
(exponentiation on real numbers) again. 

722 

62084  723 
* HOLMultivariate_Analysis: theory Cauchy_Integral_Thm with Contour 
724 
integrals (= complex path integrals), Cauchy's integral theorem, winding 

725 
numbers and Cauchy's integral formula, Liouville theorem, Fundamental 

726 
Theorem of Algebra. Ported from HOL Light. 

727 

728 
* HOLMultivariate_Analysis: topological concepts such as connected 

62017  729 
components, homotopic paths and the inside or outside of a set. 
61121
efe8b18306b7
do not expose lowlevel "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset

730 

62084  731 
* HOLMultivariate_Analysis: radius of convergence of power series and 
62064  732 
various summability tests; Harmonic numbers and the Euler–Mascheroni 
733 
constant; the Generalised Binomial Theorem; the complex and real 

734 
Gamma/logGamma/Digamma/ Polygamma functions and their most important 

735 
properties. 

62060
b75764fc4c35
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
eberlm
parents:
62034
diff
changeset

736 

62084  737 
* HOLProbability: The central limit theorem based on Levy's uniqueness 
738 
and continuity theorems, weak convergence, and characterisitc functions. 

739 

740 
* HOLData_Structures: new and growing session of standard data 

741 
structures. 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset

742 

60479  743 

60793  744 
*** ML *** 
745 

62017  746 
* The following combinators for lowlevel profiling of the ML runtime 
747 
system are available: 

748 

749 
profile_time (*CPU time*) 

750 
profile_time_thread (*CPU time on this thread*) 

751 
profile_allocations (*overall heap allocations*) 

752 

753 
* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). 

754 

62075  755 
* Antiquotation @{method NAME} inlines the (checked) name of the given 
756 
Isar proof method. 

757 

61922  758 
* Pretty printing of Poly/ML compiler output in Isabelle has been 
759 
improved: proper treatment of break offsets and blocks with consistent 

760 
breaks. 

761 

61268  762 
* The auxiliary module Pure/display.ML has been eliminated. Its 
763 
elementary thm print operations are now in Pure/more_thm.ML and thus 

764 
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. 

765 

61144  766 
* Simproc programming interfaces have been simplified: 
767 
Simplifier.make_simproc and Simplifier.define_simproc supersede various 

768 
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that 

769 
term patterns for the lefthand sides are specified with implicitly 

770 
fixed variables, like toplevel theorem statements. INCOMPATIBILITY. 

771 

60802  772 
* Instantiation rules have been reorganized as follows: 
773 

774 
Thm.instantiate (*lowlevel instantiation with named arguments*) 

775 
Thm.instantiate' (*version with positional arguments*) 

776 

777 
Drule.infer_instantiate (*instantiation with type inference*) 

778 
Drule.infer_instantiate' (*version with positional arguments*) 

779 

780 
The LHS only requires variable specifications, instead of full terms. 

781 
Old cterm_instantiate is superseded by infer_instantiate. 

782 
INCOMPATIBILITY, need to readjust some ML names and types accordingly. 

783 

60793  784 
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been 
785 
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. 

786 
instead (with proper context). 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

787 

48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

788 
* Thm.instantiate (and derivatives) no longer require the LHS of the 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

789 
instantiation to be certified: plain variables are given directly. 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

790 

60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

791 
* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

792 
quasibound variables (like the Simplifier), instead of accidentally 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

793 
named local fixes. This has the potential to improve stability of proof 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

794 
tools, but can also cause INCOMPATIBILITY for tools that don't observe 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

795 
the proof context discipline. 
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasibound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset

796 

62017  797 
* Isar proof methods are based on a slightly more general type 
798 
context_tactic, which allows to change the proof context dynamically 

799 
(e.g. to update cases) and indicate explicit Seq.Error results. Former 

800 
METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are 

801 
provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. 

61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61848
diff
changeset

802 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset

803 

60983
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

804 
*** System *** 
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

805 

61958  806 
* Commandline tool "isabelle console" enables print mode "ASCII". 
807 

62017  808 
* Commandline tool "isabelle update_then" expands old Isar command 
809 
conflations: 

810 

811 
hence ~> then have 

812 
thus ~> then show 

813 

814 
This syntax is more orthogonal and improves readability and 

815 
maintainability of proofs. 

816 

61602  817 
* Global session timeout is multiplied by timeout_scale factor. This 
818 
allows to adjust largescale tests (e.g. AFP) to overall hardware 

819 
performance. 

820 

61174  821 
* Property values in etc/symbols may contain spaces, if written with the 
62205  822 
replacement character "␣" (Unicode point 0x2324). For example: 
61174  823 

61602  824 
\<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono 
61174  825 

60995
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

826 
* Java runtime environment for x86_64windows allows to use larger heap 
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

827 
space. 
5176de8f90db
updated to jdk8u60, with support for x86_64windows;
wenzelm
parents:
60986
diff
changeset

828 

61135
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

829 
* 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

830 
platforms as follows. 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

831 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

832 
 Isabelle desktop application: platformspecific files that are 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

833 
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

834 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

835 
 isabelle jedit: settings 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

836 
JEDIT_JAVA_SYSTEM_OPTIONS 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

837 
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

838 

8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

839 
 isabelle build: settings 
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset

840 
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

841 

61294  842 
* Bash shell function "jvmpath" has been renamed to "platform_path": it 
843 
is relevant both for Poly/ML and JVM processes. 

844 

62017  845 
* Poly/ML default platform architecture may be changed from 32bit to 
62205  846 
64bit via system option ML_system_64. A system restart (and rebuild) is 
847 
required after change. 

62017  848 

849 
* Poly/ML 5.6 runs natively on x86windows and x86_64windows, which 

850 
both allow larger heap space than former x86cygwin. 

851 

62157  852 
* Heap images are 1015% smaller due to less wasteful persistent theory 
853 
content (using ML type theory_id instead of theory); 

854 

60983
ff4a67c65084
updated to polyml5.5.320150820, with native x86windows support;
wenzelm
parents:
60922
diff
changeset

855 

60479  856 

60009  857 
New in Isabelle2015 (May 2015) 
858 
 

57695  859 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

860 
*** General *** 
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

861 

59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset

862 
* 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

863 
'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

864 
as provided by some "context begin ... end" block. For example: 
59926  865 

866 
context 

867 
begin 

868 

869 
private definition ... 

870 
private lemma ... 

871 

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

872 
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

873 
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

874 

59926  875 
lemma ... 
876 
theorem ... 

877 

878 
end 

879 

59901  880 
* Command 'experiment' opens an anonymous locale context with private 
881 
naming policy. 

882 

59951  883 
* Command 'notepad' requires proper nesting of begin/end and its proof 
884 
structure in the body: 'oops' is no longer supported here. Minor 

885 
INCOMPATIBILITY, use 'sorry' instead. 

886 

887 
* Command 'named_theorems' declares a dynamic fact within the context, 

888 
together with an attribute to maintain the content incrementally. This 

889 
supersedes functor Named_Thms in Isabelle/ML, but with a subtle change 

890 
of semantics due to external visual order vs. internal reverse order. 

891 

892 
* 'find_theorems': search patterns which are abstractions are 

893 
schematically expanded before search. Search results match the naive 

894 
expectation more closely, particularly wrt. abbreviations. 

895 
INCOMPATIBILITY. 

59648  896 

59569  897 
* Commands 'method_setup' and 'attribute_setup' now work within a local 
898 
theory context. 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

899 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset

900 
* Outer syntax commands are managed authentically within the theory 
59569  901 
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

902 
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

903 

60115  904 
* Historical commandline terminator ";" is no longer accepted (and 
905 
already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle 

906 
update_semicolons" to remove obsolete semicolons from old theory 

907 
sources. 

908 

59951  909 
* Structural composition of proof methods (meth1; meth2) in Isar 
910 
corresponds to (tac1 THEN_ALL_NEW tac2) in ML. 

59105  911 

60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset

912 
* 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

913 
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

914 
method provides basic fact/term matching in addition to 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset

915 
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

916 
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

917 
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

918 
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

919 

57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset

920 

58524  921 
*** Prover IDE  Isabelle/Scala/jEdit *** 
922 

59569  923 
* Improved folding mode "isabelle" based on Isar syntax. Alternatively, 
924 
the "sidekick" mode may be used for document structure. 

925 

926 
* Extended bracket matching based on Isar language structure. System 

927 
option jedit_structure_limit determines maximum number of lines to scan 

928 
in the buffer. 

58758  929 

58540  930 
* Support for BibTeX files: context menu, contextsensitive token 
931 
marker, SideKick parser. 

58524  932 

58551  933 
* Document antiquotation @{cite} provides formal markup, which is 
60265  934 
interpreted semiformally based on .bib files that happen to be open in 
935 
the editor (hyperlinks, completion etc.). 

58551  936 

58785  937 
* Less waste of vertical space via negative line spacing (see Global 
938 
Options / Text Area). 

939 

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

940 
* 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

941 
display of 'thy_deps', 'class_deps' etc. 
60009  942 

60115  943 
* The commands 'thy_deps' and 'class_deps' allow optional bounds to 
944 
restrict the visualized hierarchy. 

60093  945 

60072  946 
* Improved scheduling for asynchronous print commands (e.g. provers 
947 
managed by the Sledgehammer panel) wrt. ongoing document processing. 

948 

58524  949 

59951  950 
*** Document preparation *** 
951 

952 
* Document markup commands 'chapter', 'section', 'subsection', 

953 
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any 

954 
context, even before the initial 'theory' command. Obsolete proof 

955 
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been 

956 
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' 

957 
instead. The old 'header' command is still retained for some time, but 

958 
should be replaced by 'chapter', 'section' etc. (using "isabelle 

959 
update_header"). Minor INCOMPATIBILITY. 

960 

60009  961 
* Official support for "tt" style variants, via \isatt{...} or 
962 
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or 

963 
verbatim environment of LaTeX is no longer used. This allows @{ML} etc. 

964 
as argument to other macros (such as footnotes). 

965 

966 
* Document antiquotation @{verbatim} prints ASCII text literally in "tt" 

967 
style. 

968 

969 
* Discontinued obsolete option "document_graph": session_graph.pdf is 

970 
produced unconditionally for HTML browser_info and PDFLaTeX document. 

971 

59951  972 
* Diagnostic commands and document markup commands within a proof do not 
973 
affect the command tag for output. Thus commands like 'thm' are subject 

974 
to proof document structure, and no longer "stick out" accidentally. 

975 
Commands 'text' and 'txt' merely differ in the LaTeX style, not their 

976 
tags. Potential INCOMPATIBILITY in exotic situations. 

977 

978 
* System option "pretty_margin" is superseded by "thy_output_margin", 

979 
which is also accessible via document antiquotation option "margin". 

980 
Only the margin for document output may be changed, but not the global 

981 
pretty printing: that is 76 for plain console output, and adapted 

982 
dynamically in GUI frontends. Implementations of document 

983 
antiquotations need to observe the margin explicitly according to 

984 
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 

985 

60299
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

986 
* 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

987 
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

988 
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

989 
INCOMPATIBILITY. 
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset

990 

59951  991 

58202  992 
*** Pure *** 
993 

59835
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

994 
* 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

995 
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

996 
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

997 
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

998 
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

999 
of schematic variables outside the context. Minor INCOMPATIBILITY, 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

1000 
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

1001 
variable declarations or dummy patterns instead. 
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset

1002 

60009  1003 
* Explicit instantiation via attributes "where", "of", and proof methods 
1004 
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns 

1005 
("_") that stand for anonymous local variables. 

1006 

59951  1007 
* Generated schematic variables in standard format of exported facts are 
1008 
incremented to avoid material in the proof context. Rare 

1009 
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 

1010 
different index. 

1011 

60010  1012 
* Lexical separation of signed and unsigned numerals: categories "num" 
1013 
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence 

1014 
of numeral signs, particularly in expressions involving infix syntax 

1015 
like "( 1) ^ n". 

58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset

1016 

58421  1017 
* Old inner token category "xnum" has been discontinued. Potential 
1018 
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" 

1019 
token category instead. 

1020 

58202  1021 

57737  1022 
*** HOL *** 
1023 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1024 
* New (co)datatype package: 
58373  1025 
 The 'datatype_new' command has been renamed 'datatype'. The old 
1026 
command of that name is now called 'old_datatype' and is provided 

1027 
by "~~/src/HOL/Library/Old_Datatype.thy". See 

1028 
'isabelle doc datatypes' for information on porting. 

1029 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1030 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1031 
disc_corec ~> corec_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1032 
disc_corec_iff ~> corec_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1033 
disc_exclude ~> distinct_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1034 
disc_exhaust ~> exhaust_disc 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1035 
disc_map_iff ~> map_disc_iff 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1036 
sel_corec ~> corec_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1037 
sel_exhaust ~> exhaust_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1038 
sel_map ~> map_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1039 
sel_set ~> set_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1040 
sel_split ~> split_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1041 
sel_split_asm ~> split_sel_asm 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1042 
strong_coinduct ~> coinduct_strong 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1043 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1044 
INCOMPATIBILITY. 
58192  1045 
 The "no_code" option to "free_constructors", "datatype_new", and 
1046 
"codatatype" has been renamed "plugins del: code". 

1047 
INCOMPATIBILITY. 

58044  1048 
 The rules "set_empty" have been removed. They are easy 
1049 
consequences of other set rules "by auto". 

1050 
INCOMPATIBILITY. 

1051 
 The rule "set_cases" is now registered with the "[cases set]" 

57990  1052 
attribute. This can influence the behavior of the "cases" proof 
1053 
method when more than one case rule is applicable (e.g., an 

1054 
assumption is of the form "w : set ws" and the method "cases w" 

1055 
is invoked). The solution is to specify the case rule explicitly 

1056 
(e.g. "cases w rule: widget.exhaust"). 

1057 
INCOMPATIBILITY. 

59675  1058 
 Renamed theories: 
1059 
BNF_Comp ~> BNF_Composition 

1060 
BNF_FP_Base ~> BNF_Fixpoint_Base 

1061 
BNF_GFP ~> BNF_Greatest_Fixpoint 

1062 
BNF_LFP ~> BNF_Least_Fixpoint 

1063 
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions 

1064 
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions 

1065 
INCOMPATIBILITY. 

60114  1066 
 Lifting and Transfer setup for basic HOL types sum and prod (also 
1067 
option) is now performed by the BNF package. Theories Lifting_Sum, 

1068 
Lifting_Product and Lifting_Option from Main became obsolete and 

1069 
were removed. Changed definitions of the relators rel_prod and 

1070 
rel_sum (using inductive). 

60111  1071 
INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead 
60114  1072 
of rel_prod_def and rel_sum_def. 
1073 
Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names 

1074 
changed (e.g. map_prod_transfer ~> prod.map_transfer). 

60261  1075 
 Parametricity theorems for map functions, relators, set functions, 
1076 
constructors, case combinators, discriminators, selectors and 

1077 
(co)recursors are automatically proved and registered as transfer 

1078 
rules. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1079 

6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1080 
* Old datatype package: 
58310  1081 
 The old 'datatype' command has been renamed 'old_datatype', and 
58373  1082 
'rep_datatype' has been renamed 'old_rep_datatype'. They are 
1083 
provided by "~~/src/HOL/Library/Old_Datatype.thy". See 

58310  1084 
'isabelle doc datatypes' for information on porting. 
58373  1085 
INCOMPATIBILITY. 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1086 
 Renamed theorems: 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1087 
weak_case_cong ~> case_cong_weak 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1088 
INCOMPATIBILITY. 
58373  1089 
 Renamed theory: 
1090 
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy 

1091 
INCOMPATIBILITY. 

57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset

1092 

59039  1093 
* Nitpick: 
60010  1094 
 Fixed soundness bug related to the strict and nonstrict subset 
59039  1095 
operations. 
1096 

57737  1097 
* Sledgehammer: 
59511  1098 
 CVC4 is now included with Isabelle instead of CVC3 and run by 
1099 
default. 

59965  1100 
 Z3 is now always enabled by default, now that it is fully open 
1101 
source. The "z3_non_commercial" option is discontinued. 

57737  1102 
 Minimization is now always enabled by default. 
60010  1103 
Removed subcommand: 
57737  1104 
min 
59967  1105 
 Proof reconstruction, both oneliners and Isar, has been 
59039  1106 
dramatically improved. 
1107 
 Improved support for CVC4 and veriT. 

57737  1108 

58062  1109 
* Old and new SMT modules: 
58067  1110 
 The old 'smt' method has been renamed 'old_smt' and moved to 
59569  1111 
'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, 
1112 
until applications have been ported to use the new 'smt' method. For 

1113 
the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must 

1114 
be installed, and the environment variable "OLD_Z3_SOLVER" must 

1115 
point to it. 

58062  1116 
INCOMPATIBILITY. 
58067  1117 
 The 'smt2' method has been renamed 'smt'. 
58060  1118 
INCOMPATIBILITY. 
59569  1119 
 New option 'smt_reconstruction_step_timeout' to limit the 
1120 
reconstruction time of Z3 proof steps in the new 'smt' method. 

59216  1121 
 New option 'smt_statistics' to display statistics of the new 'smt' 
1122 
method, especially runtime statistics of Z3 proof reconstruction. 

58060  1123 

60261  1124 
* Lifting: command 'lift_definition' allows to execute lifted constants 
1125 
that have as a return type a datatype containing a subtype. This 

1126 
overcomes longtime limitations in the area of code generation and 

1127 
lifting, and avoids tedious workarounds. 

60258  1128 

60009  1129 
* Command and antiquotation "value" provide different evaluation slots 
1130 
(again), where the previous strategy (NBE after ML) serves as default. 

1131 
Minor INCOMPATIBILITY. 

1132 

1133 
* Add NO_MATCHsimproc, allows to check for syntactic nonequality. 

1134 

1135 
* field_simps: Use NO_MATCHsimproc for distribution rules, to avoid 

1136 
nontermination in case of distributing a division. With this change 

1137 
field_simps is in some cases slightly less powerful, if it fails try to 

1138 
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. 

1139 

1140 
* Separate class no_zero_divisors has been given up in favour of fully 

1141 
algebraic semiring_no_zero_divisors. INCOMPATIBILITY. 

1142 

1143 
* Class linordered_semidom really requires no zero divisors. 

1144 
INCOMPATIBILITY. 

1145 

1146 
* Classes division_ring, field and linordered_field always demand 

1147 
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, 

1148 
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. 

1149 

1150 
* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit 

1151 
additive inverse operation. INCOMPATIBILITY. 

1152 

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

1153 
* Complex powers and square roots. The functions "ln" and "powr" are now 
60025  1154 
overloaded for types real and complex, and 0 powr y = 0 by definition. 
1155 
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

1156 

60009  1157 
* The functions "sin" and "cos" are now defined for any type of sort 
1158 
"{real_normed_algebra_1,banach}" type, so in particular on "real" and 

1159 
"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be 

1160 
needed. 

1161 

1162 
* New library of properties of the complex transcendental functions sin, 

1163 
cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light. 

1164 

1165 
* The factorial function, "fact", now has type "nat => 'a" (of a sort 

1166 
that admits numeric types including nat, int, real and complex. 

1167 
INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type 

1168 
constraint, and the combination "real (fact k)" is likely to be 

1169 
unsatisfactory. If a type conversion is still necessary, then use 

1170 
"of_nat (fact k)" or "real_of_nat (fact k)". 

1171 

1172 
* Removed functions "natfloor" and "natceiling", use "nat o floor" and 

1173 
"nat o ceiling" instead. A few of the lemmas have been retained and 

1174 
adapted: in their names "natfloor"/"natceiling" has been replaced by 

1175 
"nat_floor"/"nat_ceiling". 

1176 

1177 
* Qualified some duplicated fact names required for boostrapping the 

1178 
type class hierarchy: 

1179 
ab_add_uminus_conv_diff ~> diff_conv_add_uminus 

1180 
field_inverse_zero ~> inverse_zero 

1181 
field_divide_inverse ~> divide_inverse 

1182 
field_inverse ~> left_inverse 

1183 
Minor INCOMPATIBILITY. 

1184 

1185 
* Eliminated fact duplicates: 

1186 
mult_less_imp_less_right ~> mult_right_less_imp_less 

1187 
mult_less_imp_less_left ~> mult_left_less_imp_less 

1188 
Minor INCOMPATIBILITY. 

1189 

1190 
* Fact consolidation: even_less_0_iff is subsumed by 

1191 
double_add_less_zero_iff_single_add_less_zero (simp by default anyway). 

1192 

1193 
* Generalized and consolidated some theorems concerning divsibility: 

1194 
dvd_reduce ~> dvd_add_triv_right_iff 

1195 
dvd_plus_eq_right ~> dvd_add_right_iff 

1196 
dvd_plus_eq_left ~> dvd_add_left_iff 

1197 
Minor INCOMPATIBILITY. 

1198 

1199 
* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _" 

1200 
and part of theory Main. 

1201 
even_def ~> even_iff_mod_2_eq_zero 

1202 
INCOMPATIBILITY. 

1203 

1204 
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor 

1205 
INCOMPATIBILITY. 

1206 

1207 
* Bootstrap of listsum as special case of abstract product over lists. 

1208 
Fact rename: 

1209 
listsum_def ~> listsum.eq_foldr 

1210 
INCOMPATIBILITY. 

1211 

1212 
* Product over lists via constant "listprod". 

1213 

1214 
* Theory List: renamed drop_Suc_conv_tl and nth_drop' to 

1215 
Cons_nth_drop_Suc. 

58247
98d0f85d247f
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
nipkow
parents:
58202
diff
changeset

1216 

58626  1217 
* New infrastructure for compiling, running, evaluating and testing 
59569  1218 
generated code in target languages in HOL/Library/Code_Test. See 
1219 
HOL/Codegenerator_Test/Code_Test* for examples. 

58008  1220 

60009  1221 
* Library/Multiset: 
59813  1222 
 Introduced "replicate_mset" operation. 
1223 
 Introduced alternative characterizations of the multiset ordering in 

1224 
"Library/Multiset_Order". 

59958
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1225 
 Renamed multiset ordering: 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1226 
<# ~> #<# 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1227 
<=# ~> #<=# 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1228 
\<subset># ~> #\<subset># 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1229 
\<subseteq># ~> #\<subseteq># 
4538d41e8e54
renamed multiset ordering to free up nice <# etc. symbols for the standard subset
blanchet
parents:
59951
diff
changeset

1230 
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

1231 
 Introduced abbreviations for illnamed 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

1232 
<#, \<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

1233 
<=#, \<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

1234 
INCOMPATIBILITY. 
59813  1235 
 Renamed 
1236 
in_multiset_of ~> in_multiset_in_set 

59998
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59991
diff
changeset

1237 
Multiset.fold ~> fold_mset 
c54d36be22ef
renamed Multiset.fold > fold_mset, Multiset.filter > filter_mset
nipkow
parents:
59991
diff
changeset

1238 
Multiset.filter ~> filter_mset 
59813  1239 
INCOMPATIBILITY. 
59949  1240 
 Removed mcard, is equal to size. 
59813  1241 
 Added attributes: 
1242 
image_mset.id [simp] 

1243 
image_mset_id [simp] 

1244 
elem_multiset_of_set [simp, intro] 

1245 
comp_fun_commute_plus_mset [simp] 

1246 
comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp] 

1247 
in_mset_fold_plus_iff [iff] 

1248 
set_of_Union_mset [simp] 

1249 
in_Union_mset_iff [iff] 

1250 
INCOMPATIBILITY. 

1251 

60009  1252 
* Library/Sum_of_Squares: simplified and improved "sos" method. Always 
1253 
use local CSDP executable, which is much faster than the NEOS server. 

1254 
The "sos_cert" functionality is invoked as "sos" with additional 

1255 
argument. Minor INCOMPATIBILITY. 

1256 

1257 
* HOLDecision_Procs: New counterexample generator quickcheck 

1258 
[approximation] for inequalities of transcendental functions. Uses 

1259 
hardware floating point arithmetic to randomly discover potential 

60010  1260 
counterexamples. Counterexamples are certified with the "approximation" 
60009  1261 
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for 
1262 
examples. 

58990  1263 

59354  1264 
* HOLProbability: Reworked measurability prover 
60010  1265 
 applies destructor rules repeatedly 
59354  1266 
 removed application splitting (replaced by destructor rule) 
59569  1267 
 added congruence rules to rewrite measure spaces under the sets 
1268 
projection 

1269 

60009  1270 
* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for 
1271 
singlestep rewriting with subterm selection based on patterns. 

1272 

58630  1273 

58066  1274 
*** ML *** 
1275 

60009  1276 
* Subtle change of name space policy: undeclared entries are now 
1277 
considered inaccessible, instead of accessible via the fullyqualified 

1278 
internal name. This mainly affects Name_Space.intern (and derivatives), 

1279 
which may produce an unexpected Long_Name.hidden prefix. Note that 

60010  1280 
contemporary applications use the strict Name_Space.check (and 
60009  1281 
derivatives) instead, which is not affected by the change. Potential 
1282 
INCOMPATIBILITY in rare applications of Name_Space.intern. 

59951  1283 

60094  1284 
* Subtle change of error semantics of Toplevel.proof_of: regular user 
1285 
ERROR instead of internal Toplevel.UNDEF. 

1286 

59951  1287 
* Basic combinators map, fold, fold_map, split_list, apply are available 
1288 
as parameterized antiquotations, e.g. @{map 4} for lists of quadruples. 

1289 

1290 
* Renamed "pairself" to "apply2", in accordance to @{apply 2}. 

1291 
INCOMPATIBILITY. 

1292 

1293 
* Former combinators NAMED_CRITICAL and CRITICAL for central critical 

1294 
sections have been discontinued, in favour of the more elementary 

1295 
Multithreading.synchronized and its highlevel derivative 

1296 
Synchronized.var (which is usually sufficient in applications). Subtle 

1297 
INCOMPATIBILITY: synchronized access needs to be atomic and cannot be 

1298 
nested. 

1299 

60009  1300 
* Synchronized.value (ML) is actually synchronized (as in Scala): subtle 
1301 
change of semantics with minimal potential for INCOMPATIBILITY. 

59899  1302 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

1303 
* 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

1304 
Thm.cterm_of with a local context; oldstyle global theory variants are 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

1305 
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

1306 
INCOMPATIBILITY. 
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59588
diff
changeset

1307 

59582  1308 
* Elementary operations in module Thm are no longer pervasive. 
1309 
INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, 

1310 
Thm.term_of etc. 

1311 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58957
diff
changeset

1312 
* 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

1313 
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

1314 
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

1315 

58066  1316 
* Tactical PARALLEL_ALLGOALS is the most common way to refer to 
1317 
PARALLEL_GOALS. 

1318 

59564
fdc03c8daacc
Goal.prove_multi is superseded by the fully general Goal.prove_common;
wenzelm
parents:
59557
diff
changeset

1319 
* 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

1320 
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

1321 

59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

1322 
* Antiquotation @{command_spec "COMMAND"} is superseded by 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

1323 
@{command_keyword COMMAND} (usually without quotes and with PIDE 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

1324 
markup). Minor INCOMPATIBILITY. 
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59926
diff
changeset

1325 

60009  1326 
* Cartouches within ML sources are turned into values of type 
1327 
Input.source (with formal position information). 

1328 

58066  1329 

58610  1330 
*** System *** 
1331 

59951  1332 
* The Isabelle tool "update_cartouches" changes theory files to use 
1333 
cartouches instead of oldstyle {* verbatim *} or `alt_string` tokens. 

1334 

60106  1335 
* The Isabelle tool "build" provides new options X, k, x. 
59951  1336 

1337 
* Discontinued oldfashioned "codegen" tool. Code generation can always 

1338 
be externally triggered using an appropriate ROOT file plus a 

1339 
corresponding theory. Parametrization is possible using environment 

1340 
variables, or ML snippets in the most extreme cases. Minor 

1341 
INCOMPATIBILITY. 

58842  1342 

59200  1343 
* JVM system property "isabelle.threads" determines size of Scala thread 
1344 
pool, like Isabelle system option "threads" for ML. 

1345 

59201
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1346 
* 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

1347 
lookandfeel, 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

1348 
menu Global Options / Appearance. 
702e0971d617
added system property isabelle.laf, notably for initial system dialog;
wenzelm
parents:
59200
diff
changeset

1349 

59951  1350 
* Support for Proof General and Isar TTY loop has been discontinued. 
60009  1351 
Minor INCOMPATIBILITY, use standard PIDE infrastructure instead. 
59891
9ce697050455
added isabelle build option k, for fast offline checking of theory sources;
wenzelm
parents:
59849
diff
changeset

1352 

58610  1353 

57695  1354 

57452  1355 
New in Isabelle2014 (August 2014) 
1356 
 

54055  1357 

54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

1358 
*** General *** 
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54688
diff
changeset

1359 

57452  1360 
* Support for official Standard ML within the Isabelle context. 
1361 
Command 'SML_file' reads and evaluates the given Standard ML file. 

1362 
Toplevel bindings are stored within the theory context; the initial 

1363 
environment is restricted to the Standard ML implementation of 

1364 
Poly/ML, without the addons of Isabelle/ML. Commands 'SML_import' 

1365 
and 'SML_export' allow to exchange toplevel bindings between the two 

1366 
separate environments. See also ~~/src/Tools/SML/Examples.thy for 

1367 
some examples. 

56499
7e0178c84994
allow text cartouches in regular outer syntax categories "text" and "altstring";
wenzelm
parents:
56450
diff
changeset

1368 

57504  1369 
* Standard tactics and proof methods such as "clarsimp", "auto" and 
1370 
"safe" now preserve equality hypotheses "x = expr" where x is a free 

1371 
variable. Locale assumptions and chained facts containing "x" 

1372 
continue to be useful. The new method "hypsubst_thin" and the 

1373 
configuration option "hypsubst_thin" (within the attribute name space) 

1374 
restore the previous behavior. INCOMPATIBILITY, especially where 

1375 
induction is done after these methods or when the names of free and 

1376 
bound variables clash. As first approximation, old proofs may be 

1377 
repaired by "using [[hypsubst_thin = true]]" in the critical spot. 

1378 

56232  1379 
* More static checking of proof methods, which allows the system to 
1380 
form a closure over the concrete syntax. Method arguments should be 

1381 
processed in the original proof context as far as possible, before 

1382 
operating on the goal state. In any case, the standard discipline for 

1383 
subgoaladdressing needs to be observed: no subgoals or a subgoal 

1384 
number that is out of range produces an empty result sequence, not an 

1385 
exception. Potential INCOMPATIBILITY for nonconformant tactical 

1386 
proof tools. 

1387 

57452  1388 
* Lexical syntax (inner and outer) supports text cartouches with 
1389 
arbitrary nesting, and without escapes of quotes etc. The Prover IDE 

1390 
supports input via ` (backquote). 

1391 

1392 
* The outer syntax categories "text" (for formal comments and document 

1393 
markup commands) and "altstring" (for literal fact references) allow 

1394 
cartouches as well, in addition to the traditional mix of quotations. 

1395 

1396 
* Syntax of document antiquotation @{rail} now uses \<newline> instead 

1397 
of "\\", to avoid the optical illusion of escaped backslash within 

57491  1398 
string token. General renovation of its syntax using text cartouches. 
57452  1399 
Minor INCOMPATIBILITY. 
1400 

1401 
* Discontinued legacy_isub_isup, which was a temporary workaround for 

1402 
Isabelle/ML in Isabelle20131. The prover process no longer accepts 

1403 
old identifier syntax with \<^isub> or \<^isup>. Potential 

1404 
INCOMPATIBILITY. 
