author  haftmann 
Wed, 21 Dec 2016 21:26:26 +0100  
changeset 64633  5ebcf6c525f1 
parent 64632  9df24b8b6c0a 
child 64634  5bd30359e46e 
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 

64603  6 

64439  7 
New in this Isabelle version 
8 
 

9 

64602  10 
*** Prover IDE  Isabelle/Scala/jEdit *** 
11 

12 
* Commandline invocation "isabelle jedit R l LOGIC" opens the ROOT 

13 
entry of the specified logic session in the editor, while its parent is 

14 
used for formal checking. 

15 

16 

64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

17 
*** HOL *** 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

18 

64632  19 
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively. 
20 
INCOMPATIBILITY. 

21 

64633
5ebcf6c525f1
prefer existing logical constant over abbreviation
haftmann
parents:
64632
diff
changeset

22 
* Dropped abbreviation transP; use constant transp instead. 
5ebcf6c525f1
prefer existing logical constant over abbreviation
haftmann
parents:
64632
diff
changeset

23 

64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

24 
* Swapped orientation of congruence rules mod_add_left_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

25 
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

26 
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

27 
mod_diff_eq. INCOMPATIBILITY. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

28 

50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

29 
* Generalized some facts: 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

30 
zminus_zmod ~> mod_minus_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

31 
zdiff_zmod_left ~> mod_diff_left_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

32 
zdiff_zmod_right ~> mod_diff_right_eq 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

33 
zmod_eq_dvd_iff ~> mod_eq_dvd_iff 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

34 
INCOMPATIBILITY. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

35 

50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

36 
* Named collection mod_simps covers various congruence rules 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

37 
concerning mod, replacing former zmod_simps. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

38 
INCOMPATIBILITY. 
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64555
diff
changeset

39 

64532
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

40 
* (Co)datatype package: 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

41 
 The 'size_gen_o_map' lemma is no longer generated for datatypes 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

42 
with type class annotations. As a result, the tactic that derives 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

43 
it no longer fails on nested datatypes. Slight INCOMPATIBILITY. 
fc2835a932d9
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
blanchet
parents:
64529
diff
changeset

44 

64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64532
diff
changeset

45 
* The theorem in Permutations has been renamed: 
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64532
diff
changeset

46 
bij_swap_ompose_bij ~> bij_swap_compose_bij 
64602  47 

60331  48 

64072  49 
New in Isabelle20161 (December 2016) 
50 
 

62216  51 

62440  52 
*** General *** 
53 

64390  54 
* Splitter in proof methods "simp", "auto" and friends: 
55 
 The syntax "split add" has been discontinued, use plain "split", 

56 
INCOMPATIBILITY. 

57 
 For situations with many conditional or case expressions, there is 

58 
an alternative splitting strategy that can be much faster. It is 

59 
selected by writing "split!" instead of "split". It applies safe 

60 
introduction and elimination rules after each split rule. As a 

61 
result the subgoal may be split into several subgoals. 

62 

63273  63 
* Command 'bundle' provides a local theory target to define a bundle 
64 
from the body of specification commands (such as 'declare', 

65 
'declaration', 'notation', 'lemmas', 'lemma'). For example: 

66 

67 
bundle foo 

68 
begin 

69 
declare a [simp] 

70 
declare b [intro] 

71 
end 

63272  72 

63282  73 
* Command 'unbundle' is like 'include', but works within a local theory 
74 
context. Unlike "context includes ... begin", the effect of 'unbundle' 

75 
on the target context persists, until different declarations are given. 

76 

63977  77 
* Simplified outer syntax: uniform category "name" includes long 
78 
identifiers. Former "xname" / "nameref" / "name reference" has been 

79 
discontinued. 

80 

81 
* Embedded content (e.g. the inner syntax of types, terms, props) may be 

82 
delimited uniformly via cartouches. This works better than oldfashioned 

83 
quotes when sublanguages are nested. 

84 

85 
* Mixfix annotations support general block properties, with syntax 

86 
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", 

87 
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent 

88 
to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks 

89 
is superseded by "(\<open>unbreabable\<close>"  rare INCOMPATIBILITY. 

63650  90 

63383  91 
* Proof method "blast" is more robust wrt. corner cases of Pure 
92 
statements without objectlogic judgment. 

93 

63624
994d1a1105ef
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
wenzelm
parents:
63610
diff
changeset

94 
* Commands 'prf' and 'full_prf' are somewhat more informative (again): 
63977  95 
proof terms are reconstructed and cleaned from administrative thm nodes. 
96 

97 
* Code generator: config option "code_timing" triggers measurements of 

98 
different phases of code generation. See src/HOL/ex/Code_Timing.thy for 

99 
examples. 

100 

101 
* Code generator: implicits in Scala (stemming from type class 

102 
instances) are generated into companion object of corresponding type 

103 
class, to resolve some situations where ambiguities may occur. 

104 

64390  105 
* Solve direct: option "solve_direct_strict_warnings" gives explicit 
106 
warnings for lemma statements with trivial proofs. 

64013
048b7dbfdfa3
option to report results of solve_direct as explicit warnings
haftmann
parents:
63995
diff
changeset

107 

64602  108 

62904  109 
*** Prover IDE  Isabelle/Scala/jEdit *** 
110 

64527  111 
* More aggressive flushing of machinegenerated input, according to 
112 
system option editor_generated_input_delay (in addition to existing 

113 
editor_input_delay for regular user edits). This may affect overall PIDE 

114 
reactivity and CPU usage. 

115 

64390  116 
* Syntactic indentation according to Isabelle outer syntax. Action 
117 
"indentlines" (shortcut C+i) indents the current line according to 

118 
command keywords and some command substructure. Action 

119 
"isabelle.newline" (shortcut ENTER) indents the old and the new line 

120 
according to command keywords only; see also option 

121 
"jedit_indent_newline". 

122 

123 
* Semantic indentation for unstructured proof scripts ('apply' etc.) via 

124 
number of subgoals. This requires information of ongoing document 

125 
processing and may thus lag behind, when the user is editing too 

126 
quickly; see also option "jedit_script_indent" and 

127 
"jedit_script_indent_limit". 

128 

129 
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' 

130 
are treated as delimiters for fold structure; 'begin' and 'end' 

131 
structure of theory specifications is treated as well. 

132 

133 
* Command 'proof' provides information about proof outline with cases, 

134 
e.g. for proof methods "cases", "induct", "goal_cases". 

135 

136 
* Completion templates for commands involving "begin ... end" blocks, 

137 
e.g. 'context', 'notepad'. 

138 

139 
* Sidekick parser "isabellecontext" shows nesting of context blocks 

140 
according to 'begin' and 'end' structure. 

141 

63977  142 
* Highlighting of entity def/ref positions wrt. cursor. 
143 

144 
* Action "isabelle.selectentity" (shortcut CS+ENTER) selects all 

64514  145 
occurrences of the formal entity at the caret position. This facilitates 
63977  146 
systematic renaming. 
147 

