author  fleury <Mathias.Fleury@mpiinf.mpg.de> 
Mon, 19 Sep 2016 20:07:39 +0200  
changeset 63919  9aed2da07200 
parent 63918  6bf55e6e0b75 
child 63920  003622e08379 
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 

63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63113
diff
changeset

12 
* Embedded content (e.g. the inner syntax of types, terms, props) may be 
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63113
diff
changeset

13 
delimited uniformly via cartouches. This works better than oldfashioned 
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63113
diff
changeset

14 
quotes when sublanguages are nested. 
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63113
diff
changeset

15 

62958
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

16 
* Typeinference improves sorts of newly introduced type variables for 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

17 
the objectlogic, using its base sort (i.e. HOL.type for Isabelle/HOL). 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

18 
Thus terms like "f x" or "\<And>x. P x" without any further syntactic context 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

19 
produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

20 
INCOMPATIBILITY, need to provide explicit type constraints for Pure 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

21 
types where this is really intended. 
b41c1cb5e251
Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents:
62939
diff
changeset

22 

62969  23 
* Simplified outer syntax: uniform category "name" includes long 
24 
identifiers. Former "xname" / "nameref" / "name reference" has been 

25 
discontinued. 

26 

62807  27 
* Mixfix annotations support general block properties, with syntax 
28 
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent", 

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

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

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

62789  32 

62440  33 
* New symbol \<circle>, e.g. for temporal operator. 
34 

62453  35 
* Old 'header' command is no longer supported (legacy since 
36 
Isabelle2015). 

37 

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

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

41 

42 
bundle foo 

43 
begin 

44 
declare a [simp] 

45 
declare b [intro] 

46 
end 

63272  47 

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

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

51 

63650  52 
* Splitter in simp, auto and friends: 
53 
 The syntax "split add" has been discontinued, use plain "split". 

63656  54 
 For situations with many conditional or case expressions, 
63650  55 
there is an alternative splitting strategy that can be much faster. 
56 
It is selected by writing "split!" instead of "split". It applies 

57 
safe introduction and elimination rules after each split rule. 

58 
As a result the subgoal may be split into several subgoals. 

59 

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

62 

63532
b01154b74314
provide Pure.simp/simp_all, which only know about metaequality;
wenzelm
parents:
63528
diff
changeset

63 
* Pure provides basic versions of proof methods "simp" and "simp_all" 
b01154b74314
provide Pure.simp/simp_all, which only know about metaequality;
wenzelm
parents:
63528
diff
changeset

64 
that only know about metaequality (==). Potential INCOMPATIBILITY in 
b01154b74314
provide Pure.simp/simp_all, which only know about metaequality;
wenzelm
parents:
63528
diff
changeset

65 
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order 
b01154b74314
provide Pure.simp/simp_all, which only know about metaequality;
wenzelm
parents:
63528
diff
changeset

66 
is relevant to avoid confusion of Pure.simp vs. HOL.simp. 
b01154b74314
provide Pure.simp/simp_all, which only know about metaequality;
wenzelm
parents:
63528
diff
changeset

67 

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

68 
* Commands 'prf' and 'full_prf' are somewhat more informative (again): 
63821  69 
proof terms are reconstructed and cleaned from administrative thm 
70 
nodes. 

71 

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

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

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

75 
regardless of the actual parameters that are provided. Rare 

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

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

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

78 

62440  79 

62904  80 
*** Prover IDE  Isabelle/Scala/jEdit *** 
81 

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

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

85 
inaccessible via keyboard completion). 

86 

63135  87 
* Cartouche abbreviations work both for " and ` to accomodate typical 
88 
situations where old ASCII notation may be updated. 

89 

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

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

93 

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

96 

97 
src/Pure/ROOT0.ML 

98 
src/Pure/ROOT.ML 

99 
src/Pure/Pure.thy 

100 
src/Pure/ML_Bootstrap.thy 

101 

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

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

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

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

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

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

63307  108 
dependencies of the above files are only observed for batch build. 
62904  109 

62987
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62969
diff
changeset

110 
* Highlighting of entity def/ref positions wrt. cursor. 
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62969
diff
changeset

111 

63461  112 
* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' 
63592
64db21931bcb
include 'begin' and 'end' structure in text folds;
wenzelm
parents:
63581
diff
changeset

