author  wenzelm 
Tue, 25 Oct 2016 12:14:17 +0200  
changeset 64391  553d8c4d7ef4 
parent 64390  ad2c5f37f659 
child 64439  2bafda87b524 
child 64457  f7aa4d0f7d02 
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 

64072  7 
New in Isabelle20161 (December 2016) 
8 
 

62216  9 

62440  10 
*** General *** 
11 

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

14 
INCOMPATIBILITY. 

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

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

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

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

19 
result the subgoal may be split into several subgoals. 

20 

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

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

24 

25 
bundle foo 

26 
begin 

27 
declare a [simp] 

28 
declare b [intro] 

29 
end 

63272  30 

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

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

34 

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

37 
discontinued. 

38 

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

40 
delimited uniformly via cartouches. This works better than oldfashioned 

41 
quotes when sublanguages are nested. 

42 

43 
* Mixfix annotations support general block properties, with syntax 

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

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

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

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

63650  48 

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

51 

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

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

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

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

57 
examples. 

58 

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

60 
instances) are generated into companion object of corresponding type 

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

62 

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

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

65 

62440  66 

62904  67 
*** Prover IDE  Isabelle/Scala/jEdit *** 
68 

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

71 
command keywords and some command substructure. Action 

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

73 
according to command keywords only; see also option 

74 
"jedit_indent_newline". 

75 

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

77 
number of subgoals. This requires information of ongoing document 

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

79 
quickly; see also option "jedit_script_indent" and 

80 
"jedit_script_indent_limit". 

81 

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

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

84 
structure of theory specifications is treated as well. 

85 

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

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

88 

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

90 
e.g. 'context', 'notepad'. 

91 

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

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

94 

63977  95 
* Highlighting of entity def/ref positions wrt. cursor. 
96 

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

98 
occurences of the formal entity at the caret position. This facilitates 

99 
systematic renaming. 

100 

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

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

103 
theorem statement. 

104 

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

106 
situations where old ASCII notation may be updated. 

107 

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

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

111 
inaccessible via keyboard completion). 

112 

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

115 

116 
src/Pure/ROOT0.ML 

117 
src/Pure/ROOT.ML 

118 
src/Pure/Pure.thy 

119 
src/Pure/ML_Bootstrap.thy 

120 

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

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

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

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

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

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

63307  127 
dependencies of the above files are only observed for batch build. 
62904  128 

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

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

63461  132 

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

136 
new 'abbrevs' section. 

137 

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

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

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

63579  141 

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

144 
keymap; nonconflicting changes are always applied implicitly. This 

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

146 
increases chances that users see new keyboard shortcuts when reusing 

147 
old keymaps. 

148 

63675  149 
* ML and document antiquotations for filesystems paths are more uniform 
150 
and diverse: 

151 

152 
@{path NAME}  no filesystem check 

153 
@{file NAME}  check for plain file 

154 
@{dir NAME}  check for directory 

155 

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

157 
have to be changed. 

63669  158 

159 

63977  160 
*** Document preparation *** 
161 

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

163 

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

166 

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

169 

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

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

172 
derivatives. 

173 

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

175 

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

177 
Isabelle2015). 

178 

179 

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

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

181 

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

184 
'definition', 'inductive', 'function'. 

185 

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

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

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

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

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

191 

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

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

63039  196 

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

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

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

199 

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

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

201 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  202 

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

205 

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

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

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

209 

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

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

212 
INCOMPATIBILITY. 

62939  213 

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

216 
definitions. 

217 

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

63259  220 

221 
(use facts in simp) 

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

223 

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

226 

62216  227 

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

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

229 

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

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

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

234 

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

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

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

238 
regardless of the actual parameters that are provided. Rare 

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

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

241 

242 
* Typeinference improves sorts of newly introduced type variables for 

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

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

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

246 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

247 
types where this is really intended. 

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

248 

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

249 

62327  250 
*** HOL *** 
251 

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