148 
* PIDE document markup works across multiple Isar commands, e.g. the 

149 
results established at the end of a proof are properly identified in the 

150 
theorem statement. 

151 

152 
* Cartouche abbreviations work both for " and ` to accomodate typical 

153 
situations where old ASCII notation may be updated. 

154 

63875  155 
* Dockable window "Symbols" also provides access to 'abbrevs' from the 
156 
outer syntax of the current theory buffer. This provides clickable 

157 
syntax templates, including entries with empty abbrevs name (which are 

158 
inaccessible via keyboard completion). 

159 

63022  160 
* IDE support for the Isabelle/Pure bootstrap process, with the 
161 
following independent stages: 

162 

163 
src/Pure/ROOT0.ML 

164 
src/Pure/ROOT.ML 

165 
src/Pure/Pure.thy 

166 
src/Pure/ML_Bootstrap.thy 

167 

168 
The ML ROOT files act like quasitheories in the context of theory 

169 
ML_Bootstrap: this allows continuous checking of all loaded ML files. 

170 
The theory files are presented with a modified header to import Pure 

171 
from the running Isabelle instance. Results from changed versions of 

172 
each stage are *not* propagated to the next stage, and isolated from the 

173 
actual Isabelle/Pure that runs the IDE itself. The sequential 

63307  174 
dependencies of the above files are only observed for batch build. 
62904  175 

63977  176 
* Isabelle/ML and Standard ML files are presented in Sidekick with the 
177 
tree structure of section headings: this special comment format is 

178 
described in "implementation" chapter 0, e.g. (*** section ***). 

63461  179 

63581  180 
* Additional abbreviations for syntactic completion may be specified 
63871  181 
within the theory header as 'abbrevs'. The theory syntax for 'keywords' 
182 
has been simplified accordingly: optional abbrevs need to go into the 

183 
new 'abbrevs' section. 

184 

185 
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and 

186 
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor 

187 
INCOMPATIBILITY, use 'abbrevs' within theory header instead. 

63579  188 

64390  189 
* Action "isabelle.keymapmerge" asks the user to resolve pending 
190 
Isabelle keymap changes that are in conflict with the current jEdit 

191 
keymap; nonconflicting changes are always applied implicitly. This 

192 
action is automatically invoked on Isabelle/jEdit startup and thus 

193 
increases chances that users see new keyboard shortcuts when reusing 

194 
old keymaps. 

195 

63675  196 
* ML and document antiquotations for filesystems paths are more uniform 
197 
and diverse: 

198 

199 
@{path NAME}  no filesystem check 

200 
@{file NAME}  check for plain file 

201 
@{dir NAME}  check for directory 

202 

203 
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may 

204 
have to be changed. 

63669  205 

206 

63977  207 
*** Document preparation *** 
208 

209 
* New symbol \<circle>, e.g. for temporal operator. 

210 

64073  211 
* New document and ML antiquotation @{locale} for locales, similar to 
212 
existing antiquotation @{class}. 

213 

63977  214 
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close>  
215 
this allows special forms of document output. 

216 

217 
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control 

218 
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its 

219 
derivatives. 

220 

221 
* \<^raw:...> symbols are no longer supported. 

222 

223 
* Old 'header' command is no longer supported (legacy since 

224 
Isabelle2015). 

225 

226 

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

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

228 

63180  229 
* Many specification elements support structured statements with 'if' / 
230 
'for' eigencontext, e.g. 'axiomatization', 'abbreviation', 

231 
'definition', 'inductive', 'function'. 

232 

63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

233 
* Toplevel theorem statements support eigencontext notation with 'if' / 
63284  234 
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the 
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

235 
traditional long statement form (in prefix). Local premises are called 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

236 
"that" or "assms", respectively. Empty premises are *not* bound in the 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

237 
context: INCOMPATIBILITY. 
056ea294c256
toplevel theorem statements support 'if'/'for' eigencontext;
wenzelm
parents:
63078
diff
changeset

238 

63039  239 
* Command 'define' introduces a local (nonpolymorphic) definition, with 
240 
optional abstraction over local parameters. The syntax resembles 

63043  241 
'definition' and 'obtain'. It fits better into the Isar language than 
242 
old 'def', which is now a legacy feature. 

63039  243 

63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

244 
* Command 'obtain' supports structured statements with 'if' / 'for' 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

245 
context. 
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset

246 

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

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

248 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  249 

63977  250 
* The defining position of a literal fact \<open>prop\<close> is maintained more 
251 
carefully, and made accessible as hyperlink in the Prover IDE. 

252 

253 
* Commands 'finally' and 'ultimately' used to expose the result as 

254 
literal fact: this accidental behaviour has been discontinued. Rare 

255 
INCOMPATIBILITY, use more explicit means to refer to facts in Isar. 

256 

257 
* Command 'axiomatization' has become more restrictive to correspond 

258 
better to internal axioms as singleton facts with mandatory name. Minor 

259 
INCOMPATIBILITY. 

62939  260 

63259  261 
* Proof methods may refer to the main facts via the dynamic fact 
262 
"method_facts". This is particularly useful for Eisbach method 

263 
definitions. 

264 

63527  265 
* Proof method "use" allows to modify the main facts of a given method 
266 
expression, e.g. 

63259  267 

268 
(use facts in simp) 

269 
(use facts in \<open>simp add: ...\<close>) 

270 

63977  271 
* The old proof method "default" has been removed (legacy since 
272 
Isabelle2016). INCOMPATIBILITY, use "standard" instead. 

273 

62216  274 

63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

275 
*** Pure *** 
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

276 

63977  277 
* Pure provides basic versions of proof methods "simp" and "simp_all" 
278 
that only know about metaequality (==). Potential INCOMPATIBILITY in 

279 
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order 

280 
is relevant to avoid confusion of Pure.simp vs. HOL.simp. 

281 

282 
* The command 'unfolding' and proof method "unfold" include a second 

283 
stage where given equations are passed through the attribute "abs_def" 

284 
before rewriting. This ensures that definitions are fully expanded, 

285 
regardless of the actual parameters that are provided. Rare 

286 
INCOMPATIBILITY in some corner cases: use proof method (simp only:) 

287 
instead, or declare [[unfold_abs_def = false]] in the proof context. 

288 

289 
* Typeinference improves sorts of newly introduced type variables for 

290 
the objectlogic, using its base sort (i.e. HOL.type for Isabelle/HOL). 

291 
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context 

292 
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare 

293 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

294 
types where this is really intended. 

63350
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset

295 

63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset

296 

62327  297 
*** HOL *** 
298 

63977  299 
* New proof method "argo" using the builtin Argo solver based on SMT 
300 
technology. The method can be used to prove goals of quantifierfree 

301 
propositional logic, goals based on a combination of quantifierfree 

302 
propositional logic with equality, and goals based on a combination of 

303 
quantifierfree propositional logic with linear real arithmetic 