113 
are treated as delimiters for fold structure; 'begin' and 'end' 
64db21931bcb
include 'begin' and 'end' structure in text folds;
wenzelm
parents:
63581
diff
changeset

114 
structure of theory specifications is treated as well. 
63461  115 

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

118 

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

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

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

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

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

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

124 
"jedit_indent_newline". 
63452  125 

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

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

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

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

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

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

131 

63236  132 
* Action "isabelle.selectentity" (shortcut CS+ENTER) selects all 
133 
occurences of the formal entity at the caret position. This facilitates 

134 
systematic renaming. 

135 

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

138 
keymap; nonconflicting changes are always applied implicitly. This 

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

140 
increases chances that users see new keyboard shortcuts when reusing 

141 
old keymaps. 

142 

63032
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset

143 
* Document markup works across multiple Isar commands, e.g. the results 
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset

144 
established at the end of a proof are properly identified in the theorem 
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset

145 
statement. 
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset

146 

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

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

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

149 

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

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

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

152 

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

156 
new 'abbrevs' section. 

157 

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

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

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

63579  161 

63675  162 
* ML and document antiquotations for filesystems paths are more uniform 
163 
and diverse: 

164 

165 
@{path NAME}  no filesystem check 

166 
@{file NAME}  check for plain file 

167 
@{dir NAME}  check for directory 

168 

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

170 
have to be changed. 

63669  171 

172 

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

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

174 

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

177 

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

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

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

181 

63178  182 
* Command 'axiomatization' has become more restrictive to correspond 
183 
better to internal axioms as singleton facts with mandatory name. Minor 

184 
INCOMPATIBILITY. 

185 

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

188 
'definition', 'inductive', 'function'. 

189 

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

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

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

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

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

195 

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

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

63039  200 

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

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

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

203 

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

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

205 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  206 

62939  207 
* The old proof method "default" has been removed (legacy since 
208 
Isabelle2016). INCOMPATIBILITY, use "standard" instead. 

209 

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

212 
definitions. 

213 

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

63259  216 

217 
(use facts in simp) 

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

219 

62216  220 

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

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

222 

63166  223 
* Code generator: config option "code_timing" triggers measurements of 
224 
different phases of code generation. See src/HOL/ex/Code_Timing.thy for 

225 
examples. 

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

226 

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

227 
* Code generator: implicits in Scala (stemming from type class instances) 
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset

228 
are generated into companion object of corresponding type class, to resolve 
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset

229 
some situations where ambiguities may occur. 
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset

230 

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

231 

62327  232 
*** HOL *** 
233 

63909  234 
* The unique existence quantifier no longer provides 'binder' syntax, 
235 
but uses syntax translations (as for bounded unique existence). Thus 

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

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

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

63917  239 
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential 
63909  240 
INCOMPATIBILITY in rare situations. 
241 

63627  242 
* Renamed session HOLMultivariate_Analysis to HOLAnalysis. 
243 

244 
* Moved measure theory from HOLProbability to HOLAnalysis. When importing 

245 
HOLAnalysis some theorems need additional name spaces prefixes due to name 

246 
clashes. 

247 
INCOMPATIBILITY. 

248 

63635  249 
* Number_Theory: algebraic foundation for primes: Generalisation of 
250 
predicate "prime" and introduction of predicates "prime_elem", 

251 
"irreducible", a "prime_factorization" function, and the "factorial_ring" 

252 
typeclass with instance proofs for nat, int, poly. Some theorems now have 

253 
different names, most notably "prime_def" is now "prime_nat_iff". 

254 
INCOMPATIBILITY. 

63552  255 

256 
* Probability: Code generation and QuickCheck for Probability Mass 

257 
Functions. 

258 

63438  259 
* Theory Set_Interval.thy: substantial new theorems on indexed sums 
260 
and products. 

261 

63882
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset

262 
* Theory List.thy: 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset

263 
listsum ~> sum_list 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset

264 
listprod ~> prod_list 
018998c00003
renamed listsum > sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset

265 

63414  266 
* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying 
267 
equations in functional programming style: variables present on the 

268 
lefthand but not on the righhand side are replaced by underscores. 

269 

