author  traytel 
Wed, 17 Feb 2016 15:41:28 +0100  
changeset 62332  eeaa2f7b5329 
parent 62327  112eefe85ff0 
child 62335  e85c42f4f30a 
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 

62327  16 
*** HOL *** 
17 

18 
* (Co)datatype package: 

62332  19 
 the predicator :: ('a => bool) => 'a F => bool is now a firstclass 
20 
citizen in bounded natural functors 

62327  21 
 "primrec" now allows nested calls through the predicator in addition 
22 
to the map function. 

62332  23 
 "bnf" automatically discharges reflexive proof obligations 
24 
"bnf" outputs a slightly modified proof obligation expressing rel in 

25 
terms of map and set 

26 
(not giving a specification for rel makes this one reflexive) 

27 
"bnf" outputs a new proof obligation expressing pred in terms of set 

28 
(not giving a specification for pred makes this one reflexive) 

29 
INCOMPATIBILITY: manual "bnf" declarations may need adjustment 

62327  30 

31 

62031  32 
New in Isabelle2016 (February 2016) 
62016  33 
 
60138  34 

61337  35 
*** General *** 
36 

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

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

38 
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

39 
~~/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

40 
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

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

42 

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

45 

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

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

49 
has been removed (see below). 

50 

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

62017  53 

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

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

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

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

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

58 

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

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

60 
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

61 
\<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

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

63 

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

66 
to update old sources. 

67 

61337  68 
* Toplevel theorem statements have been simplified as follows: 
69 

70 
theorems ~> lemmas 

71 
schematic_lemma ~> schematic_goal 

72 
schematic_theorem ~> schematic_goal 

73 
schematic_corollary ~> schematic_goal 

74 

75 
Commandline tool "isabelle update_theorems" updates theory sources 

76 
accordingly. 

77 

61338  78 
* Toplevel theorem statement 'proposition' is another alias for 
79 
'theorem'. 

80 

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

83 
deferred definitions require a surrounding 'overloading' block. 

84 

61337  85 

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

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

87 

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

91 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

95 
any effect on the running ML program. 

60984  96 

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

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

100 
update. 

61729  101 

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

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

104 
enable option "editor_output_state". 

61215  105 

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

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

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

110 
visibility. 

111 

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

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

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

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

116 
panel. 

117 

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

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

119 
state output, interactive queries) wrt. longrunning background tasks. 
62017  120 

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

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

123 
implicit: a popup will show up unconditionally. 

124 

125 
* Additional abbreviations for syntactic completion may be specified in 

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

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

128 

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

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

130 
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

131 
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

132 
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

133 

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

136 
the editor. 

137 

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

139 
instead of former C+e LEFT. 

140 

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

141 
* The commandline tool "isabelle jedit" and the isabelle.Main 
62027  142 
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

143 
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

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

145 

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

148 
singleinstance applications seen on common GUI desktops. 

149 

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

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

151 
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

152 
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

153 

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

156 

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

159 

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

160 

61405  161 
*** Document preparation *** 
162 

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

165 

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

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

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

169 

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

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

172 
follows: 

173 

174 
\<^item> itemize 

175 
\<^enum> enumerate 

176 
\<^descr> description 

177 

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

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

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

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

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

184 

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

187 
standard LaTeX macros of the same names. 

188 

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

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

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

193 
cartouche tokens seen in theory sources. 

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

194 

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

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

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

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

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

200 

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

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

204 

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

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

207 

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

209 

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

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

