author  wenzelm 
Sat, 01 Oct 2016 12:03:27 +0200  
changeset 63977  ec0fb01c6d50 
parent 63967  2aa42596edc3 
child 63979  95c3ae4baba8 
permissions  rwrr 
57491  1 
Isabelle NEWS  history of userrelevant changes 
2 
================================================= 

2553  3 

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

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

60331  6 

62216  7 
New in this Isabelle version 
8 
 

9 

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 

62440  63 

62904  64 
*** Prover IDE  Isabelle/Scala/jEdit *** 
65 

63977  66 
* Highlighting of entity def/ref positions wrt. cursor. 
67 

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

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

70 
systematic renaming. 

71 

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

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

74 
theorem statement. 

75 

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

77 
situations where old ASCII notation may be updated. 

78 

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

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

82 
inaccessible via keyboard completion). 

83 

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

86 

87 
src/Pure/ROOT0.ML 

88 
src/Pure/ROOT.ML 

89 
src/Pure/Pure.thy 

90 
src/Pure/ML_Bootstrap.thy 

91 

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

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

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

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

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

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

63307  98 
dependencies of the above files are only observed for batch build. 
62904  99 

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

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

63461  103 

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

106 

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

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

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

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

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

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

112 
"jedit_indent_newline". 
63452  113 

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

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

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

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

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

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

119 

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

122 
structure of theory specifications is treated as well. 

63236  123 

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

126 
keymap; nonconflicting changes are always applied implicitly. This 

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

128 
increases chances that users see new keyboard shortcuts when reusing 

129 
old keymaps. 

130 

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

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

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

133 

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

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

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

136 

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

140 
new 'abbrevs' section. 

141 

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

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

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

63579  145 

63675  146 
* ML and document antiquotations for filesystems paths are more uniform 
147 
and diverse: 

148 

149 
@{path NAME}  no filesystem check 

150 
@{file NAME}  check for plain file 

151 
@{dir NAME}  check for directory 

152 

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

154 
have to be changed. 

63669  155 

156 

63977  157 
*** Document preparation *** 
158 

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

160 

161 
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close>  

162 
this allows special forms of document output. 

163 

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

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

166 
derivatives. 

167 

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

169 

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

171 
Isabelle2015). 

172 

173 

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

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

175 

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

178 
'definition', 'inductive', 'function'. 

179 

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

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

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

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

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

185 

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

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

63039  190 

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

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

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

193 

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

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

195 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  196 

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

199 

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

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

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

203 

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

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

206 
INCOMPATIBILITY. 

62939  207 

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

210 
definitions. 

211 

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

63259  214 

215 
(use facts in simp) 

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

217 

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

220 

62216  221 

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

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

223 

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

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

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

228 

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

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

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

232 
regardless of the actual parameters that are provided. Rare 

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

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

235 

236 
* Typeinference improves sorts of newly introduced type variables for 

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

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

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

240 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 

241 
types where this is really intended. 

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

242 

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

243 

62327  244 
*** HOL *** 
245 

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

248 
propositional logic, goals based on a combination of quantifierfree 

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

250 
quantifierfree propositional logic with linear real arithmetic 

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

252 

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

63785  254 
break existing proofs. INCOMPATIBILITY. 
255 

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

257 
 The MaSh relevance filter is now faster than before. 
63116  258 
 Produce syntactically correct Vampire 4.0 problem files. 
259 

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

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

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

62335  276 
 Renamed lemmas: 
277 
rel_prod_apply ~> rel_prod_inject 

278 
pred_prod_apply ~> pred_prod_inject 

279 
INCOMPATIBILITY. 

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

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

283 
INCOMPATIBILITY. 

62327  284 

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

287 
which exposed details of the internal fixpoint construction and was 

288 
hard to use. INCOMPATIBILITY. 

289 

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

291 

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

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

294 

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

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

297 
eliminated altogether. 

298 

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

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

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

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

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

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

305 
INCOMPATIBILITY in rare situations. 

306 

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