254 
propositional logic, goals based on a combination of quantifierfree 

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

256 
quantifierfree propositional logic with linear real arithmetic 

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

258 

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

261 

63977  262 
* Metis: The problem encoding has changed very slightly. This might 
63785  263 
break existing proofs. INCOMPATIBILITY. 
264 

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

266 
 The MaSh relevance filter is now faster than before. 
63116  267 
 Produce syntactically correct Vampire 4.0 problem files. 
268 

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

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

62842  273 
method. See 'isabelle doc corec'. 
63977  274 
 The predicator :: ('a \<Rightarrow> bool) \<Rightarrow> 'a F \<Rightarrow> bool is now a firstclass 
63855  275 
citizen in bounded natural functors. 
62693  276 
 'primrec' now allows nested calls through the predicator in addition 
62327  277 
to the map function. 
63855  278 
 'bnf' automatically discharges reflexive proof obligations. 
62693  279 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  280 
terms of map and set 
63855  281 
(not giving a specification for rel makes this one reflexive). 
62693  282 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  283 
(not giving a specification for pred makes this one reflexive). 
284 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  285 
 Renamed lemmas: 
286 
rel_prod_apply ~> rel_prod_inject 

287 
pred_prod_apply ~> pred_prod_inject 

288 
INCOMPATIBILITY. 

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

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

292 
INCOMPATIBILITY. 

62327  293 

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

296 
which exposed details of the internal fixpoint construction and was 

297 
hard to use. INCOMPATIBILITY. 

298 

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

300 

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

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

303 

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

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

306 
eliminated altogether. 

307 

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

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

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

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

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

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

314 
INCOMPATIBILITY in rare situations. 

315 

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

317 
INCOMPATIBILITY. 

318 

64390  319 
* Renamed constants and corresponding theorems: 
320 

321 
setsum ~> sum 

322 
setprod ~> prod 

323 
listsum ~> sum_list 

324 
listprod ~> prod_list 

325 

326 
INCOMPATIBILITY. 

327 

328 
* Sligthly more standardized theorem names: 

329 
sgn_times ~> sgn_mult 

330 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

331 
divide_zero_left ~> div_0 

332 
zero_mod_left ~> mod_0 

333 
divide_zero ~> div_by_0 

334 
divide_1 ~> div_by_1 

335 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

336 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

337 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

338 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

339 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

340 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

341 
mod_div_equality ~> div_mult_mod_eq 

342 
mod_div_equality2 ~> mult_div_mod_eq 

343 
mod_div_equality3 ~> mod_div_mult_eq 

344 
mod_div_equality4 ~> mod_mult_div_eq 

345 
minus_div_eq_mod ~> minus_div_mult_eq_mod 

346 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 

347 
minus_mod_eq_div ~> minus_mod_eq_div_mult 

348 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 

349 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 

350 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

351 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 

352 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

353 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

354 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

355 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

356 
div_1 ~> div_by_Suc_0 

357 
mod_1 ~> mod_by_Suc_0 

358 
INCOMPATIBILITY. 

359 

360 
* New type class "idom_abs_sgn" specifies algebraic properties 

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

362 
disappeared. Slight INCOMPATIBILITY. 

363 

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

365 

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

368 

369 
 Logical representation: 

370 
* 0 is instantiated to the ASCII zero character. 

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

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

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

374 
are noncanonical. 

375 
 Printing and parsing: 

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

377 
(as before). 

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

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

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

381 
is parsable for every numeral expression n. 

382 
* Noncanonical characters have no special syntax and are 

383 
printed as their logical representation. 

384 
 Explicit conversions from and to the natural numbers are 

385 
provided as char_of_nat, nat_of_char (as before). 

386 
 The auxiliary nibble type has been discontinued. 

387 

388 
INCOMPATIBILITY. 

389 

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

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

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

393 
infix "mod" syntax. INCOMPATIBILITY. 

394 

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

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

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

399 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

400 

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

403 

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

405 
which renders those abstract effectively. 

406 

407 
* Command 'export_code' checks given constants for abstraction 

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

409 
interface for the generated code. 

410 

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

412 
spelt out explicitly. 

413 

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

415 
explicitly provided auxiliary definitions for required type class 

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

418 

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

420 
products. 

63977  421 

422 
* Locale bijection establishes convenient default simp rules such as 

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

424 

425 
* Abstract locales semigroup, abel_semigroup, semilattice, 

426 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

427 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

428 
semilattice_neutr_set, semilattice_order_set, 

429 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

430 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

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

432 
INCOMPATIBILITY. 

433 

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

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

436 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

437 

63807  438 
* Some old / obsolete theorems have been renamed / removed, potential 
439 
INCOMPATIBILITY. 

440 

441 
nat_less_cases  removed, use linorder_cases instead 

442 
inv_image_comp  removed, use image_inv_f_f instead 

443 
image_surj_f_inv_f ~> image_f_inv_f 

63113  444 

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

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

446 
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

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

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

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

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

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

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

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

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

455 

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

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

457 
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

458 
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

459 
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

460 
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

461 
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

462 
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

463 
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

464 
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

465 
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

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

467 

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

62396  470 

63977  471 
* Added class topological_monoid. 
472 

64391  473 
* The following theorems have been renamed: 
474 

475 
setsum_left_distrib ~> setsum_distrib_right 

476 
setsum_right_distrib ~> setsum_distrib_left 

477 

478 
INCOMPATIBILITY. 

479 

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

481 
INCOMPATIBILITY. 

482 

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

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

485 
A)". 