304 
including min/max/abs. See HOL/ex/Argo_Examples.thy for examples. 

305 

64390  306 
* The new "nunchaku" program integrates the Nunchaku model finder. The 
307 
tool is experimental. See ~~/src/HOL/Nunchaku/Nunchaku.thy for details. 

308 

63977  309 
* Metis: The problem encoding has changed very slightly. This might 
63785  310 
break existing proofs. INCOMPATIBILITY. 
311 

63116  312 
* Sledgehammer: 
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset

313 
 The MaSh relevance filter is now faster than before. 
63116  314 
 Produce syntactically correct Vampire 4.0 problem files. 
315 

62327  316 
* (Co)datatype package: 
62693  317 
 New commands for defining corecursive functions and reasoning about 
318 
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', 

319 
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof 

62842  320 
method. See 'isabelle doc corec'. 
63977  321 
 The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a firstclass 
63855  322 
citizen in bounded natural functors. 
62693  323 
 'primrec' now allows nested calls through the predicator in addition 
62327  324 
to the map function. 
63855  325 
 'bnf' automatically discharges reflexive proof obligations. 
62693  326 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  327 
terms of map and set 
63855  328 
(not giving a specification for rel makes this one reflexive). 
62693  329 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  330 
(not giving a specification for pred makes this one reflexive). 
331 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  332 
 Renamed lemmas: 
333 
rel_prod_apply ~> rel_prod_inject 

334 
pred_prod_apply ~> pred_prod_inject 

335 
INCOMPATIBILITY. 

62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
62525
diff
changeset

336 
 The "size" plugin has been made compatible again with locales. 
63855  337 
 The theorems about "rel" and "set" may have a slightly different (but 
338 
equivalent) form. 

339 
INCOMPATIBILITY. 

62327  340 

63977  341 
* The 'coinductive' command produces a proper coinduction rule for 
342 
mutual coinductive predicates. This new rule replaces the old rule, 

343 
which exposed details of the internal fixpoint construction and was 

344 
hard to use. INCOMPATIBILITY. 

345 

346 
* New abbreviations for negated existence (but not bounded existence): 

347 

348 
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) 

349 
\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) 

350 

351 
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" 

352 
has been removed for output. It is retained for input only, until it is 

353 
eliminated altogether. 

354 

355 
* The unique existence quantifier no longer provides 'binder' syntax, 

356 
but uses syntax translations (as for bounded unique existence). Thus 

357 
iterated quantification \<exists>!x y. P x y with its slightly confusing 

358 
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead, 

359 
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y 

360 
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential 

361 
INCOMPATIBILITY in rare situations. 

362 

363 
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic 

364 
INCOMPATIBILITY. 

365 

64390  366 
* Renamed constants and corresponding theorems: 
367 

368 
setsum ~> sum 

369 
setprod ~> prod 

370 
listsum ~> sum_list 

371 
listprod ~> prod_list 

372 

373 
INCOMPATIBILITY. 

374 

375 
* Sligthly more standardized theorem names: 

376 
sgn_times ~> sgn_mult 

377 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

378 
divide_zero_left ~> div_0 

379 
zero_mod_left ~> mod_0 

380 
divide_zero ~> div_by_0 

381 
divide_1 ~> div_by_1 

382 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

383 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

384 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

385 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

386 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

387 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

388 
mod_div_equality ~> div_mult_mod_eq 

389 
mod_div_equality2 ~> mult_div_mod_eq 

390 
mod_div_equality3 ~> mod_div_mult_eq 

391 
mod_div_equality4 ~> mod_mult_div_eq 

392 
minus_div_eq_mod ~> minus_div_mult_eq_mod 

393 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 

394 
minus_mod_eq_div ~> minus_mod_eq_div_mult 

395 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 

396 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 

397 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

398 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 

399 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

400 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

401 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

402 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

403 
div_1 ~> div_by_Suc_0 

404 
mod_1 ~> mod_by_Suc_0 

405 
INCOMPATIBILITY. 

406 

407 
* New type class "idom_abs_sgn" specifies algebraic properties 

408 
of sign and absolute value functions. Type class "sgn_if" has 

409 
disappeared. Slight INCOMPATIBILITY. 

410 

411 
* Dedicated syntax LENGTH('a) for length of types. 

412 

63977  413 
* Characters (type char) are modelled as finite algebraic type 
414 
corresponding to {0..255}. 

415 

416 
 Logical representation: 

417 
* 0 is instantiated to the ASCII zero character. 

418 
* All other characters are represented as "Char n" 

419 
with n being a raw numeral expression less than 256. 

420 
* Expressions of the form "Char n" with n greater than 255 

421 
are noncanonical. 

422 
 Printing and parsing: 

423 
* Printable characters are printed and parsed as "CHR ''\<dots>''" 

424 
(as before). 

425 
* The ASCII zero character is printed and parsed as "0". 

426 
* All other canonical characters are printed as "CHR 0xXX" 

427 
with XX being the hexadecimal character code. "CHR n" 

428 
is parsable for every numeral expression n. 

429 
* Noncanonical characters have no special syntax and are 

430 
printed as their logical representation. 

431 
 Explicit conversions from and to the natural numbers are 

432 
provided as char_of_nat, nat_of_char (as before). 

433 
 The auxiliary nibble type has been discontinued. 

434 

435 
INCOMPATIBILITY. 

436 

437 
* Type class "div" with operation "mod" renamed to type class "modulo" 

438 
with operation "modulo", analogously to type class "divide". This 

439 
eliminates the need to qualify any of those names in the presence of 

440 
infix "mod" syntax. INCOMPATIBILITY. 

441 

63979  442 
* Statements and proofs of KnasterTarski fixpoint combinators lfp/gfp 
443 
have been clarified. The fixpoint properties are lfp_fixpoint, its 

444 
symmetric lfp_unfold (as before), and the duals for gfp. Auxiliary items 

445 
for the proof (lfp_lemma2 etc.) are no longer exported, but can be 

446 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

447 

63977  448 
* Constant "surj" is a mere input abbreviation, to avoid hiding an 
449 
equation in term output. Minor INCOMPATIBILITY. 

450 

451 
* Command 'code_reflect' accepts empty constructor lists for datatypes, 

452 
which renders those abstract effectively. 

453 

454 
* Command 'export_code' checks given constants for abstraction 

455 
violations: a small guarantee that given constants specify a safe 

456 
interface for the generated code. 

457 

458 
* Code generation for Scala: ambiguous implicts in class diagrams are 

459 
spelt out explicitly. 

460 

461 
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on 

462 
explicitly provided auxiliary definitions for required type class 

64390  463 
dictionaries rather than halfworking magic. INCOMPATIBILITY, see the 
464 
tutorial on code generation for details. 

465 

466 
* Theory Set_Interval: substantial new theorems on indexed sums and 

467 
products. 

63977  468 

469 
* Locale bijection establishes convenient default simp rules such as 

470 
"inv f (f a) = a" for total bijections. 

471 

472 
* Abstract locales semigroup, abel_semigroup, semilattice, 

473 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

474 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

475 
semilattice_neutr_set, semilattice_order_set, 

476 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

477 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

478 
syntax uniformly that does not clash with corresponding global syntax. 

479 
INCOMPATIBILITY. 

480 

481 
* Former locale lifting_syntax is now a bundle, which is easier to 

482 
include in a local context or theorem statement, e.g. "context includes 

483 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

484 

63807  485 
* Some old / obsolete theorems have been renamed / removed, potential 
486 
INCOMPATIBILITY. 

487 

488 
nat_less_cases  removed, use linorder_cases instead 

489 
inv_image_comp  removed, use image_inv_f_f instead 

490 
image_surj_f_inv_f ~> image_f_inv_f 

63113  491 

63456
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

492 
* Some theorems about groups and orders have been generalised from 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

493 
groups to semigroups that are also monoids: 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

494 
le_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

495 
le_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

496 
less_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

497 
less_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

498 
add_le_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

499 
add_le_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

500 
add_less_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

501 
add_less_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

502 

3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

503 
* Some simplifications theorems about rings have been removed, since 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

504 
superseeded by a more general version: 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

505 
less_add_cancel_left_greater_zero ~> less_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

506 
less_add_cancel_right_greater_zero ~> less_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

507 
less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

508 
less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

509 
less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

510 
less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

511 
less_add_cancel_left_less_zero ~> add_less_same_cancel1 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

512 
less_add_cancel_right_less_zero ~> add_less_same_cancel2 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

513 
INCOMPATIBILITY. 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

514 

62407  515 
* Renamed split_if > if_split and split_if_asm > if_split_asm to 
516 
resemble the f.split naming convention, INCOMPATIBILITY. 

62396  517 

63977  518 
* Added class topological_monoid. 
519 

64391  520 
* The following theorems have been renamed: 
521 

64457  522 
setsum_left_distrib ~> sum_distrib_right 
523 
setsum_right_distrib ~> sum_distrib_left 

64391  524 

525 
INCOMPATIBILITY. 

526 

527 
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 

528 
INCOMPATIBILITY. 

529 

530 
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 

531 
comprehensionlike syntax analogously to "Inf (f ` A)" and "Sup (f ` 

532 
A)". 