308 
INCOMPATIBILITY. 

309 

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

311 
corresponding to {0..255}. 

312 

313 
 Logical representation: 

314 
* 0 is instantiated to the ASCII zero character. 

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

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

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

318 
are noncanonical. 

319 
 Printing and parsing: 

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

321 
(as before). 

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

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

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

325 
is parsable for every numeral expression n. 

326 
* Noncanonical characters have no special syntax and are 

327 
printed as their logical representation. 

328 
 Explicit conversions from and to the natural numbers are 

329 
provided as char_of_nat, nat_of_char (as before). 

330 
 The auxiliary nibble type has been discontinued. 

331 

332 
INCOMPATIBILITY. 

333 

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

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

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

337 
infix "mod" syntax. INCOMPATIBILITY. 

338 

339 
* Constant "surj" is a mere input abbreviation, to avoid hiding an 

340 
equation in term output. Minor INCOMPATIBILITY. 

341 

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

343 
which renders those abstract effectively. 

344 

345 
* Command 'export_code' checks given constants for abstraction 

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

347 
interface for the generated code. 

348 

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

350 
spelt out explicitly. 

351 

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

353 
explicitly provided auxiliary definitions for required type class 

354 
dictionaries rather than halfworking magic. INCOMPATIBILITY, see 

355 
the tutorial on code generation for details. 

356 

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

358 
and products. 

359 

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

361 
prod_list, INCOMPATIBILITY. 

362 

363 
* Locale bijection establishes convenient default simp rules such as 

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

365 

366 
* Abstract locales semigroup, abel_semigroup, semilattice, 

367 
semilattice_neutr, ordering, ordering_top, semilattice_order, 

368 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 

369 
semilattice_neutr_set, semilattice_order_set, 

370 
semilattice_order_neutr_set monoid_list, comm_monoid_list, 

371 
comm_monoid_list_set, comm_monoid_mset, comm_monoid_fun use boldified 

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

373 
INCOMPATIBILITY. 

374 

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

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

377 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

378 

63807  379 
* Some old / obsolete theorems have been renamed / removed, potential 
380 
INCOMPATIBILITY. 

381 

382 
nat_less_cases  removed, use linorder_cases instead 

383 
inv_image_comp  removed, use image_inv_f_f instead 

384 
image_surj_f_inv_f ~> image_f_inv_f 

63113  385 

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

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

387 
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

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

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

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

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

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

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

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

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

396 

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

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

398 
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

399 
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

400 
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

401 
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

402 
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

403 
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

404 
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

405 
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

406 
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

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

408 

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

62396  411 

63977  412 
* Added class topological_monoid. 
413 

414 
* HOLLibrary: theory FinFun bundles "finfun_syntax" and 

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

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

417 
"unbundle finfun_syntax" to imitate import of 

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

419 

420 
* HOLLibrary: theory Set_Permutations (executably) defines the set of 

421 
permutations of a set, i.e. the set of all lists that contain every 

422 
element of the carrier set exactly once. 

423 

424 
* HOLLibrary: multiset membership is now expressed using set_mset 

425 
rather than count. 

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

426 

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

427 
 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

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

429 

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

430 
 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

431 
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

432 

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

433 
 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

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

435 

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

436 
 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

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

438 

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

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

440 

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

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

444 
underscores. 

445 

446 
* HOLLibrary: theory Combinator_PER provides combinator to build 

447 
partial equivalence relations from a predicate and an equivalence 

448 
relation. 

449 

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

451 
fix bijections. 

452 

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

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

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

456 
normalized wrt. unit factors). 

457 

458 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 

459 

460 
* Session HOLMultivariate_Analysis has been renamed to HOLAnalysis. 

461 

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

463 
When importing HOLAnalysis some theorems need additional name spaces 

464 
prefixes due to name clashes. INCOMPATIBILITY. 

465 

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

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

468 
Residue theorem, Schwarz Lemma. 

469 

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

471 
and the Kreinâ€“Milman Minkowski theorem. 

472 

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

