author  blanchet 
Mon, 12 Sep 2016 17:32:09 +0200  
changeset 63855  40f34614bd06 
parent 63830  2ea3725a34bd 
child 63871  f745c6e683b7 
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 

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

84 

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

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

88 

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

91 

92 
src/Pure/ROOT0.ML 

93 
src/Pure/ROOT.ML 

94 
src/Pure/Pure.thy 

95 
src/Pure/ML_Bootstrap.thy 

96 

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

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

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

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

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

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

63307  103 
dependencies of the above files are only observed for batch build. 
62904  104 

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

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

106 

63461  107 
* 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

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

109 
structure of theory specifications is treated as well. 
63461  110 

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

113 

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

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

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

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

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

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

119 
"jedit_indent_newline". 
63452  120 

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

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

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

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

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

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

126 

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

129 
systematic renaming. 

130 

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

133 
keymap; nonconflicting changes are always applied implicitly. This 

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

135 
increases chances that users see new keyboard shortcuts when reusing 

136 
old keymaps. 

137 

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

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

139 
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

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

141 

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

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

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

144 

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

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

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

147 

63581  148 
* Additional abbreviations for syntactic completion may be specified 
63579  149 
within the theory header as 'abbrevs', in addition to global 
63581  150 
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as 
151 
before. The theory syntax for 'keywords' has been simplified 

152 
accordingly: optional abbrevs need to go into the new 'abbrevs' section. 

63579  153 

63675  154 
* ML and document antiquotations for filesystems paths are more uniform 
155 
and diverse: 

156 

157 
@{path NAME}  no filesystem check 

158 
@{file NAME}  check for plain file 

159 
@{dir NAME}  check for directory 

160 

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

162 
have to be changed. 

63669  163 

164 

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

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

166 

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

169 

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

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

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

173 

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

176 
INCOMPATIBILITY. 

177 

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

180 
'definition', 'inductive', 'function'. 

181 

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

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

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

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

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

187 

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

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

63039  192 

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

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

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

195 

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

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

197 
typesetting. E.g. to produce proof holes in examples and documentation. 
62216  198 

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

201 

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

204 
definitions. 

205 

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

63259  208 

209 
(use facts in simp) 

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

211 

62216  212 

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

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

214 

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

217 
examples. 

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

218 

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

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

220 
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

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

222 

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

223 

62327  224 
*** HOL *** 
225 

63627  226 
* Renamed session HOLMultivariate_Analysis to HOLAnalysis. 
227 

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

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

230 
clashes. 

231 
INCOMPATIBILITY. 

232 

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

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

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

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

238 
INCOMPATIBILITY. 

63552  239 

240 
* Probability: Code generation and QuickCheck for Probability Mass 

241 
Functions. 

242 

63438  243 
* Theory Set_Interval.thy: substantial new theorems on indexed sums 
244 
and products. 

245 

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

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

249 

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

250 
* "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

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

252 

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

253 
* Theory Library/Combinator_PER.thy: combinator to build partial 
63378  254 
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

255 

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

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

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

258 

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

261 

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

264 
lifting_syntax begin ... end". Minor INCOMPATIBILITY. 

265 

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

268 

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

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

270 
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

271 
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

272 
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

273 
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

274 
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

275 
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

276 

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

279 

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

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

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

282 

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

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

284 
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

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

286 

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

289 
list in random order. 

290 

63246  291 
* Probability/SPMF formalises discrete subprobability distributions. 
292 

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

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

294 
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

295 
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

296 
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

297 

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

300 
element of the carrier set exactly once. 

301 

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

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

303 
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

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

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

306 

62522  307 
* New abbreviations for negated existence (but not bounded existence): 
308 

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

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

311 

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

314 
eliminated altogether. 

315 

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

318 

63116  319 
* Sledgehammer: 
63699  320 
 The MaSh relevance filter has been sped up. 
63116  321 
 Produce syntactically correct Vampire 4.0 problem files. 
322 

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

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