63416
6af79184bef3
avoid to hide equality behind (output) abbreviation
haftmann
parents:
63414
diff
changeset

270 
* "surj" is a mere input abbreviation, to avoid hiding an equation in 
6af79184bef3
avoid to hide equality behind (output) abbreviation
haftmann
parents:
63414
diff
changeset

271 
term output. Minor INCOMPATIBILITY. 
6af79184bef3
avoid to hide equality behind (output) abbreviation
haftmann
parents:
63414
diff
changeset

272 

63377
64adf4ba9526
combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
63375
diff
changeset

273 
* Theory Library/Combinator_PER.thy: combinator to build partial 
63378  274 
equivalence relations from a predicate and an equivalence relation. 
63377
64adf4ba9526
combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
63375
diff
changeset

275 

63375
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset

276 
* Theory Library/Perm.thy: basic facts about almost everywhere fix 
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset

277 
bijections. 
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset

278 

63374  279 
* Locale bijection establishes convenient default simp rules 
280 
like "inv f (f a) = a" for total bijections. 

281 

63343  282 
* Former locale lifting_syntax is now a bundle, which is easier to 
283 
include in a local context or theorem statement, e.g. "context includes 

284 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

285 

63303  286 
* Code generation for scala: ambiguous implicts in class diagrams 
287 
are spelt out explicitly. 

288 

63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

289 
* Abstract locales semigroup, abel_semigroup, semilattice, 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

290 
semilattice_neutr, ordering, ordering_top, semilattice_order, 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

291 
semilattice_neutr_order, comm_monoid_set, semilattice_set, 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

292 
semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

293 
monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset, 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

294 
comm_monoid_fun use boldified syntax uniformly that does not clash 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

295 
with corresponding global syntax. INCOMPATIBILITY. 
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset

296 

63237  297 
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic 
298 
INCOMPATIBILITY. 

299 

63174
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset

300 
* Command 'code_reflect' accepts empty constructor lists for datatypes, 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset

301 
which renders those abstract effectively. 
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset

302 

63175
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset

303 
* Command 'export_code' checks given constants for abstraction violations: 
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset

304 
a small guarantee that given constants specify a safe interface for the 
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset

305 
generated code. 
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset

306 

63144  307 
* Probability/Random_Permutations.thy contains some theory about 
308 
choosing a permutation of a set uniformly at random and folding over a 

309 
list in random order. 

310 

63246  311 
* Probability/SPMF formalises discrete subprobability distributions. 
312 

63283
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset

313 
* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax" 
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset

314 
allow to control optional syntax in local contexts; this supersedes 
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset

315 
former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle 
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset

316 
finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax". 
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset

317 

63144  318 
* Library/Set_Permutations.thy (executably) defines the set of 
319 
permutations of a set, i.e. the set of all lists that contain every 

320 
element of the carrier set exactly once. 

321 

63161
2660ba498798
delegate inclusion of required dictionaries to userspace instead of halfworking magic
haftmann
parents:
63155
diff
changeset

322 
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on 
2660ba498798
delegate inclusion of required dictionaries to userspace instead of halfworking magic
haftmann
parents:
63155
diff
changeset

323 
explicitly provided auxiliary definitions for required type class 
2660ba498798
delegate inclusion of required dictionaries to userspace instead of halfworking magic
haftmann
parents:
63155
diff
changeset

324 
dictionaries rather than halfworking magic. INCOMPATIBILITY, see 
2660ba498798
delegate inclusion of required dictionaries to userspace instead of halfworking magic
haftmann
parents:
63155
diff
changeset

325 
the tutorial on code generation for details. 
2660ba498798
delegate inclusion of required dictionaries to userspace instead of halfworking magic
haftmann
parents:
63155
diff
changeset

326 

62522  327 
* New abbreviations for negated existence (but not bounded existence): 
328 

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

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

331 

62521  332 
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" 
333 
has been removed for output. It is retained for input only, until it is 

334 
eliminated altogether. 

335 

63785  336 
* metis: The problem encoding has changed very slightly. This might 
337 
break existing proofs. INCOMPATIBILITY. 

338 

63116  339 
* Sledgehammer: 
63699  340 
 The MaSh relevance filter has been sped up. 