474 
homeomorphisms, continuous function extensions and other advanced topics 

475 
in topology 

476 

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

478 
ereal to ennreal, INCOMPATIBILITY. 

479 

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

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

482 

483 
* HOLProbability: Code generation and QuickCheck for Probability Mass 

484 
Functions. 

485 

486 
* HOLProbability: theory Random_Permutations contains some theory about 

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

488 
list in random order. 

489 

490 
* HOLProbability: theory SPMF formalises discrete subprobability 

491 
distributions. 

492 

493 
* HOLNumber_Theory: algebraic foundation for primes: Generalisation of 

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

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

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

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

498 
"prime_nat_iff". INCOMPATIBILITY. 

499 

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

501 
distinguish which ordering the theorems are about 

502 

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

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

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

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

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

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

508 
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

509 
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

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

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

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

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

514 
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

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

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

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

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

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

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

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

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

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

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

525 
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

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

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

528 

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

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

531 

63977  532 
* 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

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

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

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

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

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

538 

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

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

542 
interpretations "multiset_linorder" and "multiset_wellorder" have been 

543 
replaced by instantiations. INCOMPATIBILITY. 

544 

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

546 
renamed: 

547 

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

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

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

550 
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

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

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

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

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

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

556 
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

557 

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

558 
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

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

560 
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

561 
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

562 
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

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

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

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

566 
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

567 
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

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

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

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

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

572 

63977  573 
* HOLLibrary: the lemma mset_map has now the attribute [simp]. 
574 
INCOMPATIBILITY. 

575 

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

577 
INCOMPATIBILITY, use the following replacements: 

578 

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

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

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

581 
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

582 
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right 
63977  583 

584 
* HOLLibrary: some typeclass constraints about multisets have been 

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

586 
additional typeclasses order_bot, no_top, 

587 
ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, 

588 
linordered_cancel_ab_semigroup_add, and 

589 
ordered_ab_semigroup_monoid_add_imp_le. INCOMPATIBILITY. 

590 

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

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

593 
INCOMPATIBILITY. 

594 

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

596 
interpretations ordered_ab_semigroup_monoid_add_imp_le and 

597 
bounded_lattice_bot. INCOMPATIBILITY. 

598 

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

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

601 
changed: 

602 

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

603 
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

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

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

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

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

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

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

610 

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

613 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

654 

63977  655 
* HOLLibrary/Multiset. The definitions of some constants have changed 
656 
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

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

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

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

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

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

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

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

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

665 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

688 

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

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

692 

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

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

695 
INCOMPATIBILITY. 

696 

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

63830  698 
msetsum ~> sum_mset 
699 
msetprod ~> prod_mset 

700 

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

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

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

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

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

706 

63977  707 
* HOLLibrary/Multiset. The lemma one_step_implies_mult_aux on multisets 
708 
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

709 

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

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

711 
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

712 
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

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

714 

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

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

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

717 

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

720 

62345  721 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 
722 

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

723 
* The type class ordered_comm_monoid_add is now called 
63977  724 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add 
725 
is introduced as the combination of ordered_ab_semigroup_add + 

726 
comm_monoid_add. INCOMPATIBILITY. 

727 

728 
* Introduced the type classes canonically_ordered_comm_monoid_add and 

729 
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

730 

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

731 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 
63977  732 
instantiating linordered_semiring_strict and ordered_ab_group_add, an 
733 
explicit instantiation of ordered_ab_semigroup_monoid_add_imp_le might 

734 
be required. INCOMPATIBILITY. 

735 

736 
* HOLLibrary: theory Complete_Partial_Order2 provides reasoning support 

737 
for monotonicity and continuity in chaincomplete partial orders and 

738 
about admissibility conditions for fixpoint inductions. 

739 

740 
* HOLLibrary: theory Polynomial contains also derivation of polynomials 

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

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

743 
possible future different type class instantiation for polynomials over 

744 
factorial rings. INCOMPATIBILITY. 

745 

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

747 
following renaming 

748 