211 
(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

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

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

215 
documentation, with a hyperlink in the Prover IDE. 

216 

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

218 
entities of the Isar language. 

219 

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

61488  222 
print mode "HTML" loses its special meaning. 
61471  223 

61405  224 

60406  225 
*** Isar *** 
226 

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

229 
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

230 
example: 
60414  231 

232 
have result: "C x y" 

233 
if "A x" and "B y" 

234 
for x :: 'a and y :: 'a 

235 
<proof> 

236 

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

60414  239 
corresponds to a raw proof block like this: 
240 

241 
{ 

242 
fix x :: 'a and y :: 'a 

60449  243 
assume that: "A x" "B y" 
60414  244 
have "C x y" <proof> 
245 
} 

246 
note result = this 

60406  247 

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

248 
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

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

250 

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

61658  253 

254 
assume result: "C x y" 

255 
if "A x" and "B y" 

256 
for x :: 'a and y :: 'a 

257 

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

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

260 

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

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

263 
example: 

264 

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

266 

267 
is equivalent to: 

268 

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

270 

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

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

60595  275 

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

277 

278 
or: 

279 

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

281 

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

283 

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

285 

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

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

289 
of the local context elements yet. 

290 

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

293 

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

295 
then have something 

296 
proof cases 

297 
case a 

298 
then show ?thesis <proof> 

299 
next 

300 
case b 

301 
then show ?thesis <proof> 

302 
next 

303 
case c 

304 
then show ?thesis <proof> 

305 
qed 

306 

60565  307 
* Command 'case' allows fact name and attribute specification like this: 
308 

309 
case a: (c xs) 

310 
case a [attributes]: (c xs) 

311 

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

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

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

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

316 
and always put attributes in front. 

317 

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

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

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

320 
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

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

322 

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

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

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

327 

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

329 
supply [simp] = a 

330 
proof 

331 
show A by simp 

332 
next 

333 
show A by simp 

334 
qed 

335 

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

337 
proof body as well, abstracted over relevant parameters. 

338 

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

340 
parameter scope for of each clause. 

341 

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

343 
statements: result is abstracted over unknowns. 

344 

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

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

348 
manual. 

349 

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

352 

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

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

354 
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

355 
example: 
60617  356 

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

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

359 
proof goal_cases 
60622  360 
case (1 x) 
361 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

362 
next 

363 
case (2 y z) 

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

365 
qed 

366 

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

368 
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

369 
proof goal_cases 
60617  370 
case prems: 1 
371 
then show ?case using prems sorry 

372 
next 

373 
case prems: 2 

374 
then show ?case using prems sorry 

375 
qed 

60578  376 

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

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

60581  381 

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

60551  384 

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

387 

60406  388 

60331  389 
*** Pure *** 
390 

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

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

392 
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

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

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

395 

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

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

398 

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

399 
* More gentle suppression of syntax along locale morphisms while 
62017  400 
printing terms. Previously 'abbreviation' and 'notation' declarations 
401 
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

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

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

406 
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

407 

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

408 
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

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

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

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

412 

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

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

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

415 
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

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

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

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

419 

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

422 

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

61675  424 
'defines'. 
425 

61895  426 
* Command 'permanent_interpretation' has been discontinued. Use 
427 
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. 

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

428 

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

431 

60331  432 
* Configuration option rule_insts_schematic has been discontinued 
62017  433 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 
60331  434 

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

437 
exploited. 

60347  438 

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

62205  440 
operations behave more similar to abbreviations. Potential 
60347  441 
INCOMPATIBILITY in exotic situations. 
442 

443 

60171  444 
*** HOL *** 
445 

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

448 
global collection of overloaded constant / type definitions into 

449 
account. Type definitions with open dependencies on overloaded 

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

451 
provides extra robustness in theory construction. Rare INCOMPATIBILITY. 

452 

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

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

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

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

457 
Option.is_none_def. Occasional INCOMPATIBILITY in applications. 

458 

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

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

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

462 
simplify porting old theories: 

463 

464 
notation iff (infixr "<>" 25) 

465 

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

467 

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

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

470 

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

472 

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

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

475 

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

477 

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

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

480 

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

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

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

484 

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

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

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

488 

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

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

491 
INCOMPATIBILITY, use plain "::" instead. 

492 

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

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

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

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

497 

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

499 
lowlevel facts of the internal construction only if the option 

62093  500 
"inductive_internals" is enabled. This refers to the internal predicate 
62017  501 
definition and its monotonicity result. Rare INCOMPATIBILITY. 
502 

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

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

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

62093  507 

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

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

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

511 
INCOMPATIBILITY. 

62017  512 

513 
* Combinator to represent case distinction on products is named 

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

515 
theorem aliasses have been retained. 

516 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

540 
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

541 
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

542 
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

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

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

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

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

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

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

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

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

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

552 
split_curry ~> case_prod_curry 
62017  553 

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

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

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

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

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

558 
strip_psplits ~> strip_ptupleabs 
62017  559 

560 
INCOMPATIBILITY. 

561 

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

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

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

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

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

567 

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

568 
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

569 
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

570 
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

571 
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

572 
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

573 
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

574 
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

575 
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

576 
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

577 
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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

584 
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

585 
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

586 
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

587 
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

588 
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

589 
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

590 
ceiling_real_of_int ceiling_of_int 
62017  591 

592 
INCOMPATIBILITY. 

61143  593 

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

596 

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

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

598 

60171  599 
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. 
60138  600 

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

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

603 
 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

604 
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

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

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

610 

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

612 
 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

613 
 Fixed soundness bug in "destroy_constrs" optimization. 
62080  614 
 Fixed soundness bug in translation of "rat" type. 
60310  615 
 Removed "check_potential" and "check_genuine" options. 
61317  616 
 Eliminated obsolete "blocking" option. 
60310  617 

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

621 
 Always generate "case_transfer" theorem. 

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

61551  624 
 Allow discriminators and selectors with the same name as the type 
625 
being defined. 

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

60920  627 

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

630 
'transfer_prover_start' and 'transfer_prover_end'. 

61370  631 

62118  632 
* New diagnostic command print_record for displaying record definitions. 
633 

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

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

637 
simprocs binary_int_div and binary_int_mod 

638 

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

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

641 

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

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

645 
fields with notions that are trivial there. 

646 

647 
* Class normalization_semidom specifies canonical representants for 

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

649 
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

650 

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

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

654 
gcd_nat.assoc and gcd_int.assoc by gcd.assoc. 

655 

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

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

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

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

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

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

662 
during instantiation. 

663 

664 
* New cancellation simprocs for boolean algebras to cancel complementary 

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

666 
"top". INCOMPATIBILITY. 

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

667 

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

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

62101  672 

673 
open_real_def \<leadsto> open_dist 

674 
open_complex_def \<leadsto> open_dist 

675 

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

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

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

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

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

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

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

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

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

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

686 
INCOMPATIBILITY. 
62209  687 
 Added multiset inclusion operator syntax: 
688 
\<subset># 

689 
\<subseteq># 

690 
\<supset># 

691 
\<supseteq># 

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

692 
 "'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

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

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

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

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

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

698 
INCOMPATIBILITY. 
60497  699 
 Renamed conversions: 
60515  700 
multiset_of ~> mset 
701 
multiset_of_set ~> mset_set 

60497  702 
set_of ~> set_mset 
703 
INCOMPATIBILITY 

60398  704 
 Renamed lemmas: 
705 
mset_le_def ~> subseteq_mset_def 

706 
mset_less_def ~> subset_mset_def 

60400  707 
less_eq_multiset.rep_eq ~> subseteq_mset_def 
708 
INCOMPATIBILITY 

709 
 Removed lemmas generated by lift_definition: 

62235  710 
less_eq_multiset.abs_eq, less_eq_multiset.rsp, 
711 
less_eq_multiset.transfer, less_eq_multiset_def 

60400  712 
INCOMPATIBILITY 
60006  713 

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

716 
* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the 

717 
BourbakiWitt fixpoint theorem for increasing functions in 

718 
chaincomplete partial orders. 

719 

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

721 
Minor INCOMPATIBILITY, use 'function' instead. 

722 

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

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

725 

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

728 
GCD. 

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

729 

62084  730 
* HOLImperative_HOL: obsolete theory Legacy_Mrec has been removed. 
731 

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

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

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

735 

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

738 

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

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

742 
Theorem of Algebra. Ported from HOL Light. 

743 

744 
* HOLMultivariate_Analysis: topological concepts such as connected 

62017  745 
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

746 

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

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

751 
properties. 

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

752 

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

755 

756 
* HOLData_Structures: new and growing session of standard data 

757 
structures. 

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

758 

60479  759 

60793  760 
*** ML *** 
761 

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

764 

765 
profile_time (*CPU time*) 

766 
profile_time_thread (*CPU time on this thread*) 

767 
profile_allocations (*overall heap allocations*) 

768 

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

770 

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

773 

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

776 
breaks. 

777 

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

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

781 

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

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

785 
term patterns for the lefthand sides are specified with implicitly 

786 
fixed variables, like toplevel theorem statements. INCOMPATIBILITY. 

787 

60802  788 
* Instantiation rules have been reorganized as follows: 
789 

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

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

792 

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

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

795 

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

797 
Old cterm_instantiate is superseded by infer_instantiate. 

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

799 

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

802 
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

803 

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

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

805 
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

806 

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

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

808 
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

809 
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

810 
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

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

812 

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

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

816 
METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are 

817 
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

818 

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

819 

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

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

821 

61958  822 
* Commandline tool "isabelle console" enables print mode "ASCII". 
823 

62017  824 
* Commandline tool "isabelle update_then" expands old Isar command 
825 
conflations: 

826 

827 
hence ~> then have 

828 
thus ~> then show 

829 

830 
This syntax is more orthogonal and improves readability and 

831 
maintainability of proofs. 

832 

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

835 
performance. 

836 

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

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

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

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

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

844 

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

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

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

847 

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

848 
 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

849 
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

850 

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

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

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

853 
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

854 

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

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

856 
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

857 

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

860 

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

62017  864 

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

866 
both allow larger heap space than former x86cygwin. 

867 

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

870 

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

871 

60479  872 

60009  873 
New in Isabelle2015 (May 2015) 
874 
 

57695  875 

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

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

877 

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

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

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

880 
as provided by some "context begin ... end" block. For example: 
59926  881 

882 
context 

883 
begin 

884 

885 
private definition ... 

886 
private lemma ... 

887 

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

888 
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

889 
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

890 

59926  891 
lemma ... 
892 
theorem ... 

893 

894 
end 

895 

59901  896 
* Command 'experiment' opens an anonymous locale context with private 
897 
naming policy. 

898 

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

901 
INCOMPATIBILITY, use 'sorry' instead. 

902 

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

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

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

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

907 

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

909 
schematically expanded before search. Search results match the naive 

910 
expectation more closely, particularly wrt. abbreviations. 

911 
INCOMPATIBILITY. 

59648  912 

59569  913 
* Commands 'method_setup' and 'attribute_setup' now work within a local 
914 
theory context. 

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

915 

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

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

918 
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

919 

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

922 
update_semicolons" to remove obsolete semicolons from old theory 

923 
sources. 

924 

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

59105  927 

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

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

929 
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

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

931 
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

932 
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

933 
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

934 
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

935 

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

936 

58524  937 
*** Prover IDE  Isabelle/Scala/jEdit *** 
938 

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

941 

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

943 
option jedit_structure_limit determines maximum number of lines to scan 

944 
in the buffer. 

58758  945 

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

58524  948 

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

58551  952 

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

955 

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

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

957 
display of 'thy_deps', 'class_deps' etc. 
60009  958 

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

60093  961 

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

964 

58524  965 

59951  966 
*** Document preparation *** 
967 

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

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

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

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

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

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

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

975 
update_header"). Minor INCOMPATIBILITY. 

976 

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

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

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

981 

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

983 
style. 

984 

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

986 
produced unconditionally for HTML browser_info and PDFLaTeX document. 

987 

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

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

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

992 
tags. Potential INCOMPATIBILITY in exotic situations. 

993 

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

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

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

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

998 
dynamically in GUI frontends. Implementations of document 

999 
antiquotations need to observe the margin explicitly according to 

1000 
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. 

1001 

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

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

1003 
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

1004 
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

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

1006 

59951  1007 

58202  1008 
*** Pure *** 
1009 

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

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

1011 
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

1012 
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

1013 
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

1014 
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

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

1016 
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

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

1018 

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

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

1022 

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

1025 
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to 

1026 
different index. 

1027 

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

1030 
of numeral signs, particularly in expressions involving infix syntax 

1031 
like "( 1) ^ n". 

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

1032 

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

1035 
token category instead. 

1036 

58202  1037 

57737  1038 
*** HOL *** 
1039 

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

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

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

1044 
'isabelle doc datatypes' for information on porting. 

1045 
INCOMPATIBILITY. 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1060 
INCOMPATIBILITY. 
58192  1061 
 The "no_code" option to "free_constructors", "datatype_new", and 
1062 
"codatatype" has been renamed "plugins del: code". 

1063 
INCOMPATIBILITY. 

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

1066 
INCOMPATIBILITY. 

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

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

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

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

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

1073 
INCOMPATIBILITY. 

59675  1074 
 Renamed theories: 
1075 
BNF_Comp ~> BNF_Composition 

1076 
BNF_FP_Base ~> BNF_Fixpoint_Base 

1077 
BNF_GFP ~> BNF_Greatest_Fixpoint 

1078 
BNF_LFP ~> BNF_Least_Fixpoint 

1079 
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions 

1080 
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions 

1081 
INCOMPATIBILITY. 

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

1084 
Lifting_Product and Lifting_Option from Main became obsolete and 

1085 
were removed. Changed definitions of the relators rel_prod and 

1086 
rel_sum (using inductive). 

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

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

60261  1091 
 Parametricity theorems for map functions, relators, set functions, 
1092 
constructors, case combinators, discriminators, selectors and 

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

1094 
rules. 

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

1095 

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

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

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

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

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

1104 
INCOMPATIBILITY. 
58373  1105 
 Renamed theory: 
1106 
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy 

1107 
INCOMPATIBILITY. 

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

1108 

59039  1109 
* Nitpick: 
60010  1110 
 Fixed soundness bug related to the strict and nonstrict subset 
59039  1111 
operations. 
1112 

57737  1113 
* Sledgehammer: 
59511  1114 
 CVC4 is now included with Isabelle instead of CVC3 and run by 
1115 
default. 

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

57737  1118 
 Minimization is now always enabled by default. 
60010  1119 
Removed subcommand: 
57737  1120 
min 
59967  1121 
 Proof reconstruction, both oneliners and Isar, has been 
59039  1122 
dramatically improved. 
1123 
 Improved support for CVC4 and veriT. 

57737  1124 

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

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

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

1131 
point to it. 

58062  1132 
INCOMPATIBILITY. 
58067  1133 
 The 'smt2' method has been renamed 'smt'. 
58060  1134 
INCOMPATIBILITY. 
59569  1135 
 New option 'smt_reconstruction_step_timeout' to limit the 
1136 
reconstruction time of Z3 proof steps in the new 'smt' method. 

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

58060  1139 

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

1142 
overcomes longtime limitations in the area of code generation and 

1143 
lifting, and avoids tedious workarounds. 

60258  1144 

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

1147 
Minor INCOMPATIBILITY. 

1148 

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

1150 

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

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

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

1154 
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. 

1155 

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

1157 
algebraic semiring_no_zero_divisors. INCOMPATIBILITY. 

1158 

1159 
* Class linordered_semidom really requires no zero divisors. 

1160 
INCOMPATIBILITY. 

1161 

1162 
* Classes division_ring, field and linordered_field always demand 

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

1164 
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. 

1165 

1166 
* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit 

1167 
additive inverse operation. INCOMPATIBILITY. 

1168 

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

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

1172 

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

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

1176 
needed. 

1177 

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

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

1180 

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

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

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

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

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

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

1187 

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

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

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

1191 
"nat_floor"/"nat_ceiling". 

1192 

1193 
* Qualified some duplicated fact names required for boostrapping the 

1194 
type class hierarchy: 

1195 
ab_add_uminus_conv_diff ~> diff_conv_add_uminus 

1196 
field_inverse_zero ~> inverse_zero 

1197 
field_divide_inverse ~> divide_inverse 

1198 
field_inverse ~> left_inverse 

1199 
Minor INCOMPATIBILITY. 

1200 

1201 
* Eliminated fact duplicates: 

1202 
mult_less_imp_less_right ~> mult_right_less_imp_less 

1203 
mult_less_imp_less_left ~> mult_left_less_imp_less 

1204 
Minor INCOMPATIBILITY. 

1205 

1206 
* Fact consolidation: even_less_0_iff is subsumed by 

1207 
double_add_less_zero_iff_single_add_less_zero (simp by default anyway). 

1208 

1209 
* Generalized and consolidated some theorems concerning divsibility: 

1210 
dvd_reduce ~> dvd_add_triv_right_iff 

1211 
dvd_plus_eq_right ~> dvd_add_right_iff 

1212 
dvd_plus_eq_left ~> dvd_add_left_iff 

1213 
Minor INCOMPATIBILITY. 

1214 

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

1216 
and part of theory Main. 

1217 
even_def ~> even_iff_mod_2_eq_zero 

1218 
INCOMPATIBILITY. 

1219 

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

1221 
INCOMPATIBILITY. 

1222 

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

1224 
Fact rename: 

1225 
listsum_def ~> listsum.eq_foldr 

1226 
INCOMPATIBILITY. 

1227 

1228 
* Product over lists via constant "listprod". 

1229 

1230 
* Theory List: renamed drop_Suc_conv_tl and nth_drop' to 

1231 
Cons_nth_drop_Suc. 

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

1232 

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

58008  1236 

60009  1237 
* Library/Multiset: 
59813  1238 
 Introduced "replicate_mset" operation. 
1239 
 Introduced alternative characterizations of the multiset ordering in 

1240 
"Library/Multiset_Order". 

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

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

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

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

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

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

1246 
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

1247 
 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

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

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

1250 
INCOMPATIBILITY. 
59813  1251 
 Renamed 
1252 
in_multiset_of ~> in_multiset_in_set 

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

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

1254 
Multiset.filter ~> filter_mset 
59813  1255 
INCOMPATIBILITY. 
59949  1256 
 Removed mcard, is equal to size. 
59813  1257 
 Added attributes: 
1258 
image_mset.id [simp] 

1259 
image_mset_id [simp] 

1260 
elem_multiset_of_set [simp, intro] 

1261 
comp_fun_commute_plus_mset [simp] 

1262 
comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp] 