533 

534 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 

535 

536 
* The type class ordered_comm_monoid_add is now called 

537 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 

538 
is introduced as the combination of ordered_ab_semigroup_add + 

539 
comm_monoid_add. INCOMPATIBILITY. 

540 

541 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

542 
dioid. 

543 

544 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 

545 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 

546 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

547 
be required. INCOMPATIBILITY. 

63117  548 

62348  549 
* Dropped various legacy fact bindings, whose replacements are often 
550 
of a more general type also: 

551 
lcm_left_commute_nat ~> lcm.left_commute 

552 
lcm_left_commute_int ~> lcm.left_commute 

553 
gcd_left_commute_nat ~> gcd.left_commute 

554 
gcd_left_commute_int ~> gcd.left_commute 

555 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

556 
gcd_greatest_iff_int ~> gcd_greatest_iff 

557 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

558 
coprime_dvd_mult_int ~> coprime_dvd_mult 

559 
zpower_numeral_even ~> power_numeral_even 

560 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

561 
gcd_mult_cancel_int ~> gcd_mult_cancel 

562 
div_gcd_coprime_nat ~> div_gcd_coprime 

563 
div_gcd_coprime_int ~> div_gcd_coprime 

564 
zpower_numeral_odd ~> power_numeral_odd 

565 
zero_less_int_conv ~> of_nat_0_less_iff 

566 
gcd_greatest_nat ~> gcd_greatest 

567 
gcd_greatest_int ~> gcd_greatest 

568 
coprime_mult_nat ~> coprime_mult 

569 
coprime_mult_int ~> coprime_mult 

570 
lcm_commute_nat ~> lcm.commute 

571 
lcm_commute_int ~> lcm.commute 

572 
int_less_0_conv ~> of_nat_less_0_iff 

573 
gcd_commute_nat ~> gcd.commute 

574 
gcd_commute_int ~> gcd.commute 

575 
Gcd_insert_nat ~> Gcd_insert 

576 
Gcd_insert_int ~> Gcd_insert 

577 
of_int_int_eq ~> of_int_of_nat_eq 

578 
lcm_least_nat ~> lcm_least 

579 
lcm_least_int ~> lcm_least 

580 
lcm_assoc_nat ~> lcm.assoc 

581 
lcm_assoc_int ~> lcm.assoc 

582 
int_le_0_conv ~> of_nat_le_0_iff 

583 
int_eq_0_conv ~> of_nat_eq_0_iff 

584 
Gcd_empty_nat ~> Gcd_empty 

585 
Gcd_empty_int ~> Gcd_empty 

586 
gcd_assoc_nat ~> gcd.assoc 

587 
gcd_assoc_int ~> gcd.assoc 

588 
zero_zle_int ~> of_nat_0_le_iff 

589 
lcm_dvd2_nat ~> dvd_lcm2 

590 
lcm_dvd2_int ~> dvd_lcm2 

591 
lcm_dvd1_nat ~> dvd_lcm1 

592 
lcm_dvd1_int ~> dvd_lcm1 

593 
gcd_zero_nat ~> gcd_eq_0_iff 

594 
gcd_zero_int ~> gcd_eq_0_iff 

595 
gcd_dvd2_nat ~> gcd_dvd2 

596 
gcd_dvd2_int ~> gcd_dvd2 

597 
gcd_dvd1_nat ~> gcd_dvd1 

598 
gcd_dvd1_int ~> gcd_dvd1 

599 
int_numeral ~> of_nat_numeral 

600 
lcm_ac_nat ~> ac_simps 

601 
lcm_ac_int ~> ac_simps 

602 
gcd_ac_nat ~> ac_simps 

603 
gcd_ac_int ~> ac_simps 

604 
abs_int_eq ~> abs_of_nat 

605 
zless_int ~> of_nat_less_iff 

606 
zdiff_int ~> of_nat_diff 

607 
zadd_int ~> of_nat_add 

608 
int_mult ~> of_nat_mult 

609 
int_Suc ~> of_nat_Suc 

610 
inj_int ~> inj_of_nat 

611 
int_1 ~> of_nat_1 

612 
int_0 ~> of_nat_0 

62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

613 
Lcm_empty_nat ~> Lcm_empty 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

614 
Lcm_empty_int ~> Lcm_empty 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

615 
Lcm_insert_nat ~> Lcm_insert 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

616 
Lcm_insert_int ~> Lcm_insert 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

617 
comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

618 
comp_fun_idem_gcd_int ~> comp_fun_idem_gcd 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

619 
comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

620 
comp_fun_idem_lcm_int ~> comp_fun_idem_lcm 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

