author  traytel 
Mon, 24 Oct 2016 16:53:32 +0200  
changeset 64379  71f42dcaa1df 
parent 64363  90ceace1e814 
child 64389  6273d4c8325b 
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 

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

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

15 

16 
bundle foo 

17 
begin 

18 
declare a [simp] 

19 
declare b [intro] 

20 
end 

63272  21 

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

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

25 

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

28 
discontinued. 

29 

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

31 
delimited uniformly via cartouches. This works better than oldfashioned 

32 
quotes when sublanguages are nested. 

33 

34 
* Mixfix annotations support general block properties, with syntax 

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

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

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

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

63650  39 

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

42 

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

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

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

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

48 
examples. 

49 

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

51 
instances) are generated into companion object of corresponding type 

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

53 

54 
* Splitter in 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. 

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

62 

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

63 
* Solve direct: option 'solve_direct_strict_warnings' gives explicit 
048b7dbfdfa3
option to report results of solve_direct as explicit warnings
haftmann
parents:
63995
diff
changeset

64 
warnings for lemma statements with trivial proofs. 
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 

63977  69 
* Highlighting of entity def/ref positions wrt. cursor. 
70 

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

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

73 
systematic renaming. 

74 

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

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

77 
theorem statement. 

78 

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

80 
situations where old ASCII notation may be updated. 

81 

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

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

85 
inaccessible via keyboard completion). 

86 

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

89 

90 
src/Pure/ROOT0.ML 

91 
src/Pure/ROOT.ML 

92 
src/Pure/Pure.thy 

93 
src/Pure/ML_Bootstrap.thy 

94 

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

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

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

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

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

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

63307  101 
dependencies of the above files are only observed for batch build. 
62904  102 

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

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

63461  106 

63608  107 
* Sidekick parser "isabellecontext" shows nesting of context blocks 
108 
according to 'begin' and 'end' structure. 

109 

63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

110 
* Syntactic indentation according to Isabelle outer syntax. Action 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

111 
"indentlines" (shortcut C+i) indents the current line according to 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

112 
command keywords and some command substructure. Action 
63455
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset

113 
"isabelle.newline" (shortcut ENTER) indents the old and the new line 
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset

114 
according to command keywords only; see also option 
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset

115 
"jedit_indent_newline". 
63452  116 

63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

117 
* Semantic indentation for unstructured proof scripts ('apply' etc.) via 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

118 
number of subgoals. This requires information of ongoing document 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

119 
processing and may thus lag behind, when the user is editing too 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

120 
quickly; see also option "jedit_script_indent" and 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

121 
"jedit_script_indent_limit". 
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset

122 

63977  123 
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' 
124 
are treated as delimiters for fold structure; 'begin' and 'end' 

125 
structure of theory specifications is treated as well. 

63236  126 

63751  127 
* Action "isabelle.keymapmerge" asks the user to resolve pending 
128 
Isabelle keymap changes that are in conflict with the current jEdit 

129 
keymap; nonconflicting changes are always applied implicitly. This 

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

131 
increases chances that users see new keyboard shortcuts when reusing 

132 
old keymaps. 

133 

63513
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset

134 
* Command 'proof' provides information about proof outline with cases, 
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset

135 
e.g. for proof methods "cases", "induct", "goal_cases". 
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset

136 

63528
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset

137 
* Completion templates for commands involving "begin ... end" blocks, 
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset

138 
e.g. 'context', 'notepad'. 
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset

139 

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

143 
new 'abbrevs' section. 

144 

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

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

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

63579  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 

64363
90ceace1e814
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
eberlm <eberlm@in.tum.de>
parents:
64342
diff
changeset

252 
* Ported remaining theories of Old_Number_Theory and removed Old_Number_Theory. 
90ceace1e814
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
eberlm <eberlm@in.tum.de>
parents:
64342
diff
changeset

253 

64240  254 
* Sligthly more standardized theorem names: 
255 
sgn_times ~> sgn_mult 

256 
sgn_mult' ~> Real_Vector_Spaces.sgn_mult 

257 
divide_zero_left ~> div_0 

258 
zero_mod_left ~> mod_0 

259 
divide_zero ~> div_by_0 

260 
divide_1 ~> div_by_1 

261 
nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left 

262 
div_mult_self1_is_id ~> nonzero_mult_div_cancel_left 

263 
nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right 

264 
div_mult_self2_is_id ~> nonzero_mult_div_cancel_right 

265 
is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left 

266 
is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right 

64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

267 
mod_div_equality ~> div_mult_mod_eq 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

268 
mod_div_equality2 ~> mult_div_mod_eq 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

269 
mod_div_equality3 ~> mod_div_mult_eq 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

270 
mod_div_equality4 ~> mod_mult_div_eq 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

271 
minus_div_eq_mod ~> minus_div_mult_eq_mod 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