63116  341 
 Produce syntactically correct Vampire 4.0 problem files. 
342 

63891  343 
* The 'coinductive' command produces a proper coinduction rule for 
344 
mutual coinductive predicates. This new rule replaces the old rule, 

345 
which exposed details of the internal fixpoint construction and was 

346 
hard to use. INCOMPATIBILITY. 

347 

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

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

62842  352 
method. See 'isabelle doc corec'. 
62693  353 
 The predicator :: ('a => bool) => 'a F => bool is now a firstclass 
63855  354 
citizen in bounded natural functors. 
62693  355 
 'primrec' now allows nested calls through the predicator in addition 
62327  356 
to the map function. 
63855  357 
 'bnf' automatically discharges reflexive proof obligations. 
62693  358 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  359 
terms of map and set 
63855  360 
(not giving a specification for rel makes this one reflexive). 
62693  361 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  362 
(not giving a specification for pred makes this one reflexive). 
363 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  364 
 Renamed lemmas: 
365 
rel_prod_apply ~> rel_prod_inject 

366 
pred_prod_apply ~> pred_prod_inject 

367 
INCOMPATIBILITY. 

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

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

371 
INCOMPATIBILITY. 

62327  372 

63807  373 
* Some old / obsolete theorems have been renamed / removed, potential 
374 
INCOMPATIBILITY. 

375 

376 
nat_less_cases  removed, use linorder_cases instead 

377 
inv_image_comp  removed, use image_inv_f_f instead 

378 
image_surj_f_inv_f ~> image_f_inv_f 

63113  379 

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

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

381 
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

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

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

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

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

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

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

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

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

390 

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

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

392 
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

393 
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

394 
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

395 
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

396 
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

397 
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

398 
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

399 
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

400 
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

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

402 

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

62396  405 

62597  406 
* Characters (type char) are modelled as finite algebraic type 
407 
corresponding to {0..255}. 

408 

409 
 Logical representation: 

410 
* 0 is instantiated to the ASCII zero character. 

62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset

411 
* All other characters are represented as "Char n" 
62597  412 
with n being a raw numeral expression less than 256. 
62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset

413 
* Expressions of the form "Char n" with n greater than 255 
62597  414 
are noncanonical. 
415 
 Printing and parsing: 

62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset

416 
* Printable characters are printed and parsed as "CHR ''\<dots>''" 
62597  417 
(as before). 
62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset

418 
* The ASCII zero character is printed and parsed as "0". 
62678  419 
* All other canonical characters are printed as "CHR 0xXX" 
420 
with XX being the hexadecimal character code. "CHR n" 

62597  421 
is parsable for every numeral expression n. 
62598  422 
* Noncanonical characters have no special syntax and are 
62597  423 
printed as their logical representation. 
424 
 Explicit conversions from and to the natural numbers are 

425 
provided as char_of_nat, nat_of_char (as before). 

426 
 The auxiliary nibble type has been discontinued. 

427 

428 
INCOMPATIBILITY. 

429 

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

430 
* Multiset membership is now expressed using set_mset rather than count. 
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset

431 

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

432 
 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

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

434 

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

435 
 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

436 
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

437 

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

438 
 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

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

440 

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

441 
 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

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

443 

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

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

445 

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

446 
* The names of multiset theorems have been normalised to distinguish which 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

447 
ordering the theorems are about 
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63307
diff
changeset

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

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

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

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

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

453 
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

454 
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

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

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

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

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

459 
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

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

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

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

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

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

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

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

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

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

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

470 
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

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

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

473 

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

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

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

476 

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

477 
* Multisets are now ordered with the multiset ordering 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

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

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

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

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

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

483 

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

484 
* The prefix multiset_order has been discontinued: the theorems can be directly 
63407
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

485 
accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset" 
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

486 
have been discontinued, and the interpretations "multiset_linorder" and 
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

487 
"multiset_wellorder" have been replaced by instantiations. 
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset

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

489 

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

490 
* Some theorems about the multiset ordering have been renamed: 
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63384
diff
changeset

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

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

493 
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

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

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

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

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

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

499 
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

500 

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

501 
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

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

503 
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

504 
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

505 
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

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

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

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

509 
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

510 
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

511 
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

512 
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

513 
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

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

515 

63524
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63513
diff
changeset

516 
* The lemma mset_map has now the attribute [simp]. 
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63513
diff
changeset

517 
INCOMPATIBILITY. 
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63513
diff
changeset

518 

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

519 
* Some theorems about multisets have been removed: 
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63524
diff
changeset

520 
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

521 
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

522 
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

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

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

525 

63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

526 
* Some typeclass constraints about multisets have been reduced from ordered or 
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

527 
linordered to preorder. Multisets have the additional typeclasses order_bot, 
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

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

529 
linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le. 
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

530 
INCOMPATIBILITY. 
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

531 

63560
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63553
diff
changeset

532 
* There are some new simplification rules about multisets, the multiset 
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63553
diff
changeset

533 
ordering, and the subset ordering on multisets. 
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63553
diff
changeset

534 
INCOMPATIBILITY. 
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63553
diff
changeset

535 

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

536 
* The subset ordering on multisets has now the interpretations 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

537 
ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot. 
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

538 
INCOMPATIBILITY. 
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63407
diff
changeset

539 

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

540 
* Multiset: single has been removed in favor of add_mset that roughly 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

541 
corresponds to Set.insert. Some theorems have removed or changed: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

542 
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

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

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

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

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

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

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

549 

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

550 
* Multiset: some theorems have been changed to use add_mset instead of single: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

591 

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

592 
* Multiset: the definitions of some constants have changed to use add_mset instead 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

593 
of adding a single element: 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

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

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

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

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

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

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

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

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

602 

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

603 
* Due to the above changes, the attributes of some multiset theorems have 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

625 

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

626 
* The order of the variables in the second cases of multiset_induct, 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

627 
multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A). 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

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