621 
Lcm_eq_0 ~> Lcm_eq_0_I 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

622 
Lcm0_iff ~> Lcm_0_iff 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

623 
Lcm_dvd_int ~> Lcm_least 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

624 
divides_mult_nat ~> divides_mult 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

625 
divides_mult_int ~> divides_mult 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

626 
lcm_0_nat ~> lcm_0_right 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

627 
lcm_0_int ~> lcm_0_right 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

628 
lcm_0_left_nat ~> lcm_0_left 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

629 
lcm_0_left_int ~> lcm_0_left 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

630 
dvd_gcd_D1_nat ~> dvd_gcdD1 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

631 
dvd_gcd_D1_int ~> dvd_gcdD1 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

632 
dvd_gcd_D2_nat ~> dvd_gcdD2 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

633 
dvd_gcd_D2_int ~> dvd_gcdD2 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

634 
coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff 
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

635 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  636 
realpow_minus_mult ~> power_minus_mult 
637 
realpow_Suc_le_self ~> power_Suc_le_self 

62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset

638 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  639 
INCOMPATIBILITY. 
640 

63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset

641 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  642 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
643 

64390  644 
* Session HOLLibrary: theory FinFun bundles "finfun_syntax" and 
645 
"no_finfun_syntax" allow to control optional syntax in local contexts; 

646 
this supersedes former theory FinFun_Syntax. INCOMPATIBILITY, e.g. use 

647 
"unbundle finfun_syntax" to imitate import of 

648 
"~~/src/HOL/Library/FinFun_Syntax". 

649 

650 
* Session HOLLibrary: theory Multiset_Permutations (executably) defines 

651 
the set of permutations of a given set or multiset, i.e. the set of all 

652 
lists that contain every element of the carrier (multi)set exactly 

653 
once. 

654 

655 
* Session HOLLibrary: multiset membership is now expressed using 

656 
set_mset rather than count. 

657 

658 
 Expressions "count M a > 0" and similar simplify to membership 

659 
by default. 

660 

661 
 Converting between "count M a = 0" and nonmembership happens using 

662 
equations count_eq_zero_iff and not_in_iff. 

663 

664 
 Rules count_inI and in_countE obtain facts of the form 

665 
"count M a = n" from membership. 

666 

667 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 

668 
"count M a = n + count N a" from membership on difference sets. 

669 

670 
INCOMPATIBILITY. 

671 

672 
* Session HOLLibrary: theory LaTeXsugar uses newstyle "dummy_pats" for 

673 
displaying equations in functional programming style  variables 

674 
present on the lefthand but not on the righhand side are replaced by 

675 
underscores. 

676 

677 
* Session HOLLibrary: theory Combinator_PER provides combinator to 

678 
build partial equivalence relations from a predicate and an equivalence 

679 
relation. 

680 

681 
* Session HOLLibrary: theory Perm provides basic facts about almost 

682 
everywhere fix bijections. 

683 

684 
* Session HOLLibrary: theory Normalized_Fraction allows viewing an 

685 
element of a field of fractions as a normalized fraction (i.e. a pair of 

686 
numerator and denominator such that the two are coprime and the 

687 
denominator is normalized wrt. unit factors). 

688 

689 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

690 

691 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

692 

693 
* Session HOLAnalysis: measure theory has been moved here from 

694 
HOLProbability. When importing HOLAnalysis some theorems need 

695 
additional name spaces prefixes due to name clashes. INCOMPATIBILITY. 

696 

697 
* Session HOLAnalysis: more complex analysis including Cauchy's 

698 
inequality, Liouville theorem, open mapping theorem, maximum modulus 

699 
principle, Residue theorem, Schwarz Lemma. 

700 

701 
* Session HOLAnalysis: Theory of polyhedra: faces, extreme points, 

702 
polytopes, and the Kreinâ€“Milman Minkowski theorem. 

703 

704 
* Session HOLAnalysis: Numerous results ported from the HOL Light 

705 
libraries: homeomorphisms, continuous function extensions, invariance of 

706 
domain. 

707 

708 
* Session HOLProbability: the type of emeasure and nn_integral was 

709 
changed from ereal to ennreal, INCOMPATIBILITY. 

710 

711 
emeasure :: 'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal 

712 
nn_integral :: 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal 

713 

714 
* Session HOLProbability: Code generation and QuickCheck for 

715 
Probability Mass Functions. 

716 

717 
* Session HOLProbability: theory Random_Permutations contains some 

718 
theory about choosing a permutation of a set uniformly at random and 

719 
folding over a list in random order. 

720 

721 
* Session HOLProbability: theory SPMF formalises discrete 

722 
subprobability distributions. 

723 

724 
* Session HOLLibrary: the names of multiset theorems have been 

725 
normalised to distinguish which ordering the theorems are about 

726 

727 
mset_less_eqI ~> mset_subset_eqI 

728 
mset_less_insertD ~> mset_subset_insertD 

729 
mset_less_eq_count ~> mset_subset_eq_count 

730 
mset_less_diff_self ~> mset_subset_diff_self 

731 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 

732 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 

733 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 

734 
mset_le_mono_add ~> mset_subset_eq_mono_add 

735 
mset_le_add_left ~> mset_subset_eq_add_left 

736 
mset_le_add_right ~> mset_subset_eq_add_right 

737 
mset_le_single ~> mset_subset_eq_single 

738 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 

739 
diff_le_self ~> diff_subset_eq_self 

740 
mset_leD ~> mset_subset_eqD 

741 
mset_lessD ~> mset_subsetD 

742 
mset_le_insertD ~> mset_subset_eq_insertD 

743 
mset_less_of_empty ~> mset_subset_of_empty 

744 
mset_less_size ~> mset_subset_size 

745 
wf_less_mset_rel ~> wf_subset_mset_rel 

746 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 

747 
mset_remdups_le ~> mset_remdups_subset_eq 

748 
ms_lesseq_impl ~> subset_eq_mset_impl 

749 

750 
Some functions have been renamed: 

751 
ms_lesseq_impl > subset_eq_mset_impl 

752 

753 
* HOLLibrary: multisets are now ordered with the multiset ordering 

754 
#\<subseteq># ~> \<le> 

755 
#\<subset># ~> < 

756 
le_multiset ~> less_eq_multiset 

757 
less_multiset ~> le_multiset 

758 
INCOMPATIBILITY. 

759 

760 
* Session HOLLibrary: the prefix multiset_order has been discontinued: 

761 
the theorems can be directly accessed. As a consequence, the lemmas 

762 
"order_multiset" and "linorder_multiset" have been discontinued, and the 

763 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

764 
replaced by instantiations. INCOMPATIBILITY. 

765 

766 
* Session HOLLibrary: some theorems about the multiset ordering have 

767 
been renamed: 

768 

769 
le_multiset_def ~> less_eq_multiset_def 

770 
less_multiset_def ~> le_multiset_def 

771 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 

772 
mult_less_not_refl ~> mset_le_not_refl 