486 

487 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 

488 

489 
* The type class ordered_comm_monoid_add is now called 

490 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 

491 
is introduced as the combination of ordered_ab_semigroup_add + 

492 
comm_monoid_add. INCOMPATIBILITY. 

493 

494 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

495 
dioid. 

496 

497 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 

498 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 

499 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

500 
be required. INCOMPATIBILITY. 

63117  501 

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

504 
lcm_left_commute_nat ~> lcm.left_commute 

505 
lcm_left_commute_int ~> lcm.left_commute 

506 
gcd_left_commute_nat ~> gcd.left_commute 

507 
gcd_left_commute_int ~> gcd.left_commute 

508 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

509 
gcd_greatest_iff_int ~> gcd_greatest_iff 

510 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

511 
coprime_dvd_mult_int ~> coprime_dvd_mult 

512 
zpower_numeral_even ~> power_numeral_even 

513 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

514 
gcd_mult_cancel_int ~> gcd_mult_cancel 

515 
div_gcd_coprime_nat ~> div_gcd_coprime 

516 
div_gcd_coprime_int ~> div_gcd_coprime 

517 
zpower_numeral_odd ~> power_numeral_odd 

518 
zero_less_int_conv ~> of_nat_0_less_iff 

519 
gcd_greatest_nat ~> gcd_greatest 

520 
gcd_greatest_int ~> gcd_greatest 

521 
coprime_mult_nat ~> coprime_mult 

522 
coprime_mult_int ~> coprime_mult 

523 
lcm_commute_nat ~> lcm.commute 

524 
lcm_commute_int ~> lcm.commute 

525 
int_less_0_conv ~> of_nat_less_0_iff 

526 
gcd_commute_nat ~> gcd.commute 

527 
gcd_commute_int ~> gcd.commute 

528 
Gcd_insert_nat ~> Gcd_insert 

529 
Gcd_insert_int ~> Gcd_insert 

530 
of_int_int_eq ~> of_int_of_nat_eq 

531 
lcm_least_nat ~> lcm_least 

532 
lcm_least_int ~> lcm_least 

533 
lcm_assoc_nat ~> lcm.assoc 

534 
lcm_assoc_int ~> lcm.assoc 

535 
int_le_0_conv ~> of_nat_le_0_iff 

536 
int_eq_0_conv ~> of_nat_eq_0_iff 

537 
Gcd_empty_nat ~> Gcd_empty 