629 

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

630 
* There is now a simplification procedure on multisets. It mimics the behavior 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

631 
of the procedure on natural numbers. 
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63785
diff
changeset

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

633 

63830  634 
* Renamed sums and products of multisets: 
635 
msetsum ~> sum_mset 

636 
msetprod ~> prod_mset 

637 

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

638 
* The symbols for intersection and union of multisets have been changed: 
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63918
diff
changeset

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

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

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

642 

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

643 
* The lemma one_step_implies_mult_aux on multisets has been removed, use 
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63793
diff
changeset

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

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

646 

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

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

648 
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

649 
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

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

651 

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

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

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

654 

62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62407
diff
changeset

655 
* More complex analysis including Cauchy's inequality, Liouville theorem, 
63078
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Kreinâ€“Milman
paulson <lp15@cam.ac.uk>
parents:
63066
diff
changeset

656 
open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma. 
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Kreinâ€“Milman
paulson <lp15@cam.ac.uk>
parents:
63066
diff
changeset

657 

e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Kreinâ€“Milman
paulson <lp15@cam.ac.uk>
parents:
63066
diff
changeset

658 
* Theory of polyhedra: faces, extreme points, polytopes, and the Kreinâ€“Milman 
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Kreinâ€“Milman
paulson <lp15@cam.ac.uk>
parents:
63066
diff
changeset

659 
Minkowski theorem. 
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62407
diff
changeset

660 

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

663 

62345  664 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 
665 

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

666 
* The type class ordered_comm_monoid_add is now called 
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

667 
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is 
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

668 
introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add. 
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

669 
INCOMPATIBILITY. 
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

670 

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

671 
* Introduced the type classes canonically_ordered_comm_monoid_add and dioid. 
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

672 

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

673 
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

674 
instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit 
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
63455
diff
changeset

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

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

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

678 

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

679 
* Added topological_monoid 
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

680 

62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset

681 
* Library/Complete_Partial_Order2.thy provides reasoning support for 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset

682 
proofs about monotonicity and continuity in chaincomplete partial 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset

683 
orders and about admissibility conditions for fixpoint inductions. 
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset

684 

62352
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

685 
* Library/Polynomial.thy contains also derivation of polynomials 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

686 
but not gcd/lcm on polynomials over fields. This has been moved 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

687 
to a separate theory Library/Polynomial_GCD_euclidean.thy, to 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

688 
pave way for a possible future different type class instantiation 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

689 
for polynomials over factorial rings. INCOMPATIBILITY. 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset

690 