62842  327 
method. See 'isabelle doc corec'. 
62693  328 
 The predicator :: ('a => bool) => 'a F => bool is now a firstclass 
63855  329 
citizen in bounded natural functors. 
62693  330 
 'primrec' now allows nested calls through the predicator in addition 
62327  331 
to the map function. 
63855  332 
 'bnf' automatically discharges reflexive proof obligations. 
62693  333 
 'bnf' outputs a slightly modified proof obligation expressing rel in 
62332  334 
terms of map and set 
63855  335 
(not giving a specification for rel makes this one reflexive). 
62693  336 
 'bnf' outputs a new proof obligation expressing pred in terms of set 
63855  337 
(not giving a specification for pred makes this one reflexive). 
338 
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. 

62335  339 
 Renamed lemmas: 
340 
rel_prod_apply ~> rel_prod_inject 

341 
pred_prod_apply ~> pred_prod_inject 

342 
INCOMPATIBILITY. 

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

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

346 
INCOMPATIBILITY. 

62327  347 

63807  348 
* Some old / obsolete theorems have been renamed / removed, potential 
349 
INCOMPATIBILITY. 

350 

351 
nat_less_cases  removed, use linorder_cases instead 

352 
inv_image_comp  removed, use image_inv_f_f instead 

353 
image_surj_f_inv_f ~> image_f_inv_f 

63113  354 

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

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

356 
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

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

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

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

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

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

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

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

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

365 

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

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

367 
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

368 
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

369 
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

370 
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

371 
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

372 
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

373 
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

374 
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

375 
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

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

377 

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

62396  380 

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

383 

384 
 Logical representation: 

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

386 
* All other characters are represented as "Char n" 
62597  387 
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

388 
* Expressions of the form "Char n" with n greater than 255 
62597  389 
are noncanonical. 
390 
 Printing and parsing: 

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

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

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

62597  396 
is parsable for every numeral expression n. 
62598  397 
* Noncanonical characters have no special syntax and are 
62597  398 
printed as their logical representation. 
399 
 Explicit conversions from and to the natural numbers are 

400 
provided as char_of_nat, nat_of_char (as before). 

401 
 The auxiliary nibble type has been discontinued. 

402 

403 
INCOMPATIBILITY. 

404 

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

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

406 

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

407 
 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

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

409 

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

410 
 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

411 
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

412 

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

413 
 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

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

415 

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

416 
 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

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

418 

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

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

420 

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

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

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

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

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

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

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

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

428 
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

429 
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

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

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

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

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

434 
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

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

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

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

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

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

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

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

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

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

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

445 
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

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

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

448 

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

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

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

451 

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

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

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

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

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

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

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

458 

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

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

460 
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

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

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

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

464 

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

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

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

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

468 
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

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

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

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

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

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

474 
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

475 

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

476 
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

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

478 
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

479 
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

480 
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

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

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

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

484 
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

485 
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

486 
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

487 
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

488 
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

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

490 

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

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

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

493 

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

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

495 
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

496 
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

497 
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

498 
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

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

500 

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

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

502 
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

503 
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

504 
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

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

506 

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

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

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

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

510 

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

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

512 
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

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

514 

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

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

516 
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

517 
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

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

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

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

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

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

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

524 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

566 

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

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

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

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

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

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

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

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

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

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

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

577 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

600 

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

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

602 
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

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

604 

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

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

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

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

608 

63830  609 
* Renamed sums and products of multisets: 
610 
msetsum ~> sum_mset 

611 
msetprod ~> prod_mset 

612 

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

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

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

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

616 

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

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

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

619 

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

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

621 
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

622 

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

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

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

625 

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

628 

62345  629 
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. 
630 

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

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

632 
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

633 
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

634 
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

635 

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

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

637 

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

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

639 
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

640 
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

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

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

643 

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

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

645 

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

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

647 
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

648 
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

649 

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

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

651 
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

652 
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

653 
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

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

655 

63155  656 
* Library/Sublist.thy: added function "prefixes" and renamed 
63173  657 
prefixeq > prefix 
658 
prefix > strict_prefix 

659 
suffixeq > suffix 

660 
suffix > strict_suffix 

661 
Added theory of longest common prefixes. 

63117  662 

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

665 
lcm_left_commute_nat ~> lcm.left_commute 

666 
lcm_left_commute_int ~> lcm.left_commute 

667 
gcd_left_commute_nat ~> gcd.left_commute 

668 
gcd_left_commute_int ~> gcd.left_commute 

669 
gcd_greatest_iff_nat ~> gcd_greatest_iff 

670 
gcd_greatest_iff_int ~> gcd_greatest_iff 

671 
coprime_dvd_mult_nat ~> coprime_dvd_mult 

672 
coprime_dvd_mult_int ~> coprime_dvd_mult 

673 
zpower_numeral_even ~> power_numeral_even 

674 
gcd_mult_cancel_nat ~> gcd_mult_cancel 

675 
gcd_mult_cancel_int ~> gcd_mult_cancel 

676 
div_gcd_coprime_nat ~> div_gcd_coprime 

677 
div_gcd_coprime_int ~> div_gcd_coprime 

678 
zpower_numeral_odd ~> power_numeral_odd 

679 
zero_less_int_conv ~> of_nat_0_less_iff 

680 
gcd_greatest_nat ~> gcd_greatest 

681 
gcd_greatest_int ~> gcd_greatest 

682 
coprime_mult_nat ~> coprime_mult 

683 
coprime_mult_int ~> coprime_mult 

684 
lcm_commute_nat ~> lcm.commute 

685 
lcm_commute_int ~> lcm.commute 

686 
int_less_0_conv ~> of_nat_less_0_iff 

687 
gcd_commute_nat ~> gcd.commute 

688 
gcd_commute_int ~> gcd.commute 

689 
Gcd_insert_nat ~> Gcd_insert 

690 
Gcd_insert_int ~> Gcd_insert 

691 
of_int_int_eq ~> of_int_of_nat_eq 

692 
lcm_least_nat ~> lcm_least 

693 
lcm_least_int ~> lcm_least 

694 
lcm_assoc_nat ~> lcm.assoc 

695 
lcm_assoc_int ~> lcm.assoc 

696 
int_le_0_conv ~> of_nat_le_0_iff 

697 
int_eq_0_conv ~> of_nat_eq_0_iff 

698 
Gcd_empty_nat ~> Gcd_empty 

699 
Gcd_empty_int ~> Gcd_empty 

700 
gcd_assoc_nat ~> gcd.assoc 

701 
gcd_assoc_int ~> gcd.assoc 

702 
zero_zle_int ~> of_nat_0_le_iff 

703 
lcm_dvd2_nat ~> dvd_lcm2 

704 
lcm_dvd2_int ~> dvd_lcm2 

705 
lcm_dvd1_nat ~> dvd_lcm1 

706 
lcm_dvd1_int ~> dvd_lcm1 

707 
gcd_zero_nat ~> gcd_eq_0_iff 

708 
gcd_zero_int ~> gcd_eq_0_iff 

709 
gcd_dvd2_nat ~> gcd_dvd2 

710 
gcd_dvd2_int ~> gcd_dvd2 

711 
gcd_dvd1_nat ~> gcd_dvd1 

712 
gcd_dvd1_int ~> gcd_dvd1 

713 
int_numeral ~> of_nat_numeral 

714 
lcm_ac_nat ~> ac_simps 

715 
lcm_ac_int ~> ac_simps 

716 
gcd_ac_nat ~> ac_simps 

717 
gcd_ac_int ~> ac_simps 

718 
abs_int_eq ~> abs_of_nat 

719 
zless_int ~> of_nat_less_iff 

720 
zdiff_int ~> of_nat_diff 

721 
zadd_int ~> of_nat_add 

722 
int_mult ~> of_nat_mult 

723 
int_Suc ~> of_nat_Suc 

724 
inj_int ~> inj_of_nat 

725 
int_1 ~> of_nat_1 

726 
int_0 ~> of_nat_0 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

749 
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff 
62348  750 
realpow_minus_mult ~> power_minus_mult 
751 
realpow_Suc_le_self ~> power_Suc_le_self 

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

752 
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest 
62347  753 
INCOMPATIBILITY. 
754 

62479  755 
* Session HOLNSA has been renamed to HOLNonstandard_Analysis. 
756 

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

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

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

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

760 
nn_integral :: 'a measure => ('a => ennreal) => ennreal 
62976  761 
INCOMPATIBILITY. 
62327  762 

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