63173  749 
prefixeq > prefix 
750 
prefix > strict_prefix 

751 
suffixeq > suffix 

752 
suffix > strict_suffix 

63977  753 

754 
Added theory of longest common prefixes. 

63117  755 

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

758 
lcm_left_commute_nat ~> lcm.left_commute 

759 
lcm_left_commute_int ~> lcm.left_commute 

760 
gcd_left_commute_nat ~> gcd.left_commute 

761 
gcd_left_commute_int ~> gcd.left_commute 

762 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

763 
gcd_greatest_iff_int ~> gcd_greatest_iff 

764 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

765 
coprime_dvd_mult_int ~> coprime_dvd_mult 

766 
zpower_numeral_even ~> power_numeral_even 

767 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

768 
gcd_mult_cancel_int ~> gcd_mult_cancel 

769 
div_gcd_coprime_nat ~> div_gcd_coprime 

770 
div_gcd_coprime_int ~> div_gcd_coprime 

771 
zpower_numeral_odd ~> power_numeral_odd 

772 
zero_less_int_conv ~> of_nat_0_less_iff 

773 
gcd_greatest_nat ~> gcd_greatest 

774 
gcd_greatest_int ~> gcd_greatest 

775 
coprime_mult_nat ~> coprime_mult 

776 
coprime_mult_int ~> coprime_mult 

777 
lcm_commute_nat ~> lcm.commute 

778 
lcm_commute_int ~> lcm.commute 

779 
int_less_0_conv ~> of_nat_less_0_iff 

780 
gcd_commute_nat ~> gcd.commute 

781 
gcd_commute_int ~> gcd.commute 

782 
Gcd_insert_nat ~> Gcd_insert 

783 
Gcd_insert_int ~> Gcd_insert 

784 
of_int_int_eq ~> of_int_of_nat_eq 

785 
lcm_least_nat ~> lcm_least 

786 
lcm_least_int ~> lcm_least 

787 
lcm_assoc_nat ~> lcm.assoc 

788 
lcm_assoc_int ~> lcm.assoc 

789 
int_le_0_conv ~> of_nat_le_0_iff 

790 
int_eq_0_conv ~> of_nat_eq_0_iff 

791 
Gcd_empty_nat ~> Gcd_empty 

792 
Gcd_empty_int ~> Gcd_empty 

793 
gcd_assoc_nat ~> gcd.assoc 

794 
gcd_assoc_int ~> gcd.assoc 

795 
zero_zle_int ~> of_nat_0_le_iff 

796 
lcm_dvd2_nat ~> dvd_lcm2 

797 
lcm_dvd2_int ~> dvd_lcm2 

798 
lcm_dvd1_nat ~> dvd_lcm1 

799 
lcm_dvd1_int ~> dvd_lcm1 

800 
gcd_zero_nat ~> gcd_eq_0_iff 

801 
gcd_zero_int ~> gcd_eq_0_iff 

802 
gcd_dvd2_nat ~> gcd_dvd2 

803 
gcd_dvd2_int ~> gcd_dvd2 

804 
gcd_dvd1_nat ~> gcd_dvd1 

805 
gcd_dvd1_int ~> gcd_dvd1 

806 
int_numeral ~> of_nat_numeral 

807 
lcm_ac_nat ~> ac_simps 

808 
lcm_ac_int ~> ac_simps 

809 
gcd_ac_nat ~> ac_simps 

810 
gcd_ac_int ~> ac_simps 

811 
abs_int_eq ~> abs_of_nat 

812 
zless_int ~> of_nat_less_iff 

813 
zdiff_int ~> of_nat_diff 

814 
zadd_int ~> of_nat_add 

815 
int_mult ~> of_nat_mult 

816 
int_Suc ~> of_nat_Suc 

817 
inj_int ~> inj_of_nat 

818 
int_1 ~> of_nat_1 

819 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

842 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  843 
realpow_minus_mult ~> power_minus_mult 
844 
realpow_Suc_le_self ~> power_Suc_le_self 

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