63155  691 
* Library/Sublist.thy: added function "prefixes" and renamed 
63173  692 
prefixeq > prefix 
693 
prefix > strict_prefix 

694 
suffixeq > suffix 

695 
suffix > strict_suffix 

696 
Added theory of longest common prefixes. 

63117  697 

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

700 
lcm_left_commute_nat ~> lcm.left_commute 

701 
lcm_left_commute_int ~> lcm.left_commute 

702 
gcd_left_commute_nat ~> gcd.left_commute 

703 
gcd_left_commute_int ~> gcd.left_commute 

704 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

705 
gcd_greatest_iff_int ~> gcd_greatest_iff 

706 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

707 
coprime_dvd_mult_int ~> coprime_dvd_mult 

708 
zpower_numeral_even ~> power_numeral_even 

709 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

710 
gcd_mult_cancel_int ~> gcd_mult_cancel 

711 
div_gcd_coprime_nat ~> div_gcd_coprime 

712 
div_gcd_coprime_int ~> div_gcd_coprime 

713 
zpower_numeral_odd ~> power_numeral_odd 

714 
zero_less_int_conv ~> of_nat_0_less_iff 

715 
gcd_greatest_nat ~> gcd_greatest 

716 
gcd_greatest_int ~> gcd_greatest 

717 
coprime_mult_nat ~> coprime_mult 

718 
coprime_mult_int ~> coprime_mult 

719 
lcm_commute_nat ~> lcm.commute 

720 
lcm_commute_int ~> lcm.commute 

721 
int_less_0_conv ~> of_nat_less_0_iff 

722 
gcd_commute_nat ~> gcd.commute 

723 
gcd_commute_int ~> gcd.commute 

724 
Gcd_insert_nat ~> Gcd_insert 

725 
Gcd_insert_int ~> Gcd_insert 

726 
of_int_int_eq ~> of_int_of_nat_eq 

727 
lcm_least_nat ~> lcm_least 

728 
lcm_least_int ~> lcm_least 

729 
lcm_assoc_nat ~> lcm.assoc 

730 
lcm_assoc_int ~> lcm.assoc 

731 
int_le_0_conv ~> of_nat_le_0_iff 

732 
int_eq_0_conv ~> of_nat_eq_0_iff 

733 
Gcd_empty_nat ~> Gcd_empty 

734 
Gcd_empty_int ~> Gcd_empty 

735 
gcd_assoc_nat ~> gcd.assoc 

736 
gcd_assoc_int ~> gcd.assoc 

737 
zero_zle_int ~> of_nat_0_le_iff 

738 
lcm_dvd2_nat ~> dvd_lcm2 

739 
lcm_dvd2_int ~> dvd_lcm2 

740 
lcm_dvd1_nat ~> dvd_lcm1 

741 
lcm_dvd1_int ~> dvd_lcm1 

742 
gcd_zero_nat ~> gcd_eq_0_iff 

743 
gcd_zero_int ~> gcd_eq_0_iff 

744 
gcd_dvd2_nat ~> gcd_dvd2 

745 
gcd_dvd2_int ~> gcd_dvd2 

746 
gcd_dvd1_nat ~> gcd_dvd1 

747 
gcd_dvd1_int ~> gcd_dvd1 

748 
int_numeral ~> of_nat_numeral 

749 
lcm_ac_nat ~> ac_simps 

750 
lcm_ac_int ~> ac_simps 

751 
gcd_ac_nat ~> ac_simps 

752 
gcd_ac_int ~> ac_simps 

753 
abs_int_eq ~> abs_of_nat 

754 
zless_int ~> of_nat_less_iff 

755 
zdiff_int ~> of_nat_diff 

756 
zadd_int ~> of_nat_add 

757 
int_mult ~> of_nat_mult 

758 
int_Suc ~> of_nat_Suc 

759 
inj_int ~> inj_of_nat 

760 
int_1 ~> of_nat_1 

761 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

784 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  785 
realpow_minus_mult ~> power_minus_mult 
786 
realpow_Suc_le_self ~> power_Suc_le_self 

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

787 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  788 
INCOMPATIBILITY. 
789 

62479  790 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 
791 

62975
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62969
diff
changeset

792 
* In HOLProbability the type of emeasure and nn_integral was changed 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62969
diff
changeset