538 
Gcd_empty_int ~> Gcd_empty 

539 
gcd_assoc_nat ~> gcd.assoc 

540 
gcd_assoc_int ~> gcd.assoc 

541 
zero_zle_int ~> of_nat_0_le_iff 

542 
lcm_dvd2_nat ~> dvd_lcm2 

543 
lcm_dvd2_int ~> dvd_lcm2 

544 
lcm_dvd1_nat ~> dvd_lcm1 

545 
lcm_dvd1_int ~> dvd_lcm1 

546 
gcd_zero_nat ~> gcd_eq_0_iff 

547 
gcd_zero_int ~> gcd_eq_0_iff 

548 
gcd_dvd2_nat ~> gcd_dvd2 

549 
gcd_dvd2_int ~> gcd_dvd2 

550 
gcd_dvd1_nat ~> gcd_dvd1 

551 
gcd_dvd1_int ~> gcd_dvd1 

552 
int_numeral ~> of_nat_numeral 

553 
lcm_ac_nat ~> ac_simps 

554 
lcm_ac_int ~> ac_simps 

555 
gcd_ac_nat ~> ac_simps 

556 
gcd_ac_int ~> ac_simps 

557 
abs_int_eq ~> abs_of_nat 

558 
zless_int ~> of_nat_less_iff 

559 
zdiff_int ~> of_nat_diff 

560 
zadd_int ~> of_nat_add 

561 
int_mult ~> of_nat_mult 

562 
int_Suc ~> of_nat_Suc 

563 
inj_int ~> inj_of_nat 

564 
int_1 ~> of_nat_1 

565 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

588 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  589 
realpow_minus_mult ~> power_minus_mult 
590 
realpow_Suc_le_self ~> power_Suc_le_self 

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

591 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  592 
INCOMPATIBILITY. 
593 

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

594 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  595 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
596 

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

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

600 
"unbundle finfun_syntax" to imitate import of 

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

602 

603 
* Session HOLLibrary: theory Multiset_Permutations (executably) defines 

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

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

606 
once. 

607 

608 
* Session HOLLibrary: multiset membership is now expressed using 

609 
set_mset rather than count. 

610 

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

612 
by default. 

613 

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

615 
equations count_eq_zero_iff and not_in_iff. 

616 

617 
 Rules count_inI and in_countE obtain facts of the form 

618 
"count M a = n" from membership. 

619 

620 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 

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

622 

623 
INCOMPATIBILITY. 

624 

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

626 
displaying equations in functional programming style  variables 

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

628 
underscores. 

629 

630 
* Session HOLLibrary: theory Combinator_PER provides combinator to 

631 
build partial equivalence relations from a predicate and an equivalence 

632 
relation. 

633 

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

635 
everywhere fix bijections. 

636 

637 
* Session HOLLibrary: theory Normalized_Fraction allows viewing an 

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

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

640 
denominator is normalized wrt. unit factors). 

641 

642 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

643 

644 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

645 

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

647 
HOLProbability. When importing HOLAnalysis some theorems need 

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

649 

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

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

652 
principle, Residue theorem, Schwarz Lemma. 

653 

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

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

656 

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

658 
libraries: homeomorphisms, continuous function extensions, invariance of 

659 
domain. 

660 

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

662 
changed from ereal to ennreal, INCOMPATIBILITY. 

663 

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

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

666 

667 
* Session HOLProbability: Code generation and QuickCheck for 

668 
Probability Mass Functions. 

669 

670 
* Session HOLProbability: theory Random_Permutations contains some 

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

672 
folding over a list in random order. 

673 

674 
* Session HOLProbability: theory SPMF formalises discrete 

675 
subprobability distributions. 

676 

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

678 
normalised to distinguish which ordering the theorems are about 

679 

680 
mset_less_eqI ~> mset_subset_eqI 

681 
mset_less_insertD ~> mset_subset_insertD 

682 
mset_less_eq_count ~> mset_subset_eq_count 