272 
minus_div_eq_mod2 ~> minus_mult_div_eq_mod 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

273 
minus_mod_eq_div ~> minus_mod_eq_div_mult 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
64240
diff
changeset

274 
minus_mod_eq_div2 ~> minus_mod_eq_mult_div 
64243  275 
div_mod_equality' ~> minus_mod_eq_div_mult [symmetric] 
276 
mod_div_equality' ~> minus_div_mult_eq_mod [symmetric] 

64246  277 
zmod_zdiv_equality ~> mult_div_mod_eq [symmetric] 
278 
zmod_zdiv_equality' ~> minus_div_mult_eq_mod [symmetric] 

279 
Divides.mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

280 
mult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

281 
zmult_div_cancel ~> minus_mod_eq_mult_div [symmetric] 

64244  282 
div_1 ~> div_by_Suc_0 
283 
mod_1 ~> mod_by_Suc_0 

64240  284 
INCOMPATIBILITY. 
285 

64323  286 
* Renamed constants "setsum" ~> "sum" and "setprod" ~> "prod". 
287 
Corresponding renaming of theorems. 

288 

64290  289 
* New type class "idom_abs_sgn" specifies algebraic properties 
290 
of sign and absolute value functions. Type class "sgn_if" has 

291 
disappeared. Slight INCOMPATIBILITY. 

64322  292 