845 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  846 
INCOMPATIBILITY. 
847 

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

848 
* Renamed HOL/Quotient_Examples/FSet.thy to 
63977  849 
HOL/Quotient_Examples/Quotient_FSet.thy INCOMPATIBILITY. 
850 

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

851 

62498  852 
*** ML *** 
853 

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

856 

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

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

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

861 
INCOMPATIBILITY. 

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

862 

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

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

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

870 

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

873 
requiring separate files. 

874 

62851  875 
* 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

876 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 
62851  877 

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

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

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

880 

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

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

884 
debugger information requires consirable time and space: main 

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

886 

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

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

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

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

892 
balanced blocks of Local_Theory.open_target versus 

893 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

894 

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

897 
INCOMPATIBILITY. 

898 

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

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

902 
File.full_path). Potential INCOMPATIBILITY. 

903 

63352  904 
* Binding.empty_atts supersedes Thm.empty_binding and 
905 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

906 

62498  907 

62354  908 
*** System *** 
909 

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

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

911 
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

912 
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

913 
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

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

915 

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

918 
"isabelle_scala_script". 

919 

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

922 
Isabelle_Tool.Body. 

923 

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

926 
particular: 

927 

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

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

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

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

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

932 

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

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

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

936 

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

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

938 
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

939 
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

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

941 

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

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

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

944 

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

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

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

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

948 

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

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

950 
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

951 
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

952 
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

953 
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

954 
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

955 
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

956 

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

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

961 

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

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

963 
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

964 
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

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

966 

62354  967 

968 

62031  969 
New in Isabelle2016 (February 2016) 
62016  970 
 
60138  971 

61337  972 
*** General *** 
973 

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

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

975 
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

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

977 
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

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

979 

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

982 

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

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

986 
has been removed (see below). 

987 

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

62017  990 

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

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

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

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

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

995 

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

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

997 
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

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

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

1000 

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

1003 
to update old sources. 

1004 

61337  1005 
* Toplevel theorem statements have been simplified as follows: 
1006 

1007 
theorems ~> lemmas 

1008 
schematic_lemma ~> schematic_goal 

1009 
schematic_theorem ~> schematic_goal 

1010 
schematic_corollary ~> schematic_goal 

1011 

1012 
Commandline tool "isabelle update_theorems" updates theory sources 

1013 
accordingly. 

1014 

61338  1015 
* Toplevel theorem statement 'proposition' is another alias for 
1016 
'theorem'. 

1017 

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

1020 
deferred definitions require a surrounding 'overloading' block. 

1021 

61337  1022 

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

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

1024 

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

1028 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

1032 
any effect on the running ML program. 

60984  1033 

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

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

1037 
update. 

61729  1038 

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

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

1041 
enable option "editor_output_state". 

61215  1042 

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

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

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

1047 
visibility. 

1048 

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

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

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

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

1053 
panel. 

1054 

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

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

1056 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1057 

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

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

1060 
implicit: a popup will show up unconditionally. 

1061 

1062 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1065 

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

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

1067 
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

1068 
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

1069 
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

1070 

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

1073 
the editor. 

1074 

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

1076 
instead of former C+e LEFT. 

1077 

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

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

1080 
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

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

1082 

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

1085 
singleinstance applications seen on common GUI desktops. 

1086 

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

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

1088 
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

1089 
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

1090 

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

1093 

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

1096 

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

1097 

61405  1098 
*** Document preparation *** 
1099 

63553
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset

1100 
* Text and ML antiquotation @{locale} for locales, similar to existing 
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset

1101 
antiquotations for classes. 
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset

1102 

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

1105 

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

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

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

1109 

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

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

1112 
follows: 

1113 

1114 
\<^item> itemize 

1115 
\<^enum> enumerate 

1116 
\<^descr> description 

1117 

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

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

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

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

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

1124 

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

1127 
standard LaTeX macros of the same names. 

1128 

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

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

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

1133 
cartouche tokens seen in theory sources. 

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

1134 

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

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

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

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

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

1140 

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

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