683 
mset_less_diff_self ~> mset_subset_diff_self 

684 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 

685 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 

686 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 

687 
mset_le_mono_add ~> mset_subset_eq_mono_add 

688 
mset_le_add_left ~> mset_subset_eq_add_left 

689 
mset_le_add_right ~> mset_subset_eq_add_right 

690 
mset_le_single ~> mset_subset_eq_single 

691 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 

692 
diff_le_self ~> diff_subset_eq_self 

693 
mset_leD ~> mset_subset_eqD 

694 
mset_lessD ~> mset_subsetD 

695 
mset_le_insertD ~> mset_subset_eq_insertD 

696 
mset_less_of_empty ~> mset_subset_of_empty 

697 
mset_less_size ~> mset_subset_size 

698 
wf_less_mset_rel ~> wf_subset_mset_rel 

699 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 

700 
mset_remdups_le ~> mset_remdups_subset_eq 

701 
ms_lesseq_impl ~> subset_eq_mset_impl 

702 

703 
Some functions have been renamed: 

704 
ms_lesseq_impl > subset_eq_mset_impl 

705 

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

707 
#\<subseteq># ~> \<le> 

708 
#\<subset># ~> < 

709 
le_multiset ~> less_eq_multiset 

710 
less_multiset ~> le_multiset 

711 
INCOMPATIBILITY. 

712 

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

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

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

716 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

717 
replaced by instantiations. INCOMPATIBILITY. 

718 

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

720 
been renamed: 

721 

722 
le_multiset_def ~> less_eq_multiset_def 

723 
less_multiset_def ~> le_multiset_def 

724 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 

725 
mult_less_not_refl ~> mset_le_not_refl 

726 
mult_less_trans ~> mset_le_trans 

727 
mult_less_not_sym ~> mset_le_not_sym 

728 
mult_less_asym ~> mset_le_asym 

729 
mult_less_irrefl ~> mset_le_irrefl 

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

731 

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

733 
le_multiset_total ~> less_eq_multiset_total 

734 
less_multiset_right_total ~> subset_eq_imp_le_multiset 

735 
le_multiset_empty_left ~> less_eq_multiset_empty_left 

736 
le_multiset_empty_right ~> less_eq_multiset_empty_right 

737 
less_multiset_empty_right ~> le_multiset_empty_left 

738 
less_multiset_empty_left ~> le_multiset_empty_right 

739 
union_less_diff_plus ~> union_le_diff_plus 

740 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 

741 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 

742 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 

743 
INCOMPATIBILITY. 

744 

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

746 
INCOMPATIBILITY. 

747 

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

749 
INCOMPATIBILITY, use the following replacements: 

750 

751 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 

752 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 

753 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 

754 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 

755 
add_eq_self_empty_iff ~> add_cancel_left_right 

756 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 

757 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 

758 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 

759 
empty_inter ~> subset_mset.inf_bot_left 

760 
inter_empty ~> subset_mset.inf_bot_right 

761 
empty_sup ~> subset_mset.sup_bot_left 

762 
sup_empty ~> subset_mset.sup_bot_right 

763 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

764 
subset_eq_empty ~> subset_mset.le_zero_eq 

765 
le_empty ~> subset_mset.le_zero_eq 

766 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

767 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 

768 

769 
* Session HOLLibrary: some typeclass constraints about multisets have 

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

771 
additional typeclasses order_bot, no_top, 

772 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

773 
linordered_cancel_ab_semigroup_add, and 

774 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

775 

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

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

778 
INCOMPATIBILITY. 

779 

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

781 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

782 
bounded_lattice_bot. INCOMPATIBILITY. 

783 

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

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

786 
removed or changed: 

787 

788 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 

789 
fold_mset_insert ~> fold_mset_add_mset 

790 
image_mset_insert ~> image_mset_add_mset 

791 
union_single_eq_diff 

792 
multi_self_add_other_not_self 

793 
diff_single_eq_union 