793 
from ereal to ennreal: 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62969
diff
changeset

794 
emeasure :: 'a measure => 'a set => ennreal 
1d066f6ab25d
Probability: move emeasure and nn_integral from ereal to ennreal
hoelzl
parents:
62969
diff
changeset

795 
nn_integral :: 'a measure => ('a => ennreal) => ennreal 
62976  796 
INCOMPATIBILITY. 
62327  797 

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

798 

62498  799 
*** ML *** 
800 

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

803 

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

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

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

808 
INCOMPATIBILITY. 

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

809 

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

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

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

817 

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

820 
requiring separate files. 

821 

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

823 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 
62851  824 

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

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

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

827 

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

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

831 
debugger information requires consirable time and space: main 

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

833 

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

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

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

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

839 
balanced blocks of Local_Theory.open_target versus 

840 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

841 

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

844 
INCOMPATIBILITY. 

845 

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

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

849 
File.full_path). Potential INCOMPATIBILITY. 

850 

63352  851 
* Binding.empty_atts supersedes Thm.empty_binding and 
852 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

853 

62498  854 

62354  855 
*** System *** 
856 

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

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

858 
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

859 
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

860 
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

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

862 

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

865 
"isabelle_scala_script". 

866 

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

869 
Isabelle_Tool.Body. 

870 

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

873 
particular: 

874 

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

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

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

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

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

879 

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

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

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

883 

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

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

885 
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

886 
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

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

888 

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

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

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

891 

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

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

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

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

895 

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

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

897 
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

898 
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

899 
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

900 
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

901 
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

902 
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

903 

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

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

908 

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

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

910 
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

911 
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

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

913 

62354  914 

915 

62031  916 
New in Isabelle2016 (February 2016) 
62016  917 
 
60138  918 

61337  919 
*** General *** 
920 

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

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

922 
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

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

924 
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

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

926 

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

929 

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

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

933 
has been removed (see below). 

934 

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

62017  937 

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

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

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

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

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

942 

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

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

944 
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

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

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

947 

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

950 
to update old sources. 

951 

61337  952 
* Toplevel theorem statements have been simplified as follows: 
953 

954 
theorems ~> lemmas 

955 
schematic_lemma ~> schematic_goal 

956 
schematic_theorem ~> schematic_goal 

957 
schematic_corollary ~> schematic_goal 

958 

959 
Commandline tool "isabelle update_theorems" updates theory sources 

960 
accordingly. 

961 

61338  962 
* Toplevel theorem statement 'proposition' is another alias for 
963 
'theorem'. 

964 

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

967 
deferred definitions require a surrounding 'overloading' block. 

968 

61337  969 

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

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

971 

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

975 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

979 
any effect on the running ML program. 

60984  980 

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

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

984 
update. 

61729  985 

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

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

988 
enable option "editor_output_state". 

61215  989 

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

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

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

994 
visibility. 

995 

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

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

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

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

1000 
panel. 

1001 

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

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

1003 
state output, interactive queries) wrt. longrunning background tasks. 
62017  1004 

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

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

1007 
implicit: a popup will show up unconditionally. 

1008 

1009 
* Additional abbreviations for syntactic completion may be specified in 

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

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

1012 

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

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

1014 
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

1015 
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

1016 
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

1017 

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

1020 
the editor. 

1021 

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

1023 
instead of former C+e LEFT. 

1024 

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

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

1027 
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

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

1029 

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

1032 
singleinstance applications seen on common GUI desktops. 

1033 

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

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

1035 
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

1036 
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

1037 

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

1040 

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

1043 

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

1044 

61405  1045 
*** Document preparation *** 
1046 

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

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

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

1049 

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

1052 

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

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

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

1056 

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

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

1059 
follows: 

1060 

1061 
\<^item> itemize 

1062 
\<^enum> enumerate 

1063 
\<^descr> description 

1064 

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

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

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

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

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

1071 

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

1074 
standard LaTeX macros of the same names. 

1075 

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

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

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

1080 
cartouche tokens seen in theory sources. 

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

1081 

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

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

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

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

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

1087 

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

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

1091 

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

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

1094 

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

1096 

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

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

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

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

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

1102 
documentation, with a hyperlink in the Prover IDE. 