1144 

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

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

1147 

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

1149 

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

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

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

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

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

1155 
documentation, with a hyperlink in the Prover IDE. 

1156 

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

1158 
entities of the Isar language. 

1159 

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

61488  1162 
print mode "HTML" loses its special meaning. 
61471  1163 

61405  1164 

60406  1165 
*** Isar *** 
1166 

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

1169 
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

1170 
example: 
60414  1171 

1172 
have result: "C x y" 

1173 
if "A x" and "B y" 

1174 
for x :: 'a and y :: 'a 

1175 
<proof> 

1176 

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

60414  1179 
corresponds to a raw proof block like this: 
1180 

1181 
{ 

1182 
fix x :: 'a and y :: 'a 

60449  1183 
assume that: "A x" "B y" 
60414  1184 
have "C x y" <proof> 
1185 
} 

1186 
note result = this 

60406  1187 

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

1188 
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

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

1190 

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

61658  1193 

1194 
assume result: "C x y" 

1195 
if "A x" and "B y" 

1196 
for x :: 'a and y :: 'a 

1197 

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

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

1200 

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

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

1203 
example: 

1204 

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

1206 

1207 
is equivalent to: 

1208 

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

1210 

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

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

60595  1215 

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

1217 

1218 
or: 

1219 

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

1221 

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

1223 

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

1225 

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

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

1229 
of the local context elements yet. 

1230 

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

1233 

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

1235 
then have something 

1236 
proof cases 

1237 
case a 

1238 
then show ?thesis <proof> 

1239 
next 

1240 
case b 

1241 
then show ?thesis <proof> 

1242 
next 

1243 
case c 

1244 
then show ?thesis <proof> 

1245 
qed 

1246 

60565  1247 
* Command 'case' allows fact name and attribute specification like this: 
1248 

1249 
case a: (c xs) 

1250 
case a [attributes]: (c xs) 

1251 

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

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

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

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

1256 
and always put attributes in front. 

1257 

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

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

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

1260 
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

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

1262 

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

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

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

1267 

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

1269 
supply [simp] = a 

1270 
proof 

1271 
show A by simp 

1272 
next 

1273 
show A by simp 

1274 
qed 

1275 

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

1277 
proof body as well, abstracted over relevant parameters. 

1278 

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

1280 
parameter scope for of each clause. 

1281 

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

1283 
statements: result is abstracted over unknowns. 

1284 

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

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

1288 
manual. 

1289 

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

1292 

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

1293 
* Proof method "goal_cases" turns the current subgoals into cases within 
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

1294 
the context; the conclusion is bound to variable ?case in each case. For 
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

1295 
example: 
60617  1296 

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

60622  1298 
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" 
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset

1299 
proof goal_cases 
60622  1300 
case (1 x) 
1301 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

1302 
next 

1303 
case (2 y z) 

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

1305 
qed 

1306 

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

1308 
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" 

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

1309 
proof goal_cases 
60617  1310 
case prems: 1 
1311 
then show ?case using prems sorry 

1312 
next 

1313 
case prems: 2 

1314 
then show ?case using prems sorry 

1315 
qed 

60578  1316 

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

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

60581  1321 

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

60551  1324 

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

1327 

60406  1328 

60331  1329 
*** Pure *** 
1330 

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

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

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

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

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

1335 

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

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

1338 

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

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

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

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

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

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

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

1347 

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

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

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

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

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

1352 

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

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

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

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

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

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

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

1359 

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

1362 

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

61675  1364 
'defines'. 
1365 

61895  1366 
* Command 'permanent_interpretation' has been discontinued. Use 
1367 
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. 

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

1368 

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

1371 

60331  1372 
* Configuration option rule_insts_schematic has been discontinued 
62017  1373 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 
60331  1374 

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

1377 
exploited. 

60347  1378 

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

62205  1380 
operations behave more similar to abbreviations. Potential 
60347  1381 
INCOMPATIBILITY in exotic situations. 
1382 

1383 

60171
b3be7677461e
no more simp_ 