794 
INCOMPATIBILITY. 

795 

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

797 
to use add_mset instead of single: 

798 

799 
mset_add 

800 
multi_self_add_other_not_self 

801 
diff_single_eq_union 

802 
union_single_eq_diff 

803 
union_single_eq_member 

804 
add_eq_conv_diff 

805 
insert_noteq_member 

806 
add_eq_conv_ex 

807 
multi_member_split 

808 
multiset_add_sub_el_shuffle 

809 
mset_subset_eq_insertD 

810 
mset_subset_insertD 

811 
insert_subset_eq_iff 

812 
insert_union_subset_iff 

813 
multi_psub_of_add_self 

814 
inter_add_left1 

815 
inter_add_left2 

816 
inter_add_right1 

817 
inter_add_right2 

818 
sup_union_left1 

819 
sup_union_left2 

820 
sup_union_right1 

821 
sup_union_right2 

822 
size_eq_Suc_imp_eq_union 

823 
multi_nonempty_split 

824 
mset_insort 

825 
mset_update 

826 
mult1I 

827 
less_add 

828 
mset_zip_take_Cons_drop_twice 

829 
rel_mset_Zero 

830 
msed_map_invL 

831 
msed_map_invR 

832 
msed_rel_invL 

833 
msed_rel_invR 

834 
le_multiset_right_total 

835 
multiset_induct 

836 
multiset_induct2_size 

837 
multiset_induct2 

838 
INCOMPATIBILITY. 

839 

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

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

842 
element: 

843 

844 
image_mset 

845 
mset 

846 
replicate_mset 

847 
mult1 

848 
pred_mset 

849 
rel_mset' 

850 
mset_insort 

851 

852 
INCOMPATIBILITY. 

853 

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

855 
attributes of some multiset theorems have been changed: 

856 

857 
insert_DiffM [] ~> [simp] 

858 
insert_DiffM2 [simp] ~> [] 

859 
diff_add_mset_swap [simp] 

860 
fold_mset_add_mset [simp] 

861 
diff_diff_add [simp] (for multisets only) 

862 
diff_cancel [simp] ~> [] 

863 
count_single [simp] ~> [] 

864 
set_mset_single [simp] ~> [] 

865 
size_multiset_single [simp] ~> [] 

866 
size_single [simp] ~> [] 

867 
image_mset_single [simp] ~> [] 

868 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 

869 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 

870 
fold_mset_single [simp] ~> [] 

871 
subset_eq_empty [simp] ~> [] 

872 
empty_sup [simp] ~> [] 

873 
sup_empty [simp] ~> [] 

874 
inter_empty [simp] ~> [] 

875 
empty_inter [simp] ~> [] 

876 
INCOMPATIBILITY. 

877 

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

881 
INCOMPATIBILITY. 

882 

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

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

885 
natural numbers. INCOMPATIBILITY. 

886 

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

888 
multisets: 

889 

890 
msetsum ~> sum_mset 

891 
msetprod ~> prod_mset 

892 

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

894 
and union of multisets have been changed: 

895 

896 
#\<inter> ~> \<inter># 

897 
#\<union> ~> \<union># 

898 

899 
INCOMPATIBILITY. 

900 

901 
* Session HOLLibrary, theory Multiset: the lemma 

902 
one_step_implies_mult_aux on multisets has been removed, use 

903 
one_step_implies_mult instead. INCOMPATIBILITY. 

904 

905 
* Session HOLLibrary: theory Complete_Partial_Order2 provides reasoning 

906 
support for monotonicity and continuity in chaincomplete partial orders 

907 
and about admissibility conditions for fixpoint inductions. 

908 

909 
* Session HOLLibrary: theory Polynomial contains also derivation of 

910 
polynomials but not gcd/lcm on polynomials over fields. This has been 

911 
moved to a separate theory Library/Polynomial_GCD_euclidean.thy, to pave 

912 
way for a possible future different type class instantiation for 

913 
polynomials over factorial rings. INCOMPATIBILITY. 