763 

62498  764 
*** ML *** 
765 

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

768 

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

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

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

773 
INCOMPATIBILITY. 

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

774 

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

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

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

782 

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

785 
requiring separate files. 

786 

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

788 
exposed to Isabelle/ML userspace. Potential INCOMPATIBILITY. 
62851  789 

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

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

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

792 

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

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

796 
debugger information requires consirable time and space: main 

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

798 

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

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

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

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

804 
balanced blocks of Local_Theory.open_target versus 

805 
Local_Theory.close_target instead. Rare INCOMPATIBILITY. 

806 

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

809 
INCOMPATIBILITY. 

810 

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

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

814 
File.full_path). Potential INCOMPATIBILITY. 

815 

63352  816 
* Binding.empty_atts supersedes Thm.empty_binding and 
817 
Attrib.empty_binding. Minor INCOMPATIBILITY. 

818 

62498  819 

62354  820 
*** System *** 
821 

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

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

823 
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

824 
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

825 
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

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

827 

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

830 
"isabelle_scala_script". 

831 

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

834 
Isabelle_Tool.Body. 

835 

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

838 
particular: 

839 

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

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

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

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

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

844 

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

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

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

848 

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

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

850 
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

851 
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

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

853 

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

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

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

856 

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

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

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

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

860 

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

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