1263 
in_mset_fold_plus_iff [iff] 

1264 
set_of_Union_mset [simp] 

1265 
in_Union_mset_iff [iff] 

1266 
INCOMPATIBILITY. 

1267 

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

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

1271 
argument. Minor INCOMPATIBILITY. 

1272 

1273 
* HOLDecision_Procs: New counterexample generator quickcheck 

1274 
[approximation] for inequalities of transcendental functions. Uses 

1275 
hardware floating point arithmetic to randomly discover potential 

60010  1276 
counterexamples. Counterexamples are certified with the "approximation" 
60009  1277 
method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for 
1278 
examples. 

58990  1279 

59354  1280 
* HOLProbability: Reworked measurability prover 
60010  1281 
 applies destructor rules repeatedly 
59354  1282 
 removed application splitting (replaced by destructor rule) 
59569  1283 
 added congruence rules to rewrite measure spaces under the sets 
1284 
projection 

1285 

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

1288 

58630  1289 

58066  1290 
*** ML *** 
1291 

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

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

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

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

59951  1299 

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

1302 

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

1305 

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

1307 
INCOMPATIBILITY. 

1308 

1309 
* Former combinators NAMED_CRITICAL and CRITICAL for central critical 

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

1311 
Multithreading.synchronized and its highlevel derivative 

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

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