914 

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

916 
the following renaming 

917 

918 
prefixeq > prefix 

919 
prefix > strict_prefix 

920 
suffixeq > suffix 

921 
suffix > strict_suffix 

922 

923 
Added theory of longest common prefixes. 

64389  924 

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

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

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

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

930 
"prime_nat_iff". INCOMPATIBILITY. 

931 

932 
* Session Old_Number_Theory has been removed, after porting remaining 

933 
theories. 

934 

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

935 

62498  936 
*** ML *** 
937 

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

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

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

942 
INCOMPATIBILITY. 

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

943 

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

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

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

951 

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

954 

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

956 
with approximative output quality. 

957 

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

959 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 

960 

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

963 
requiring separate files. 

964 

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

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

968 
debugger information requires consirable time and space: main 

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

970 

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

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

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

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

976 
balanced blocks of Local_Theory.open_target versus 

977 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

978 

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

981 
INCOMPATIBILITY. 

982 

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

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

986 
File.full_path). Potential INCOMPATIBILITY. 

987 

63352  988 
* Binding.empty_atts supersedes Thm.empty_binding and 
989 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

990 

62498  991 

62354  992 
*** System *** 
993 

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

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

997 
much less disk space. 

63226  998 

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

1001 
particular: 

1002 

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

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

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

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

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

1007 

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

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

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

1011 

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

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

1013 
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

1014 
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

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

1016 

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

1019 
servers with separate CPU/memory modules. 

1020 

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

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

64274  1023 
unless there is already a default provided via ML_OPTIONS settings. 
1024 

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

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

1026 
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

1027 
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

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

1029 

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

1033 
resulting log files. 

64308  1034 

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

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

1036 
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

1037 
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

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

1039 

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

1042 

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

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

1045 
Isabelle/ML or Isabelle/Scala. 

1046 

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

1048 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 

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

1050 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 

1051 
discontinued. Potential INCOMPATIBILITY. 

1052 

1053 
* The Isabelle system environment always ensures that the main 

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

1055 
"isabelle_scala_script". 

1056 

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

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

1059 
Isabelle_Tool.Body. 

1060 

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

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

1063 
produce robust shell scripts under program control, without worrying 

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

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

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

1067 
been discontinued. 

1068 

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

1071 
but without the Isabelle settings environment. 

1072 

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

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

1076 
that Path specifications need to be resolved remotely via 

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

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

1079 

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

1081 
regular hg commandline interface. The repositroy clone and working 

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

1083 
connection). 

64265  1084 

62354  1085 

1086 

62031  1087 
New in Isabelle2016 (February 2016) 
62016  1088 
 
60138  1089 

61337  1090 
*** General *** 
1091 

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

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

1093 
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

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

1095 
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

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

1097 

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

1100 

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

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

1104 
has been removed (see below). 

1105 

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

62017  1108 

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

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

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

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

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

1113 

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

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

1115 
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

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

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

1118 

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

1121 
to update old sources. 

1122 

61337  1123 
* Toplevel theorem statements have been simplified as follows: 
1124 

1125 
theorems ~> lemmas 

1126 
schematic_lemma ~> schematic_goal 

1127 
schematic_theorem ~> schematic_goal 

1128 
schematic_corollary ~> schematic_goal 

1129 

1130 
Commandline tool "isabelle update_theorems" updates theory sources 

1131 
accordingly. 

1132 

61338  1133 
* Toplevel theorem statement 'proposition' is another alias for 
1134 
'theorem'. 

1135 

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

1138 
deferred definitions require a surrounding 'overloading' block. 

1139 

61337  1140 

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

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

1142 

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

1146 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1150 
any effect on the running ML program. 

60984  1151 

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

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

1155 
update. 

61729  1156 

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

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

1159 
enable option "editor_output_state". 

61215  1160 

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

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

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

1165 
visibility. 

1166 

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

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

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

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

1171 
panel. 

1172 

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

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