1103 

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

1105 
entities of the Isar language. 

1106 

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

61488  1109 
print mode "HTML" loses its special meaning. 
61471  1110 

61405  1111 

60406  1112 
*** Isar *** 
1113 

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

1116 
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

1117 
example: 
60414  1118 

1119 
have result: "C x y" 

1120 
if "A x" and "B y" 

1121 
for x :: 'a and y :: 'a 

1122 
<proof> 

1123 

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

60414  1126 
corresponds to a raw proof block like this: 
1127 

1128 
{ 

1129 
fix x :: 'a and y :: 'a 

60449  1130 
assume that: "A x" "B y" 
60414  1131 
have "C x y" <proof> 
1132 
} 

1133 
note result = this 

60406  1134 

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

1135 
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

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

1137 

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

61658  1140 

1141 
assume result: "C x y" 

1142 
if "A x" and "B y" 

1143 
for x :: 'a and y :: 'a 

1144 

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

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

1147 

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

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

1150 
example: 

1151 

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

1153 

1154 
is equivalent to: 

1155 

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

1157 

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

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

60595  1162 

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

1164 

1165 
or: 

1166 

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

1168 

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

1170 

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

1172 

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

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

1176 
of the local context elements yet. 

1177 

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

1180 

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

1182 
then have something 

1183 
proof cases 

1184 
case a 

1185 
then show ?thesis <proof> 

1186 
next 

1187 
case b 

1188 
then show ?thesis <proof> 

1189 
next 

1190 
case c 

1191 
then show ?thesis <proof> 

1192 
qed 

1193 

60565  1194 
* Command 'case' allows fact name and attribute specification like this: 
1195 

1196 
case a: (c xs) 

1197 
case a [attributes]: (c xs) 

1198 

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

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

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

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

1203 
and always put attributes in front. 

1204 

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

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

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

1207 
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

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

1209 

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

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

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

1214 

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

1216 
supply [simp] = a 

1217 
proof 

1218 
show A by simp 

1219 
next 

1220 
show A by simp 

1221 
qed 

1222 

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

1224 
proof body as well, abstracted over relevant parameters. 

1225 

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

1227 
parameter scope for of each clause. 

1228 

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

1230 
statements: result is abstracted over unknowns. 

1231 

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

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

1235 
manual. 

1236 

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

1239 

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

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

1241 
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

1242 
example: 
60617  1243 

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

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

1246 
proof goal_cases 
60622  1247 
case (1 x) 
1248 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

1249 
next 

1250 
case (2 y z) 

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

1252 
qed 

1253 

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

1255 
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

1256 
proof goal_cases 
60617  1257 
case prems: 1 
1258 
then show ?case using prems sorry 

1259 
next 

1260 
case prems: 2 

1261 
then show ?case using prems sorry 

1262 
qed 

60578  1263 

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

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

60581  1268 

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

60551  1271 

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

1274 

60406  1275 

60331  1276 
*** Pure *** 
1277 

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

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

1279 
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

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

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

1282 

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

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

1285 

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

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

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

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

1293 
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

1294 

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

1295 
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

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

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

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

1299 

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

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

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

1302 
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

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

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

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

1306 

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

1309 

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

61675  1311 
'defines'. 
1312 

61895  1313 
* Command 'permanent_interpretation' has been discontinued. Use 
1314 
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. 

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

1315 

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

1318 

60331  1319 
* Configuration option rule_insts_schematic has been discontinued 
62017  1320 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 
60331  1321 

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

1324 
exploited. 

60347  1325 

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

62205  1327 
operations behave more similar to abbreviations. Potential 
60347  1328 
INCOMPATIBILITY in exotic situations. 
1329 

1330 

60171  1331 
*** HOL *** 
1332 

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

1335 
global collection of overloaded constant / type definitions into 

1336 
account. Type definitions with open dependencies on overloaded 

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

1338 
provides extra robustness in theory construction. Rare INCOMPATIBILITY. 

1339 

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

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

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

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

1344 
Option.is_none_def. Occasional INCOMPATIBILITY in applications. 

1345 

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

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

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

1349 
simplify porting old theories: 

1350 

1351 
notation iff (infixr "<>" 25) 

1352 

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

1354 

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

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

1357 