1314 
nested. 

1315 

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

59899  1318 

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

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

1320 
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

1321 
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

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

1323 

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

1326 
Thm.term_of etc. 

1327 

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

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

1329 
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

1330 
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

1331 

58066  1332 
* Tactical PARALLEL_ALLGOALS is the most common way to refer to 
1333 
PARALLEL_GOALS. 

1334 

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

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

1336 
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

1337 

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

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

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

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

1341 

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

1344 

58066  1345 

58610  1346 
*** System *** 
1347 

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

1350 

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

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

1354 
be externally triggered using an appropriate ROOT file plus a 

1355 
corresponding theory. Parametrization is possible using environment 

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

1357 
INCOMPATIBILITY. 

58842  1358 

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

1361 

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

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

1363 
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

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

1365 

59951  1366 
* Support for Proof General and Isar TTY loop has been discontinued. 
60009  1367 
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

1368 

58610  1369 

57695  1370 

57452  1371 
New in Isabelle2014 (August 2014) 
1372 
 

54055  1373 

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

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

1375 

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

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

1379 
environment is restricted to the Standard ML implementation of 

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

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

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

1383 
some examples. 

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

1384 

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

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

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

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

1390 
restore the previous behavior. INCOMPATIBILITY, especially where 

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

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

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

1394 

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

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

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

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

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

1401 
exception. Potential INCOMPATIBILITY for nonconformant tactical 

1402 
proof tools. 

1403 

57452  1404 
* Lexical syntax (inner and outer) supports text cartouches with 
1405 