1174 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1175 

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

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

1178 
implicit: a popup will show up unconditionally. 

1179 

1180 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1183 

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

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

1185 
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

1186 
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

1187 
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

1188 

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

1191 
the editor. 

1192 

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

1194 
instead of former C+e LEFT. 

1195 

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

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

1198 
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

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

1200 

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

1203 
singleinstance applications seen on common GUI desktops. 

1204 

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

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

1206 
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

1207 
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

1208 

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

1211 

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

1214 

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

1215 

61405  1216 
*** Document preparation *** 
1217 

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

1220 

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

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

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

1224 

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

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

1227 
follows: 

1228 

1229 
\<^item> itemize 

1230 
\<^enum> enumerate 

1231 
\<^descr> description 

1232 

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

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

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

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

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

1239 

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

1242 
standard LaTeX macros of the same names. 

1243 

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

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

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

1248 
cartouche tokens seen in theory sources. 

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

1249 

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

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

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

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

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

1255 

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

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

1259 

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

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

1262 

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

1264 

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

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

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

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

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

1270 
documentation, with a hyperlink in the Prover IDE. 

1271 

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

1273 
entities of the Isar language. 

1274 

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

61488  1277 
print mode "HTML" loses its special meaning. 
61471  1278 

61405  1279 

60406  1280 
*** Isar *** 
1281 

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

1284 
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

1285 
example: 
60414  1286 

1287 
have result: "C x y" 

1288 
if "A x" and "B y" 

1289 
for x :: 'a and y :: 'a 

1290 
<proof> 

1291 

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

60414  1294 
corresponds to a raw proof block like this: 
1295 

1296 
{ 

1297 
fix x :: 'a and y :: 'a 

60449  1298 
assume that: "A x" "B y" 
60414  1299 
have "C x y" <proof> 
1300 
} 

1301 
note result = this 

60406  1302 

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

1303 
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

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

1305 

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

61658  1308 

1309 
assume result: "C x y" 

1310 
if "A x" and "B y" 

1311 
for x :: 'a and y :: 'a 

1312 

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

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

1315 

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

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

1318 
example: 

1319 

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

1321 

1322 
is equivalent to: 

1323 

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

1325 

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

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

60595  1330 

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

1332 

1333 
or: 

1334 

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

1336 

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

1338 

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

1340 

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

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

1344 
of the local context elements yet. 

1345 

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

1348 

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

1350 
then have something 

1351 
proof cases 

1352 
case a 

1353 
then show ?thesis <proof> 

1354 
next 

1355 
case b 

1356 
then show ?thesis <proof> 

1357 
next 

1358 
case c 

1359 
then show ?thesis <proof> 

1360 
qed 

1361 

60565  1362 
* Command 'case' allows fact name and attribute specification like this: 
1363 

1364 
case a: (c xs) 

1365 
case a [attributes]: (c xs) 

1366 

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

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

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

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

1371 
and always put attributes in front. 

1372 

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

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

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

1375 
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

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

1377 

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

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

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

1382 

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

1384 
supply [simp] = a 

1385 
proof 

1386 
show A by simp 

1387 
next 

1388 
show A by simp 

1389 
qed 

1390 

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

1392 
proof body as well, abstracted over relevant parameters. 

1393 

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

1395 
parameter scope for of each clause. 

1396 

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

1398 
statements: result is abstracted over unknowns. 

1399 

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

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

1403 
manual. 

1404 

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

1407 

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

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

1409 
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

1410 
example: 
60617  1411 

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

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

1414 
proof goal_cases 
60622  1415 
case (1 x) 
1416 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

1417 
next 

1418 
case (2 y z) 

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

1420 
qed 

1421 

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

1423 
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

1424 
proof goal_cases 
60617  1425 
case prems: 1 
1426 
then show ?case using prems sorry 

1427 
next 

1428 
case prems: 2 

1429 
then show ?case using prems sorry 

1430 
qed 

60578  1431 

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

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

60581  1436 

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