773 
mult_less_trans ~> mset_le_trans 

774 
mult_less_not_sym ~> mset_le_not_sym 

775 
mult_less_asym ~> mset_le_asym 

776 
mult_less_irrefl ~> mset_le_irrefl 

777 
union_less_mono2{,1,2} ~> union_le_mono2{,1,2} 

778 

779 
le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O 

780 
le_multiset_total ~> less_eq_multiset_total 

781 
less_multiset_right_total ~> subset_eq_imp_le_multiset 

782 
le_multiset_empty_left ~> less_eq_multiset_empty_left 

783 
le_multiset_empty_right ~> less_eq_multiset_empty_right 

784 
less_multiset_empty_right ~> le_multiset_empty_left 

785 
less_multiset_empty_left ~> le_multiset_empty_right 

786 
union_less_diff_plus ~> union_le_diff_plus 

787 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 

788 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 

789 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 

790 
INCOMPATIBILITY. 

791 

792 
* Session HOLLibrary: the lemma mset_map has now the attribute [simp]. 

793 
INCOMPATIBILITY. 

794 

795 
* Session HOLLibrary: some theorems about multisets have been removed. 

796 
INCOMPATIBILITY, use the following replacements: 

797 

798 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 

799 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 

800 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 

801 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 

802 
add_eq_self_empty_iff ~> add_cancel_left_right 

803 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 

804 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 

805 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 

806 
empty_inter ~> subset_mset.inf_bot_left 

807 
inter_empty ~> subset_mset.inf_bot_right 

808 
empty_sup ~> subset_mset.sup_bot_left 

809 
sup_empty ~> subset_mset.sup_bot_right 

810 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

811 
subset_eq_empty ~> subset_mset.le_zero_eq 

812 
le_empty ~> subset_mset.le_zero_eq 

813 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

814 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

815 

816 
* Session HOLLibrary: some typeclass constraints about multisets have 

817 
been reduced from ordered or linordered to preorder. Multisets have the 

818 
additional typeclasses order_bot, no_top, 

819 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

820 
linordered_cancel_ab_semigroup_add, and 

821 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

822 

823 
* Session HOLLibrary: there are some new simplification rules about 

824 
multisets, the multiset ordering, and the subset ordering on multisets. 

825 
INCOMPATIBILITY. 

826 

827 
* Session HOLLibrary: the subset ordering on multisets has now the 

828 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

829 
bounded_lattice_bot. INCOMPATIBILITY. 

830 

831 
* Session HOLLibrary, theory Multiset: single has been removed in favor 

832 
of add_mset that roughly corresponds to Set.insert. Some theorems have 

833 
removed or changed: 

834 

835 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 

836 
fold_mset_insert ~> fold_mset_add_mset 

837 
image_mset_insert ~> image_mset_add_mset 

838 
union_single_eq_diff 

839 
multi_self_add_other_not_self 

840 
diff_single_eq_union 

841 
INCOMPATIBILITY. 

842 

843 
* Session HOLLibrary, theory Multiset: some theorems have been changed 

844 
to use add_mset instead of single: 

845 

846 
mset_add 

847 
multi_self_add_other_not_self 

848 
diff_single_eq_union 

849 
union_single_eq_diff 

850 
union_single_eq_member 

851 
add_eq_conv_diff 

852 
insert_noteq_member 

853 
add_eq_conv_ex 

854 
multi_member_split 

855 
multiset_add_sub_el_shuffle 

856 
mset_subset_eq_insertD 

857 
mset_subset_insertD 

858 
insert_subset_eq_iff 

859 
insert_union_subset_iff 

860 
multi_psub_of_add_self 

861 
inter_add_left1 

862 
inter_add_left2 

863 
inter_add_right1 

864 
inter_add_right2 

865 
sup_union_left1 

866 
sup_union_left2 

867 
sup_union_right1 

868 
sup_union_right2 

869 
size_eq_Suc_imp_eq_union 

870 
multi_nonempty_split 

871 
mset_insort 

872 
mset_update 

873 
mult1I 

874 
less_add 

875 
mset_zip_take_Cons_drop_twice 

876 
rel_mset_Zero 

877 
msed_map_invL 

878 
msed_map_invR 

879 
msed_rel_invL 

880 
msed_rel_invR 

881 
le_multiset_right_total 

882 
multiset_induct 

883 
multiset_induct2_size 

884 
multiset_induct2 

885 
INCOMPATIBILITY. 

886 

887 
* Session HOLLibrary, theory Multiset: the definitions of some 

888 
constants have changed to use add_mset instead of adding a single 

889 
element: 

890 

891 
image_mset 

892 
mset 

893 
replicate_mset 

894 
mult1 

895 
pred_mset 

896 
rel_mset' 

897 
mset_insort 

898 

899 
INCOMPATIBILITY. 

900 

901 
* Session HOLLibrary, theory Multiset: due to the above changes, the 

902 
attributes of some multiset theorems have been changed: 

903 

904 
insert_DiffM [] ~> [simp] 

905 
insert_DiffM2 [simp] ~> [] 

906 
diff_add_mset_swap [simp] 

907 
fold_mset_add_mset [simp] 

908 
diff_diff_add [simp] (for multisets only) 

909 
diff_cancel [simp] ~> [] 

910 
count_single [simp] ~> [] 

911 
set_mset_single [simp] ~> [] 

912 
size_multiset_single [simp] ~> [] 

913 
size_single [simp] ~> [] 

914 
image_mset_single [simp] ~> [] 

915 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 

916 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 

917 
fold_mset_single [simp] ~> [] 

918 
subset_eq_empty [simp] ~> [] 

919 
empty_sup [simp] ~> [] 

920 
sup_empty [simp] ~> [] 

921 
inter_empty [simp] ~> [] 

922 
empty_inter [simp] ~> [] 

923 
INCOMPATIBILITY. 

924 

64391  925 
* Session HOLLibrary, theory Multiset: the order of the variables in 
64390  926 
the second cases of multiset_induct, multiset_induct2_size, 
927 
multiset_induct2 has been changed (e.g. Add A a ~> Add a A). 

928 
INCOMPATIBILITY. 

929 

930 
* Session HOLLibrary, theory Multiset: there is now a simplification 

931 
procedure on multisets. It mimics the behavior of the procedure on 

932 
natural numbers. INCOMPATIBILITY. 

933 

934 
* Session HOLLibrary, theory Multiset: renamed sums and products of 

935 
multisets: 

936 

937 
msetsum ~> sum_mset 

938 
msetprod ~> prod_mset 

939 

940 
* Session HOLLibrary, theory Multiset: the notation for intersection 

941 
and union of multisets have been changed: 

942 

943 
#\<inter> ~> \<inter># 

944 
#\<union> ~> \<union># 

945 

946 
INCOMPATIBILITY. 

947 

948 
* Session HOLLibrary, theory Multiset: the lemma 

949 
one_step_implies_mult_aux on multisets has been removed, use 