862 
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

863 
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

864 
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

865 
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

866 
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

867 
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

868 

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

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

873 

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

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

875 
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

876 
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

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

878 

62354  879 

880 

62031  881 
New in Isabelle2016 (February 2016) 
62016  882 
 
60138  883 

61337  884 
*** General *** 
885 

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

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

887 
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

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

889 
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

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

891 

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

894 

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

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

898 
has been removed (see below). 

899 

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

62017  902 

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

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

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

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

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

907 

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

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

909 
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

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

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

912 

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

915 
to update old sources. 

916 

61337  917 
* Toplevel theorem statements have been simplified as follows: 
918 

919 
theorems ~> lemmas 

920 
schematic_lemma ~> schematic_goal 

921 
schematic_theorem ~> schematic_goal 

922 
schematic_corollary ~> schematic_goal 

923 

924 
Commandline tool "isabelle update_theorems" updates theory sources 

925 
accordingly. 

926 

61338  927 
* Toplevel theorem statement 'proposition' is another alias for 
928 
'theorem'. 

929 

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

932 
deferred definitions require a surrounding 'overloading' block. 

933 

61337  934 

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

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

936 

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

940 
'SML_file_no_debug' control compilation of sources with or without 

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

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

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

944 
any effect on the running ML program. 

60984  945 

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

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

949 
update. 

61729  950 

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

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

953 
enable option "editor_output_state". 

61215  954 

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

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

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

959 
visibility. 

960 

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

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

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

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

965 
panel. 

966 

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

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

968 
state output, interactive queries) wrt. longrunning background tasks. 
62017  969 

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

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

972 
implicit: a popup will show up unconditionally. 

973 

974 
* Additional abbreviations for syntactic completion may be specified in 

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

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

977 

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

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

979 
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

980 
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

981 
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

982 

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

985 
the editor. 

986 

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

988 
instead of former C+e LEFT. 

989 

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

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

992 
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

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

994 

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

997 
singleinstance applications seen on common GUI desktops. 

998 

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

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

1000 
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

1001 
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

1002 

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

1005 

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

1008 

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

1009 

61405  1010 
*** Document preparation *** 
1011 

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

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

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

1014 

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

1017 

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

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

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

1021 

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

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

1024 
follows: 

1025 

1026 
\<^item> itemize 

1027 
\<^enum> enumerate 

1028 
\<^descr> description 

1029 

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

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

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

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

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

1036 

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

1039 
standard LaTeX macros of the same names. 

1040 

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

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

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

1045 
cartouche tokens seen in theory sources. 

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

1046 

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

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

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

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

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

1052 

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

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

1056 

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

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

1059 

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

1061 

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

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

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

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

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

1067 
documentation, with a hyperlink in the Prover IDE. 

1068 

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

1070 
entities of the Isar language. 

1071 

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

61488  1074 
print mode "HTML" loses its special meaning. 
61471  1075 

61405  1076 

60406  1077 
*** Isar *** 
1078 

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

1081 
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

1082 
example: 
60414  1083 

1084 
have result: "C x y" 

1085 
if "A x" and "B y" 

1086 
for x :: 'a and y :: 'a 

1087 
<proof> 

1088 

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

60414  1091 
corresponds to a raw proof block like this: 
1092 

1093 
{ 

1094 
fix x :: 'a and y :: 'a 

60449  1095 
assume that: "A x" "B y" 
60414  1096 
have "C x y" <proof> 
1097 
} 

1098 
note result = this 

60406  1099 

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

1100 
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

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

1102 

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

61658  1105 

1106 
assume result: "C x y" 

1107 
if "A x" and "B y" 

1108 
for x :: 'a and y :: 'a 

1109 

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

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

1112 

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

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

1115 
example: 

1116 

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

1118 

1119 
is equivalent to: 

1120 

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

1122 

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

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

60595  1127 

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

1129 

1130 
or: 

1131 

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

1133 

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

1135 

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

1137 

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

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

1141 
of the local context elements yet. 

1142 

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

1145 

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

1147 
then have something 

1148 
proof cases 

1149 
case a 

1150 
then show ?thesis <proof> 

1151 
next 

1152 
case b 

1153 
then show ?thesis <proof> 

1154 
next 

1155 
case c 

1156 
then show ?thesis <proof> 

1157 
qed 

1158 

60565  1159 
* Command 'case' allows fact name and attribute specification like this: 
1160 

1161 
case a: (c xs) 

1162 
case a [attributes]: (c xs) 

1163 

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

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

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

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