64113  293 
* Dedicated syntax LENGTH('a) for length of types. 
294 

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

297 
propositional logic, goals based on a combination of quantifierfree 

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

299 
quantifierfree propositional logic with linear real arithmetic 

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

301 

302 
* Metis: The problem encoding has changed very slightly. This might 

63785  303 
break existing proofs. INCOMPATIBILITY. 
304 

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

306 
 The MaSh relevance filter is now faster than before. 
63116  307 
 Produce syntactically correct Vampire 4.0 problem files. 
308 

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

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

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

62335  325 
 Renamed lemmas: 
326 
rel_prod_apply ~> rel_prod_inject 

327 
pred_prod_apply ~> pred_prod_inject 

328 
INCOMPATIBILITY. 

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

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

332 
INCOMPATIBILITY. 

62327  333 

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

336 
which exposed details of the internal fixpoint construction and was 

337 
hard to use. INCOMPATIBILITY. 

338 

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

340 

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

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

343 

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

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

346 
eliminated altogether. 

347 

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

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

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

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

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

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

354 
INCOMPATIBILITY in rare situations. 

355 

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

357 
INCOMPATIBILITY. 

358 

359 
* Characters (type char) are modelled as finite algebraic type 

360 
corresponding to {0..255}. 

361 

362 
 Logical representation: 

363 
* 0 is instantiated to the ASCII zero character. 

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

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

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

367 
are noncanonical. 

368 
 Printing and parsing: 

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

370 
(as before). 

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

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

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

374 
is parsable for every numeral expression n. 

375 
* Noncanonical characters have no special syntax and are 

376 
printed as their logical representation. 

377 
 Explicit conversions from and to the natural numbers are 

378 
provided as char_of_nat, nat_of_char (as before). 

379 
 The auxiliary nibble type has been discontinued. 

380 

381 
INCOMPATIBILITY. 

382 

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

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

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

386 
infix "mod" syntax. INCOMPATIBILITY. 

387 

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

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

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

392 
easily recovered by composition with eq_refl. Minor INCOMPATIBILITY. 

393 

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

396 

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

398 
which renders those abstract effectively. 

399 

400 
* Command 'export_code' checks given constants for abstraction 

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

402 
interface for the generated code. 

403 

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

405 
spelt out explicitly. 

406 

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

408 
explicitly provided auxiliary definitions for required type class 

409 
dictionaries rather than halfworking magic. INCOMPATIBILITY, see 

410 
the tutorial on code generation for details. 

411 

412 
* Theory Set_Interval.thy: substantial new theorems on indexed sums 

413 
and products. 

414 

415 
* Theory List.thy: ranaming of listsum ~> sum_list, listprod ~> 

416 
prod_list, INCOMPATIBILITY. 

417 

418 
* Locale bijection establishes convenient default simp rules such as 

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

420 

421 
* Abstract locales semigroup, abel_semigroup, semilattice, 

422 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

423 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

424 
semilattice_neutr_set, semilattice_order_set, 

425 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

426 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

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

428 
INCOMPATIBILITY. 

429 

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

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

432 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

433 

63807  434 
* Some old / obsolete theorems have been renamed / removed, potential 
435 
INCOMPATIBILITY. 

436 

437 
nat_less_cases  removed, use linorder_cases instead 

438 
inv_image_comp  removed, use image_inv_f_f instead 

439 
image_surj_f_inv_f ~> image_f_inv_f 

63113  440 

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

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

442 
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

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

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

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

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

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

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

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

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

451 

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

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

453 
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

454 
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

455 
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

456 
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

457 
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

458 
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

459 
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

460 
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

461 
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

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

463 

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

62396  466 

63977  467 
* Added class topological_monoid. 
468 

469 
* HOLLibrary: theory FinFun bundles "finfun_syntax" and 

470 
"no_finfun_syntax" allow to control optional syntax in local contexts; 

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

472 
"unbundle finfun_syntax" to imitate import of 

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

474 

64074
7dccbbd8d71d
Set_Permutations > Multiset_Permutations in NEWS
eberlm <eberlm@in.tum.de>
parents:
64073
diff
changeset

475 
* HOLLibrary: theory Multiset_Permutations (executably) defines the set of 
64122  476 
permutations of a given set or multiset, i.e. the set of all lists that 
64074
7dccbbd8d71d
Set_Permutations > Multiset_Permutations in NEWS
eberlm <eberlm@in.tum.de>
parents:
64073
diff
changeset

477 
contain every element of the carrier (multi)set exactly once. 
63977  478 

479 
* HOLLibrary: multiset membership is now expressed using set_mset 

480 
rather than count. 

62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

481 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

482 
 Expressions "count M a > 0" and similar simplify to membership 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

483 
by default. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

484 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

485 
 Converting between "count M a = 0" and nonmembership happens using 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

486 
equations count_eq_zero_iff and not_in_iff. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

487 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

488 
 Rules count_inI and in_countE obtain facts of the form 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

489 
"count M a = n" from membership. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

490 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

491 
 Rules count_in_diffI and in_diff_countE obtain facts of the form 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

492 
"count M a = n + count N a" from membership on difference sets. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

493 

9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

494 
INCOMPATIBILITY. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

495 

63977  496 
* HOLLibrary: theory LaTeXsugar uses newstyle "dummy_pats" for 
497 
displaying equations in functional programming style  variables 

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

499 
underscores. 

500 

501 
* HOLLibrary: theory Combinator_PER provides combinator to build 

502 
partial equivalence relations from a predicate and an equivalence 

503 
relation. 

504 

505 
* HOLLibrary: theory Perm provides basic facts about almost everywhere 

506 
fix bijections. 

507 

508 
* HOLLibrary: theory Normalized_Fraction allows viewing an element of a 

509 
field of fractions as a normalized fraction (i.e. a pair of numerator 

510 
and denominator such that the two are coprime and the denominator is 

511 
normalized wrt. unit factors). 

512 

513 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

514 

515 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

516 

517 
* HOLAnalysis: measure theory has been moved here from HOLProbability. 

518 
When importing HOLAnalysis some theorems need additional name spaces 

519 
prefixes due to name clashes. INCOMPATIBILITY. 

520 

521 
* HOLAnalysis: more complex analysis including Cauchy's inequality, 

522 
Liouville theorem, open mapping theorem, maximum modulus principle, 

523 
Residue theorem, Schwarz Lemma. 

524 

525 
* HOLAnalysis: Theory of polyhedra: faces, extreme points, polytopes, 

526 
and the Kreinâ€“Milman Minkowski theorem. 

527 

528 
* HOLAnalysis: Numerous results ported from the HOL Light libraries: 

64122  529 
homeomorphisms, continuous function extensions, invariance of domain. 
63977  530 

531 
* HOLProbability: the type of emeasure and nn_integral was changed from 

532 
ereal to ennreal, INCOMPATIBILITY. 

533 

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

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

536 

537 
* HOLProbability: Code generation and QuickCheck for Probability Mass 

538 
Functions. 

539 

540 
* HOLProbability: theory Random_Permutations contains some theory about 

541 
choosing a permutation of a set uniformly at random and folding over a 

542 
list in random order. 

543 

544 
* HOLProbability: theory SPMF formalises discrete subprobability 

545 
distributions. 

546 

547 
* HOLNumber_Theory: algebraic foundation for primes: Generalisation of 

548 
predicate "prime" and introduction of predicates "prime_elem", 

549 
"irreducible", a "prime_factorization" function, and the 

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

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

552 
"prime_nat_iff". INCOMPATIBILITY. 

553 

554 
* HOLLibrary: the names of multiset theorems have been normalised to 

555 
distinguish which ordering the theorems are about 

556 

63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

557 
mset_less_eqI ~> mset_subset_eqI 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

558 
mset_less_insertD ~> mset_subset_insertD 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

559 
mset_less_eq_count ~> mset_subset_eq_count 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

560 
mset_less_diff_self ~> mset_subset_diff_self 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

561 
mset_le_exists_conv ~> mset_subset_eq_exists_conv 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

562 
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

563 
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

564 
mset_le_mono_add ~> mset_subset_eq_mono_add 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

565 
mset_le_add_left ~> mset_subset_eq_add_left 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

566 
mset_le_add_right ~> mset_subset_eq_add_right 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

567 
mset_le_single ~> mset_subset_eq_single 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

568 
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

569 
diff_le_self ~> diff_subset_eq_self 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

570 
mset_leD ~> mset_subset_eqD 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

571 
mset_lessD ~> mset_subsetD 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

572 
mset_le_insertD ~> mset_subset_eq_insertD 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

573 
mset_less_of_empty ~> mset_subset_of_empty 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

574 
mset_less_size ~> mset_subset_size 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

575 
wf_less_mset_rel ~> wf_subset_mset_rel 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

576 
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

577 
mset_remdups_le ~> mset_remdups_subset_eq 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

578 
ms_lesseq_impl ~> subset_eq_mset_impl 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

579 

63977  580 
Some functions have been renamed: 
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

581 
ms_lesseq_impl > subset_eq_mset_impl 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

582 

63977  583 
* HOLLibrary: multisets are now ordered with the multiset ordering 
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

584 
#\<subseteq># ~> \<le> 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

585 
#\<subset># ~> < 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

586 
le_multiset ~> less_eq_multiset 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

587 
less_multiset ~> le_multiset 
63407
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

588 
INCOMPATIBILITY. 
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

589 

63977  590 
* HOLLibrary: the prefix multiset_order has been discontinued: the 
591 
theorems can be directly accessed. As a consequence, the lemmas 

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

593 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

594 
replaced by instantiations. INCOMPATIBILITY. 

595 

596 
* HOLLibrary: some theorems about the multiset ordering have been 

597 
renamed: 

598 

63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

599 
le_multiset_def ~> less_eq_multiset_def 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

600 
less_multiset_def ~> le_multiset_def 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

601 
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

602 
mult_less_not_refl ~> mset_le_not_refl 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

603 
mult_less_trans ~> mset_le_trans 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

604 
mult_less_not_sym ~> mset_le_not_sym 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

605 
mult_less_asym ~> mset_le_asym 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

606 
mult_less_irrefl ~> mset_le_irrefl 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

607 
union_less_mono2{,1,2} ~> union_le_mono2{,1,2} 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

608 

a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

609 
le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

610 
le_multiset_total ~> less_eq_multiset_total 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

611 
less_multiset_right_total ~> subset_eq_imp_le_multiset 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

612 
le_multiset_empty_left ~> less_eq_multiset_empty_left 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

613 
le_multiset_empty_right ~> less_eq_multiset_empty_right 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

614 
less_multiset_empty_right ~> le_multiset_empty_left 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

615 
less_multiset_empty_left ~> le_multiset_empty_right 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

616 
union_less_diff_plus ~> union_le_diff_plus 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

617 
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

618 
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

619 
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty 
63407
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

620 
INCOMPATIBILITY. 
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

621 

63977  622 
* HOLLibrary: the lemma mset_map has now the attribute [simp]. 
623 
INCOMPATIBILITY. 

624 

625 
* HOLLibrary: some theorems about multisets have been removed. 

626 
INCOMPATIBILITY, use the following replacements: 

627 

63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63524
diff
changeset

628 
le_multiset_plus_plus_left_iff ~> add_less_cancel_right 
64097
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

629 
less_multiset_plus_plus_left_iff ~> add_less_cancel_right 
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63524
diff
changeset

630 
le_multiset_plus_plus_right_iff ~> add_less_cancel_left 
64097
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

631 
less_multiset_plus_plus_right_iff ~> add_less_cancel_left 
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63524
diff
changeset

632 
add_eq_self_empty_iff ~> add_cancel_left_right 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

633 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 
64097
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

634 
mset_less_add_bothsides ~> subset_mset.add_less_cancel_right 
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

635 
mset_le_add_bothsides ~> subset_mset.add_less_cancel_right 
64076  636 
empty_inter ~> subset_mset.inf_bot_left 
637 
inter_empty ~> subset_mset.inf_bot_right 

638 
empty_sup ~> subset_mset.sup_bot_left 

639 
sup_empty ~> subset_mset.sup_bot_right 

640 
bdd_below_multiset ~> subset_mset.bdd_above_bot 

641 
subset_eq_empty ~> subset_mset.le_zero_eq 

64097
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

642 
le_empty ~> subset_mset.le_zero_eq 
64076  643 
mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 
64097
331fbf2a0d2d
clarifying NEWS file
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
64076
diff
changeset

644 
mset_less_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero 
63977  645 

646 
* HOLLibrary: some typeclass constraints about multisets have been 

647 
reduced from ordered or linordered to preorder. Multisets have the 

648 
additional typeclasses order_bot, no_top, 

649 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

650 
linordered_cancel_ab_semigroup_add, and 

651 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

652 

653 
* HOLLibrary: there are some new simplification rules about multisets, 

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

655 
INCOMPATIBILITY. 

656 

657 
* HOLLibrary: the subset ordering on multisets has now the 

658 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

659 
bounded_lattice_bot. INCOMPATIBILITY. 

660 

661 
* HOLLibrary/Multiset: single has been removed in favor of add_mset 

662 
that roughly corresponds to Set.insert. Some theorems have removed or 

663 
changed: 

664 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

665 
single_not_empty ~> add_mset_not_empty or empty_not_add_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

666 
fold_mset_insert ~> fold_mset_add_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

667 
image_mset_insert ~> image_mset_add_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

668 
union_single_eq_diff 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

669 
multi_self_add_other_not_self 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

670 
diff_single_eq_union 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

671 
INCOMPATIBILITY. 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

672 

63977  673 
* HOLLibrary/Multiset: some theorems have been changed to use add_mset 
674 
instead of single: 

675 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

676 
mset_add 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

677 
multi_self_add_other_not_self 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

678 
diff_single_eq_union 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

679 
union_single_eq_diff 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

680 
union_single_eq_member 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

681 
add_eq_conv_diff 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

682 
insert_noteq_member 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

683 
add_eq_conv_ex 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

684 
multi_member_split 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

685 
multiset_add_sub_el_shuffle 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

686 
mset_subset_eq_insertD 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

687 
mset_subset_insertD 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

688 
insert_subset_eq_iff 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

689 
insert_union_subset_iff 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

690 
multi_psub_of_add_self 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

691 
inter_add_left1 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

692 
inter_add_left2 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

693 
inter_add_right1 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

694 
inter_add_right2 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

695 
sup_union_left1 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

696 
sup_union_left2 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

697 
sup_union_right1 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

698 
sup_union_right2 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

699 
size_eq_Suc_imp_eq_union 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

700 
multi_nonempty_split 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

701 
mset_insort 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

702 
mset_update 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

703 
mult1I 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

704 
less_add 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

705 
mset_zip_take_Cons_drop_twice 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

706 
rel_mset_Zero 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

707 
msed_map_invL 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

708 
msed_map_invR 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

709 
msed_rel_invL 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

710 
msed_rel_invR 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

711 
le_multiset_right_total 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

712 
multiset_induct 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

713 
multiset_induct2_size 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

714 
multiset_induct2 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

715 
INCOMPATIBILITY. 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

716 

63977  717 
* HOLLibrary/Multiset. The definitions of some constants have changed 
718 
to use add_mset instead of adding a single element: 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

719 
image_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

720 
mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

721 
replicate_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

722 
mult1 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

723 
pred_mset 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

724 
rel_mset' 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

725 
mset_insort 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

726 
INCOMPATIBILITY. 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

727 

63977  728 
* HOLLibrary/Multiset. Due to the above changes, the attributes of some 
729 
multiset theorems have been changed: 

63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

730 
insert_DiffM [] ~> [simp] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

731 
insert_DiffM2 [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

732 
diff_add_mset_swap [simp] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

733 
fold_mset_add_mset [simp] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

734 
diff_diff_add [simp] (for multisets only) 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

735 
diff_cancel [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

736 
count_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

737 
set_mset_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

738 
size_multiset_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

739 
size_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

740 
image_mset_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

741 
mset_subset_eq_mono_add_right_cancel [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

742 
mset_subset_eq_mono_add_left_cancel [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

743 
fold_mset_single [simp] ~> [] 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

744 
subset_eq_empty [simp] ~> [] 
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

745 
empty_sup [simp] ~> [] 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

746 
sup_empty [simp] ~> [] 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

747 
inter_empty [simp] ~> [] 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

748 
empty_inter [simp] ~> [] 
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

749 
INCOMPATIBILITY. 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

750 

63977  751 
* HOLLibrary/Multiset. The order of the variables in the second cases 
752 
of multiset_induct, multiset_induct2_size, multiset_induct2 has been 

753 
changed (e.g. Add A a ~> Add a A). INCOMPATIBILITY. 

754 

755 
* HOLLibrary/Multiset. There is now a simplification procedure on 

756 
multisets. It mimics the behavior of the procedure on natural numbers. 

757 
INCOMPATIBILITY. 

758 

759 
* HOLLibrary/Multiset. Renamed sums and products of multisets: 

63830  760 
msetsum ~> sum_mset 
761 
msetprod ~> prod_mset 

762 

63977  763 
* HOLLibrary/Multiset. The notation for intersection and union of 
764 
multisets have been changed: 

63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63918
diff
changeset

765 
#\<inter> ~> \<inter># 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63918
diff
changeset

766 
#\<union> ~> \<union># 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63918
diff
changeset

767 
INCOMPATIBILITY. 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63918
diff
changeset

768 

63977  769 
* HOLLibrary/Multiset. The lemma one_step_implies_mult_aux on multisets 
770 
has been removed, use one_step_implies_mult instead. INCOMPATIBILITY. 

63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

771 

63918
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63917
diff
changeset

772 
* The following theorems have been renamed: 
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63917
diff
changeset

773 
setsum_left_distrib ~> setsum_distrib_right 
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63917
diff
changeset

774 
setsum_right_distrib ~> setsum_distrib_left 
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63917
diff
changeset

775 
INCOMPATIBILITY. 
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63917
diff
changeset

776 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset

777 
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset

778 
INCOMPATIBILITY. 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset

779 

62358  780 
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional 
781 
comprehensionlike syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". 

782 

62345  783 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 
784 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset

785 
* The type class ordered_comm_monoid_add is now called 
63977  786 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 
787 
is introduced as the combination of ordered_ab_semigroup_add + 

788 
comm_monoid_add. INCOMPATIBILITY. 

789 

790 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

791 
dioid. 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset

792 

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

793 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 
63977  794 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 
795 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

796 
be required. INCOMPATIBILITY. 

797 

798 
* HOLLibrary: theory Complete_Partial_Order2 provides reasoning support 

799 
for monotonicity and continuity in chaincomplete partial orders and 

800 
about admissibility conditions for fixpoint inductions. 

801 

802 
* HOLLibrary: theory Polynomial contains also derivation of polynomials 

803 
but not gcd/lcm on polynomials over fields. This has been moved to a 

804 
separate theory Library/Polynomial_GCD_euclidean.thy, to pave way for a 

805 
possible future different type class instantiation for polynomials over 

806 
factorial rings. INCOMPATIBILITY. 

807 

808 
* HOLLibrary: theory Sublist.thy provides function "prefixes" with the 

809 
following renaming 

810 

63173  811 
prefixeq > prefix 
812 
prefix > strict_prefix 

813 
suffixeq > suffix 

814 
suffix > strict_suffix 

63977  815 

816 
Added theory of longest common prefixes. 

63117  817 

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

820 
lcm_left_commute_nat ~> lcm.left_commute 

821 
lcm_left_commute_int ~> lcm.left_commute 

822 
gcd_left_commute_nat ~> gcd.left_commute 

823 
gcd_left_commute_int ~> gcd.left_commute 

824 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

825 
gcd_greatest_iff_int ~> gcd_greatest_iff 

826 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

827 
coprime_dvd_mult_int ~> coprime_dvd_mult 

828 
zpower_numeral_even ~> power_numeral_even 

829 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

830 
gcd_mult_cancel_int ~> gcd_mult_cancel 

831 
div_gcd_coprime_nat ~> div_gcd_coprime 

832 
div_gcd_coprime_int ~> div_gcd_coprime 

833 
zpower_numeral_odd ~> power_numeral_odd 

834 
zero_less_int_conv ~> of_nat_0_less_iff 

835 
gcd_greatest_nat ~> gcd_greatest 

836 
gcd_greatest_int ~> gcd_greatest 

837 
coprime_mult_nat ~> coprime_mult 

838 
coprime_mult_int ~> coprime_mult 

839 
lcm_commute_nat ~> lcm.commute 

840 
lcm_commute_int ~> lcm.commute 

841 
int_less_0_conv ~> of_nat_less_0_iff 

842 
gcd_commute_nat ~> gcd.commute 

843 
gcd_commute_int ~> gcd.commute 

844 
Gcd_insert_nat ~> Gcd_insert 

845 
Gcd_insert_int ~> Gcd_insert 

846 
of_int_int_eq ~> of_int_of_nat_eq 

847 
lcm_least_nat ~> lcm_least 

848 
lcm_least_int ~> lcm_least 

849 
lcm_assoc_nat ~> lcm.assoc 

850 
lcm_assoc_int ~> lcm.assoc 

851 
int_le_0_conv ~> of_nat_le_0_iff 

852 
int_eq_0_conv ~> of_nat_eq_0_iff 

853 
Gcd_empty_nat ~> Gcd_empty 

854 
Gcd_empty_int ~> Gcd_empty 

855 
gcd_assoc_nat ~> gcd.assoc 

856 
gcd_assoc_int ~> gcd.assoc 

857 
zero_zle_int ~> of_nat_0_le_iff 

858 
lcm_dvd2_nat ~> dvd_lcm2 

859 
lcm_dvd2_int ~> dvd_lcm2 

860 
lcm_dvd1_nat ~> dvd_lcm1 

861 
lcm_dvd1_int ~> dvd_lcm1 

862 
gcd_zero_nat ~> gcd_eq_0_iff 

863 
gcd_zero_int ~> gcd_eq_0_iff 

864 
gcd_dvd2_nat ~> gcd_dvd2 

865 
gcd_dvd2_int ~> gcd_dvd2 

866 
gcd_dvd1_nat ~> gcd_dvd1 

867 
gcd_dvd1_int ~> gcd_dvd1 

868 
int_numeral ~> of_nat_numeral 

869 
lcm_ac_nat ~> ac_simps 

870 
lcm_ac_int ~> ac_simps 

871 
gcd_ac_nat ~> ac_simps 

872 
gcd_ac_int ~> ac_simps 

873 
abs_int_eq ~> abs_of_nat 

874 
zless_int ~> of_nat_less_iff 

875 
zdiff_int ~> of_nat_diff 

876 
zadd_int ~> of_nat_add 

877 
int_mult ~> of_nat_mult 

878 
int_Suc ~> of_nat_Suc 

879 
inj_int ~> inj_of_nat 

880 
int_1 ~> of_nat_1 

881 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

904 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  905 
realpow_minus_mult ~> power_minus_mult 
906 
realpow_Suc_le_self ~> power_Suc_le_self 

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

907 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  908 
INCOMPATIBILITY. 
909 

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

910 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  911 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
912 

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

913 

62498  914 
*** ML *** 
915 

63669  916 
* ML antiquotation @{path} is superseded by @{file}, which ensures that 
917 
the argument is a plain file. Minor INCOMPATIBILITY. 

918 

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

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

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

923 
INCOMPATIBILITY. 

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

924 

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

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

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

932 

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

935 
requiring separate files. 

936 

62851  937 
* Lowlevel ML system structures (like PolyML and RunCall) are no longer 
62886
72c475e03e22
simplified bootstrap: critical structures remain accessible in ML_Root context;
wenzelm
parents:
62875
diff
changeset

938 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 
62851  939 

62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset

940 
* Antiquotation @{make_string} is available during Pure bootstrap  
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset

941 
with approximative output quality. 
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset

942 

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

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

946 
debugger information requires consirable time and space: main 

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

948 

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

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

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

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

954 
balanced blocks of Local_Theory.open_target versus 

955 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

956 

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

959 
INCOMPATIBILITY. 

960 

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

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

964 
File.full_path). Potential INCOMPATIBILITY. 

965 

63352  966 
* Binding.empty_atts supersedes Thm.empty_binding and 
967 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

968 

62498  969 

62354  970 
*** System *** 
971 

64280  972 
* Isabelle/Scala: the SSH module supports ssh and sftp connections, for 
973 
remote commandexecution and filesystem access. This resembles 

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

975 
that Path specifications need to be resolved remotely via 

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

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

978 

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

980 
regular hg commandline interface. The repositroy clone and working 

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

982 
connection). 

983 

62840
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

984 
* Many Isabelle tools that require a Java runtime system refer to the 
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

985 
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, 
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

986 
depending on the underlying platform. The settings for "isabelle build" 
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

987 
ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been 
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

988 
discontinued. Potential INCOMPATIBILITY. 
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset

989 

62591  990 
* The Isabelle system environment always ensures that the main 
991 
executables are found within the shell search $PATH: "isabelle" and 

992 
"isabelle_scala_script". 

993 

63226  994 
* Isabelle tools may consist of .scala files: the Scala compiler is 
995 
invoked on the spot. The source needs to define some object that extends 

996 
Isabelle_Tool.Body. 

997 

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

1000 
particular: 

1001 

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

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

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

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

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

1006 

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

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

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

1010 

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

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

1012 
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

1013 
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

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

1015 

64274  1016 
* The system option "threads" (for the size of the Isabelle/ML thread 
1017 
farm) is also passed to the underlying ML runtime system as gcthreads, 

1018 
unless there is already a default provided via ML_OPTIONS settings. 

1019 

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

1020 
* Commandline tool "isabelle console" provides option r to help to 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1021 
bootstrapping Isabelle/Pure interactively. 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1022 

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

1023 
* Commandline tool "isabelle yxml" has been discontinued. 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1024 
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1025 
Isabelle/ML or Isabelle/Scala. 
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset

1026 

62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1027 
* File.bash_string, File.bash_path etc. represent Isabelle/ML and 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1028 
Isabelle/Scala strings authentically within GNU bash. This is useful to 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1029 
produce robust shell scripts under program control, without worrying 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1030 
about spaces or special characters. Note that user output works via 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1031 
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1032 
less versatile) operations File.shell_quote, File.shell_path etc. have 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1033 
been discontinued. 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset

1034 

62591  1035 
* SML/NJ and old versions of Poly/ML are no longer supported. 
1036 

62642  1037 
* Poly/ML heaps now follow the hierarchy of sessions, and thus require 
1038 
much less disk space. 

1039 

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

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

1041 
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

1042 
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

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

1044 

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

1048 
resulting log files. 

64308  1049 

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

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

1051 
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

1052 
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

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

1054 

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

1057 
but without the Isabelle settings environment. 

1058 

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

1061 
servers with separate CPU/memory modules. 

1062 

62354  1063 

1064 

62031  1065 
New in Isabelle2016 (February 2016) 
62016  1066 
 
60138  1067 

61337  1068 
*** General *** 
1069 

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

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

1071 
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

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

1073 
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

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

1075 

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

1078 

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

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

1082 
has been removed (see below). 

1083 

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

62017  1086 

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

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

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

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

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

1091 

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

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

1093 
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

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

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

1096 

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

1099 
to update old sources. 

1100 

61337  1101 
* Toplevel theorem statements have been simplified as follows: 
1102 

1103 
theorems ~> lemmas 

1104 
schematic_lemma ~> schematic_goal 

1105 
schematic_theorem ~> schematic_goal 

1106 
schematic_corollary ~> schematic_goal 

1107 

1108 
Commandline tool "isabelle update_theorems" updates theory sources 

1109 
accordingly. 

1110 

61338  1111 
* Toplevel theorem statement 'proposition' is another alias for 
1112 
'theorem'. 

1113 

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

1116 
deferred definitions require a surrounding 'overloading' block. 

1117 

61337  1118 

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

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

1120 

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

1124 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1128 
any effect on the running ML program. 

60984  1129 

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

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

1133 
update. 

61729  1134 

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

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

1137 
enable option "editor_output_state". 

61215  1138 

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

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

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

1143 
visibility. 

1144 

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

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

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

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

1149 
panel. 

1150 

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

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

1152 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1153 

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

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

1156 
implicit: a popup will show up unconditionally. 

1157 

1158 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1161 

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

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

1163 
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

1164 
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

1165 
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

1166 

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

1169 
the editor. 

1170 

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

1172 
instead of former C+e LEFT. 

1173 

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

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

1176 
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

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

1178 

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

1181 
singleinstance applications seen on common GUI desktops. 

1182 

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

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

1184 
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

1185 
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

1186 

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

1189 

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

1192 

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

1193 

61405  1194 
*** Document preparation *** 
1195 

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

1198 

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

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

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

1202 

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

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

1205 
follows: 

1206 

1207 
\<^item> itemize 

1208 
\<^enum> enumerate 

1209 
\<^descr> description 

1210 

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

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

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

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

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

1217 

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

1220 
standard LaTeX macros of the same names. 

1221 

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

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

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

1226 
cartouche tokens seen in theory sources. 

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

1227 

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

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

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

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

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

1233 

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

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

1237 

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

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

1240 

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

1242 

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

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

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

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

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

1248 
documentation, with a hyperlink in the Prover IDE. 

1249 

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

1251 
entities of the Isar language. 

1252 

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

61488  1255 
print mode "HTML" loses its special meaning. 
61471  1256 

61405  1257 

60406  1258 
*** Isar *** 
1259 

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

1262 
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

1263 
example: 
60414  1264 

1265 
have result: "C x y" 

1266 
if "A x" and "B y" 

1267 
for x :: 'a and y :: 'a 

1268 
<proof> 

1269 

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

60414  1272 
corresponds to a raw proof block like this: 
1273 

1274 
{ 

1275 
fix x :: 'a and y :: 'a 

60449  1276 
assume that: "A x" "B y" 
60414  1277 
have "C x y" <proof> 
1278 
} 

1279 
note result = this 

60406  1280 

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

1281 
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

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

1283 

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

61658  1286 

1287 
assume result: "C x y" 

1288 
if "A x" and "B y" 

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

1290 

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

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

1293 

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

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

1296 
example: 

1297 

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

1299 

1300 
is equivalent to: 

1301 

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

1303 

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

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

60595  1308 

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

1310 

1311 
or: 

1312 

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

1314 

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

1316 

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

1318 

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

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

1322 
of the local context elements yet. 

1323 

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

1326 

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

1328 
then have something 

1329 
proof cases 

1330 
case a 

1331 
then show ?thesis <proof> 

1332 
next 

1333 
case b 

1334 
then show ?thesis <proof> 

1335 
next 

1336 
case c 

1337 
then show ?thesis <proof> 

1338 
qed 

1339 

60565  1340 
* Command 'case' allows fact name and attribute specification like this: 
1341 

1342 
case a: (c xs) 

1343 
case a [attributes]: (c xs) 

1344 

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

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

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

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

1349 
and always put attributes in front. 

1350 

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

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

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

1353 
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

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

1355 

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

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

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

1360 

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

1362 
supply [simp] = a 

1363 
proof 

1364 
show A by simp 

1365 
next 

1366 
show A by simp 

1367 
qed 

1368 

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

1370 
proof body as well, abstracted over relevant parameters. 

1371 

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

1373 
parameter scope for of each clause. 

1374 

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

1376 
statements: result is abstracted over unknowns. 

1377 

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

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

1381 
manual. 

1382 

62017  1383 
* Command 'supply' supports fact definitions during goal refinement 
038ee85c95e4
misc tuning for releas 