950 
one_step_implies_mult instead. INCOMPATIBILITY. 

951 

952 
* Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 

953 
support for monotonicity and continuity in chaincomplete partial orders 

954 
and about admissibility conditions for fixpoint inductions. 

955 

64523  956 
* Session HOLLibrary: theory Library/Polynomial contains also 
957 
derivation of polynomials (formerly in Library/Poly_Deriv) but not 

958 
gcd/lcm on polynomials over fields. This has been moved to a separate 

959 
theory Library/Polynomial_GCD_euclidean.thy, to pave way for a possible 

960 
future different type class instantiation for polynomials over factorial 

961 
rings. INCOMPATIBILITY. 

64390  962 

963 
* Session HOLLibrary: theory Sublist provides function "prefixes" with 

964 
the following renaming 

965 

966 
prefixeq > prefix 

967 
prefix > strict_prefix 

968 
suffixeq > suffix 

969 
suffix > strict_suffix 

970 

971 
Added theory of longest common prefixes. 

64389  972 

64391  973 
* Session HOLNumber_Theory: algebraic foundation for primes: 
974 
Generalisation of predicate "prime" and introduction of predicates 

975 
"prime_elem", "irreducible", a "prime_factorization" function, and the 

976 
"factorial_ring" typeclass with instance proofs for nat, int, poly. Some 

977 
theorems now have different names, most notably "prime_def" is now 

978 
"prime_nat_iff". INCOMPATIBILITY. 

979 

980 
* Session Old_Number_Theory has been removed, after porting remaining 

981 
theories. 

982 

64551  983 
* Session HOLTypes_To_Sets provides an experimental extension of 
984 
HigherOrder Logic to allow translation of types to sets. 

985 

63198
c583ca33076a
adhoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset

986 

62498  987 
*** ML *** 
988 

63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset

989 
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML 
63228  990 
library (notably for big integers). Subtle change of semantics: 
991 
Integer.gcd and Integer.lcm both normalize the sign, results are never 

992 
negative. This coincides with the definitions in HOL/GCD.thy. 

993 
INCOMPATIBILITY. 

63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset

994 

63212  995 
* Structure Rat for rational numbers is now an integral part of 
63215  996 
Isabelle/ML, with special notation @int/nat or @int for numerals (an 
997 
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty 

63212  998 
printing. Standard operations on type Rat.rat are provided via adhoc 
63215  999 
overloading of +  * / < <= > >= ~ abs. INCOMPATIBILITY, need to 
63212  1000 
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been 
1001 
superseded by General.Div. 

63198
c583ca33076a
adhoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset

1002 

64390  1003 
* ML antiquotation @{path} is superseded by @{file}, which ensures that 
1004 
the argument is a plain file. Minor INCOMPATIBILITY. 

1005 

1006 
* Antiquotation @{make_string} is available during Pure bootstrap  

1007 
with approximative output quality. 

1008 

1009 
* Lowlevel ML system structures (like PolyML and RunCall) are no longer 

1010 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 

1011 

62861  1012 
* The ML function "ML" provides easy access to runtime compilation. 
1013 
This is particularly useful for conditional compilation, without 

1014 
requiring separate files. 

1015 

62498  1016 
* Option ML_exception_debugger controls detailed exception trace via the 
1017 
Poly/ML debugger. Relevant ML modules need to be compiled beforehand 

1018 
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note 

1019 
debugger information requires consirable time and space: main 

1020 
Isabelle/HOL with full debugger support may need ML_system_64. 

1021 

62514  1022 
* Local_Theory.restore has been renamed to Local_Theory.reset to 
1023 
emphasize its disruptive impact on the cumulative context, notably the 

1024 
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is 

1025 
only appropriate when targets are managed, e.g. starting from a global 

1026 
theory and returning to it. Regular definitional packages should use 

1027 
balanced blocks of Local_Theory.open_target versus 

1028 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

1029 

62519  1030 
* Structure TimeLimit (originally from the SML/NJ library) has been 
1031 
replaced by structure Timeout, with slightly different signature. 

1032 
INCOMPATIBILITY. 

1033 

62551  1034 
* Discontinued cd and pwd operations, which are not welldefined in a 
1035 
multithreaded environment. Note that files are usually located 

1036 
relatively to the master directory of a theory (see also 

1037 
File.full_path). Potential INCOMPATIBILITY. 

1038 

63352  1039 
* Binding.empty_atts supersedes Thm.empty_binding and 
1040 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

1041 

62498  1042 

62354  1043 
*** System *** 
1044 

64390  1045 
* SML/NJ and old versions of Poly/ML are no longer supported. 
1046 

1047 
* Poly/ML heaps now follow the hierarchy of sessions, and thus require 

1048 
much less disk space. 

63226  1049 

62591  1050 
* The Isabelle ML process is now managed directly by Isabelle/Scala, and 
1051 
shell scripts merely provide optional commandline access. In 

1052 
particular: 

1053 

1054 
. Scala module ML_Process to connect to the raw ML process, 

1055 
with interaction via stdin/stdout/stderr or in batch mode; 

1056 
. commandline tool "isabelle console" as interactive wrapper; 

1057 
. commandline tool "isabelle process" as batch mode wrapper. 

62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1058 

cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1059 
* The executable "isabelle_process" has been discontinued. Tools and 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1060 
prover frontends should use ML_Process or Isabelle_Process in 
62591  1061 
Isabelle/Scala. INCOMPATIBILITY. 
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1062 

cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1063 
* New commandline tool "isabelle process" supports ML evaluation of 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1064 
literal expressions (option e) or files (option f) in the context of a 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1065 
given heap image. Errors lead to premature exit of the ML process with 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1066 
return code 1. 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1067 

64390  1068 
* The commandline tool "isabelle build" supports option N for cyclic 
1069 
shuffling of NUMA CPU nodes. This may help performance tuning on Linux 

1070 
servers with separate CPU/memory modules. 

1071 

1072 
* System option "threads" (for the size of the Isabelle/ML thread farm) 

1073 
is also passed to the underlying ML runtime system as gcthreads, 

64274  1074 
unless there is already a default provided via ML_OPTIONS settings. 
1075 

63827
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1076 
* System option "checkpoint" helps to finetune the global heap space 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1077 
management of isabelle build. This is relevant for big sessions that may 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1078 
exhaust the small 32bit address space of the ML process (which is used 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1079 
by default). 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63821
diff
changeset

1080 

64308  1081 
* System option "profiling" specifies the mode for global ML profiling 
64342  1082 
in "isabelle build". Possible values are "time", "allocations". The 
1083 
commandline tool "isabelle profiling_report" helps to digest the 

1084 
resulting log files. 

64308  1085 

63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1086 
* System option "ML_process_policy" specifies an optional command prefix 
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1087 
for the underlying ML process, e.g. to control CPU affinity on 
63987
ac96fe9224f6
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents:
63986
diff
changeset

1088 
multiprocessor systems. The "isabelle jedit" tool allows to override the 
ac96fe9224f6
just one option is enough  "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents:
63986
diff
changeset

1089 
implicit default via option p. 
63986
c7a4b03727ae
options for process policy, notably for multiprocessor machines;
wenzelm
parents:
63979
diff
changeset

1090 

64390  1091 
* Commandline tool "isabelle console" provides option r to help to 
1092 
bootstrapping Isabelle/Pure interactively. 

1093 

1094 
* Commandline tool "isabelle yxml" has been discontinued. 

1095 
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in 

1096 
Isabelle/ML or Isabelle/Scala. 

1097 

1098 
* Many Isabelle tools that require a Java runtime system refer to the 

1099 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 

1100 
depending on the underlying platform. The settings for "isabelle build" 

1101 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 

1102 
discontinued. Potential INCOMPATIBILITY. 

1103 

1104 
* The Isabelle system environment always ensures that the main 

1105 
executables are found within the shell search $PATH: "isabelle" and 

1106 
"isabelle_scala_script". 

1107 

1108 
* Isabelle tools may consist of .scala files: the Scala compiler is 

1109 
invoked on the spot. The source needs to define some object that extends 

1110 
Isabelle_Tool.Body. 

1111 

1112 
* File.bash_string, File.bash_path etc. represent Isabelle/ML and 

1113 
Isabelle/Scala strings authentically within GNU bash. This is useful to 

1114 
produce robust shell scripts under program control, without worrying 

1115 
about spaces or special characters. Note that user output works via 

1116 
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and 

1117 
less versatile) operations File.shell_quote, File.shell_path etc. have 