1168 
and always put attributes in front. 

1169 

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

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

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

1172 
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

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

1174 

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

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

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

1179 

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

1181 
supply [simp] = a 

1182 
proof 

1183 
show A by simp 

1184 
next 

1185 
show A by simp 

1186 
qed 

1187 

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

1189 
proof body as well, abstracted over relevant parameters. 

1190 

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

1192 
parameter scope for of each clause. 

1193 

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

1195 
statements: result is abstracted over unknowns. 

1196 

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

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

1200 
manual. 

1201 

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

1204 

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

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

1206 
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

1207 
example: 
60617  1208 

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

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

1211 
proof goal_cases 
60622  1212 
case (1 x) 
1213 
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry 

1214 
next 

1215 
case (2 y z) 

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

1217 
qed 

1218 

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

1220 
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

1221 
proof goal_cases 
60617  1222 
case prems: 1 
1223 
then show ?case using prems sorry 

1224 
next 

1225 
case prems: 2 

1226 
then show ?case using prems sorry 

1227 
qed 

60578  1228 

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

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

60581  1233 

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

60551  1236 

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

1239 

60406  1240 

60331  1241 
*** Pure *** 
1242 

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

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

1244 
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

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

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

1247 

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

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

1250 

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

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

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

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

1258 
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

1259 

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

1260 
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

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

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

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

1264 

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

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

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

1267 
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

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

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

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

1271 

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

1274 

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

61675  1276 
'defines'. 
1277 

61895  1278 
* Command 'permanent_interpretation' has been discontinued. Use 
1279 
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. 

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

1280 

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

1283 

60331  1284 
* Configuration option rule_insts_schematic has been discontinued 
62017  1285 
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. 
60331  1286 

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

1289 
exploited. 

60347  1290 

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

62205  1292 
operations behave more similar to abbreviations. Potential 
60347  1293 
INCOMPATIBILITY in exotic situations. 
1294 

1295 

60171  1296 
*** HOL *** 
1297 

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

1300 
global collection of overloaded constant / type definitions into 

1301 
account. Type definitions with open dependencies on overloaded 

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

1303 
provides extra robustness in theory construction. Rare INCOMPATIBILITY. 

1304 

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

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

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

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

1309 
Option.is_none_def. Occasional INCOMPATIBILITY in applications. 

1310 

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

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

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

1314 
simplify porting old theories: 

1315 

1316 
notation iff (infixr "<>" 25) 

1317 

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

1319 

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

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

1322 

1323 
type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) 

1324 

1325 
notation FuncSet.funcset (infixr ">" 60) 

1326 
notation FuncSet.extensional_funcset (infixr ">\<^sub>E" 60) 

1327 

1328 
notation Omega_Words_Fun.conc (infixr "conc" 65) 

1329 

1330 
notation Preorder.equiv ("op ~~") 

1331 
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) 

1332 

1333 
notation (in topological_space) tendsto (infixr ">" 55) 

1334 
notation (in topological_space) LIMSEQ ("((_)/ > (_))" [60, 60] 60) 

1335 
notation LIM ("((_)/  (_)/ > (_))" [60, 0, 60] 60) 

1336 

1337 
notation NSA.approx (infixl "@=" 50) 

1338 
notation NSLIMSEQ ("((_)/ NS> (_))" [60, 60] 60) 

1339 
notation NSLIM ("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) 

1340 

1341 
* The alternative notation "\<Colon>" for type and sort constraints has been 

1342 
removed: in LaTeX document output it looks the same as "::". 

1343 
INCOMPATIBILITY, use plain "::" instead. 

1344 

1345 
* Commands 'inductive' and 'inductive_set' work better when names for 

1346 
intro rules are omitted: the "cases" and "induct" rules no longer 

1347 
declare empty case_names, but no case_names at all. This allows to use 

1348 
numbered cases in proofs, without requiring method "goal_cases". 

1349 

1350 
* Inductive definitions ('inductive', 'coinductive', etc.) expose 

1351 
lowlevel facts of the internal construction only if the option 

62093  1352 
"inductive_internals" is enabled. This refers to the internal predicate 
62017  1353 
definition and its monotonicity result. Rare INCOMPATIBILITY. 
1354 

1355 
* Recursive function definitions ('fun', 'function', 'partial_function') 

1356 
expose lowlevel facts of the internal construction only if the option 

62205  1357 
"function_internals" is enabled. Its internal inductive definition is 
1358 
also subject to "inductive_internals". Rare INCOMPATIBILITY. 

62093  1359 

1360 
* BNF datatypes ('datatype', 'codat 