1118 
been discontinued. 

1119 

63995  1120 
* The isabelle_java executable allows to run a Java process within the 
1121 
name space of Java and Scala components that are bundled with Isabelle, 

1122 
but without the Isabelle settings environment. 

1123 

64390  1124 
* Isabelle/Scala: the SSH module supports ssh and sftp connections, for 
1125 
remote commandexecution and filesystem access. This resembles 

1126 
operations from module File and Isabelle_System to some extent. Note 

1127 
that Path specifications need to be resolved remotely via 

1128 
ssh.remote_path instead of File.standard_path: the implicit process 

1129 
environment is different, Isabelle settings are not available remotely. 

1130 

1131 
* Isabelle/Scala: the Mercurial module supports repositories via the 

1132 
regular hg commandline interface. The repositroy clone and working 

1133 
directory may reside on a local or remote filesystem (via ssh 

1134 
connection). 

64265  1135 

62354  1136 

1137 

62031  1138 
New in Isabelle2016 (February 2016) 
62016  1139 
 
60138  1140 

61337  1141 
*** General *** 
1142 

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

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

1144 
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

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

1146 
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

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

1148 

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

1151 

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

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

1155 
has been removed (see below). 

1156 

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

62017  1159 

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

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

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

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

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

1164 

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

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

1166 
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

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

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

1169 

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

1172 
to update old sources. 

1173 

61337  1174 
* Toplevel theorem statements have been simplified as follows: 
1175 

1176 
theorems ~> lemmas 

1177 
schematic_lemma ~> schematic_goal 

1178 
schematic_theorem ~> schematic_goal 

1179 
schematic_corollary ~> schematic_goal 

1180 

1181 
Commandline tool "isabelle update_theorems" updates theory sources 

1182 
accordingly. 

1183 

61338  1184 
* Toplevel theorem statement 'proposition' is another alias for 
1185 
'theorem'. 

1186 

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

1189 
deferred definitions require a surrounding 'overloading' block. 

1190 

61337  1191 

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

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

1193 

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

1197 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1201 
any effect on the running ML program. 

60984  1202 

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

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

1206 
update. 

61729  1207 

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

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

1210 
enable option "editor_output_state". 

61215  1211 

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

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

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

1216 
visibility. 

1217 

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

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

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

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

1222 
panel. 

1223 

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

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

1225 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1226 

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

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

1229 
implicit: a popup will show up unconditionally. 

1230 

1231 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1234 

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

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

1236 
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

1237 
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

1238 
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

1239 

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

1242 
the editor. 

1243 

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

1245 
instead of former C+e LEFT. 

1246 

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

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

1249 
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

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

1251 

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

1254 
singleinstance applications seen on common GUI desktops. 

1255 

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

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

1257 
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

1258 
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

1259 

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

1262 

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

1265 

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

1266 

61405  1267 
*** Document preparation *** 
1268 

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

1271 

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

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

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

1275 

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

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

1278 
follows: 

1279 

1280 
\<^item> itemize 

1281 
\<^enum> enumerate 

1282 
\<^descr> description 

1283 

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

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

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

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

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

1290 

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

1293 
standard LaTeX macros of the same names. 

1294 

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

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

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

1299 
cartouche tokens seen in theory sources. 

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

1300 

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

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

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

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

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

1306 

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

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

1310 

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

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

1313 

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

1315 

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

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

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

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

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

1321 
documentation, with a hyperlink in the Prover IDE. 

1322 

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

1324 
entities of the Isar language. 

1325 

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

61488  1328 
print mode "HTML" loses its special meaning. 
61471  1329 

61405  1330 

60406  1331 
*** Isar *** 
1332 

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

1335 
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

1336 
example: 
60414  1337 

1338 
have result: "C x y" 

1339 
if "A x" and "B y" 

1340 
for x :: 'a and y :: 'a 

1341 
<proof> 

1342 

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

60414  1345 
corresponds to a raw proof block like this: 
1346 

1347 
{ 

1348 
fix x :: 'a and y :: 'a 

60449  1349 
assume that: "A x" "B y" 
60414  1350 
have "C x y" <proof> 
1351 
} 

1352 
note result = this 

60406  1353 

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

1354 
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

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

1356 

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

61658  1359 

1360 
assume result: "C x y" 

1361 
if "A x" and "B y" 

1362 
for x :: 'a and y :: 'a 

1363 

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

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

1366 

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

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

1369 
example: 

1370 

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

1372 

1373 
is equivalent to: 

1374 

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

1376 

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

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

60595  1381 

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

1383 

1384 
or: 

1385 

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

1387 

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

1389 

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

1391 

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

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

1395 
of the local context elements yet. 

1396 

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

1399 

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

1401 
then have something 

1402 
proof cases 

1403 
case a 

1404 
then show ?thesis <proof> 

1405 
next 

1406 
case b 

1407 
then show ?thesis <proof> 

1408 
next 

1409 
case c 

1410 
then show ?thesis <proof> 

1411 
qed 

1412 

60565  1413 
* Command 'case' allows fact name and attribute specification like this: 
1414 

1415 
case a: (c xs) 

1416 
case a [attributes]: (c xs) 

1417 

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

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

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

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

1422 
and always put attributes in front. 

1423 

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

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

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

1426 
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

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

1428 

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

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

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

1433 

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

1435 
supply [simp] = a 

1436 
proof 
