author | paulson <lp15@cam.ac.uk> |
Fri, 30 Sep 2016 14:05:51 +0100 | |
changeset 63967 | 2aa42596edc3 |
parent 63963 | ed98a055b9a5 |
child 63977 | ec0fb01c6d50 |
permissions | -rw-r--r-- |
57491 | 1 |
Isabelle NEWS -- history of user-relevant 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 tree-view 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 old-fashioned |
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
63113
diff
changeset
|
14 |
quotes when sub-languages 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 |
* Type-inference 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 object-logic, 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 |
|
63933 | 33 |
* Mixfix annotations support delimiters like \<^control>\<open>cartouche\<close> -- |
34 |
this allows special forms of document output. |
|
35 |
||
63935
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63933
diff
changeset
|
36 |
* Raw LaTeX output now works via \<^latex>\<open>...\<close> instead of raw control |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63933
diff
changeset
|
37 |
symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63933
diff
changeset
|
38 |
derivatives. |
aa1fe1103ab8
raw control symbols are superseded by Latex.embed_raw;
wenzelm
parents:
63933
diff
changeset
|
39 |
|
63936 | 40 |
* \<^raw:...> symbols are no longer supported. |
41 |
||
62440 | 42 |
* New symbol \<circle>, e.g. for temporal operator. |
43 |
||
62453 | 44 |
* Old 'header' command is no longer supported (legacy since |
45 |
Isabelle2015). |
|
46 |
||
63273 | 47 |
* Command 'bundle' provides a local theory target to define a bundle |
48 |
from the body of specification commands (such as 'declare', |
|
49 |
'declaration', 'notation', 'lemmas', 'lemma'). For example: |
|
50 |
||
51 |
bundle foo |
|
52 |
begin |
|
53 |
declare a [simp] |
|
54 |
declare b [intro] |
|
55 |
end |
|
63272 | 56 |
|
63282 | 57 |
* Command 'unbundle' is like 'include', but works within a local theory |
58 |
context. Unlike "context includes ... begin", the effect of 'unbundle' |
|
59 |
on the target context persists, until different declarations are given. |
|
60 |
||
63650 | 61 |
* Splitter in simp, auto and friends: |
62 |
- The syntax "split add" has been discontinued, use plain "split". |
|
63656 | 63 |
- For situations with many conditional or case expressions, |
63650 | 64 |
there is an alternative splitting strategy that can be much faster. |
65 |
It is selected by writing "split!" instead of "split". It applies |
|
66 |
safe introduction and elimination rules after each split rule. |
|
67 |
As a result the subgoal may be split into several subgoals. |
|
68 |
||
63383 | 69 |
* Proof method "blast" is more robust wrt. corner cases of Pure |
70 |
statements without object-logic judgment. |
|
71 |
||
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63528
diff
changeset
|
72 |
* Pure provides basic versions of proof methods "simp" and "simp_all" |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63528
diff
changeset
|
73 |
that only know about meta-equality (==). Potential INCOMPATIBILITY in |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63528
diff
changeset
|
74 |
theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63528
diff
changeset
|
75 |
is relevant to avoid confusion of Pure.simp vs. HOL.simp. |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63528
diff
changeset
|
76 |
|
63624
994d1a1105ef
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
wenzelm
parents:
63610
diff
changeset
|
77 |
* Commands 'prf' and 'full_prf' are somewhat more informative (again): |
63821 | 78 |
proof terms are reconstructed and cleaned from administrative thm |
79 |
nodes. |
|
80 |
||
81 |
* The command 'unfolding' and proof method "unfold" include a second |
|
82 |
stage where given equations are passed through the attribute "abs_def" |
|
83 |
before rewriting. This ensures that definitions are fully expanded, |
|
84 |
regardless of the actual parameters that are provided. Rare |
|
85 |
INCOMPATIBILITY in some corner cases: use proof method (simp only:) |
|
86 |
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
|
87 |
|
62440 | 88 |
|
62904 | 89 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
90 |
||
63875 | 91 |
* Dockable window "Symbols" also provides access to 'abbrevs' from the |
92 |
outer syntax of the current theory buffer. This provides clickable |
|
93 |
syntax templates, including entries with empty abbrevs name (which are |
|
94 |
inaccessible via keyboard completion). |
|
95 |
||
63135 | 96 |
* Cartouche abbreviations work both for " and ` to accomodate typical |
97 |
situations where old ASCII notation may be updated. |
|
98 |
||
63610 | 99 |
* Isabelle/ML and Standard ML files are presented in Sidekick with the |
100 |
tree structure of section headings: this special comment format is |
|
101 |
described in "implementation" chapter 0, e.g. (*** section ***). |
|
102 |
||
63022 | 103 |
* IDE support for the Isabelle/Pure bootstrap process, with the |
104 |
following independent stages: |
|
105 |
||
106 |
src/Pure/ROOT0.ML |
|
107 |
src/Pure/ROOT.ML |
|
108 |
src/Pure/Pure.thy |
|
109 |
src/Pure/ML_Bootstrap.thy |
|
110 |
||
111 |
The ML ROOT files act like quasi-theories in the context of theory |
|
112 |
ML_Bootstrap: this allows continuous checking of all loaded ML files. |
|
113 |
The theory files are presented with a modified header to import Pure |
|
114 |
from the running Isabelle instance. Results from changed versions of |
|
115 |
each stage are *not* propagated to the next stage, and isolated from the |
|
116 |
actual Isabelle/Pure that runs the IDE itself. The sequential |
|
63307 | 117 |
dependencies of the above files are only observed for batch build. |
62904 | 118 |
|
62987
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62969
diff
changeset
|
119 |
* Highlighting of entity def/ref positions wrt. cursor. |
dc8a8a7559e7
highlighting of entity def/ref positions wrt. cursor;
wenzelm
parents:
62969
diff
changeset
|
120 |
|
63461 | 121 |
* 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
|
122 |
are treated as delimiters for fold structure; 'begin' and 'end' |
64db21931bcb
include 'begin' and 'end' structure in text folds;
wenzelm
parents:
63581
diff
changeset
|
123 |
structure of theory specifications is treated as well. |
63461 | 124 |
|
63608 | 125 |
* Sidekick parser "isabelle-context" shows nesting of context blocks |
126 |
according to 'begin' and 'end' structure. |
|
127 |
||
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
128 |
* Syntactic indentation according to Isabelle outer syntax. Action |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
129 |
"indent-lines" (shortcut C+i) indents the current line according to |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
130 |
command keywords and some command substructure. Action |
63455
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset
|
131 |
"isabelle.newline" (shortcut ENTER) indents the old and the new line |
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset
|
132 |
according to command keywords only; see also option |
019856db2bb6
added action "isabelle.newline" (shortcut ENTER);
wenzelm
parents:
63453
diff
changeset
|
133 |
"jedit_indent_newline". |
63452 | 134 |
|
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
135 |
* Semantic indentation for unstructured proof scripts ('apply' etc.) via |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
136 |
number of subgoals. This requires information of ongoing document |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
137 |
processing and may thus lag behind, when the user is editing too |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
138 |
quickly; see also option "jedit_script_indent" and |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
139 |
"jedit_script_indent_limit". |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63463
diff
changeset
|
140 |
|
63236 | 141 |
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all |
142 |
occurences of the formal entity at the caret position. This facilitates |
|
143 |
systematic renaming. |
|
144 |
||
63751 | 145 |
* Action "isabelle.keymap-merge" asks the user to resolve pending |
146 |
Isabelle keymap changes that are in conflict with the current jEdit |
|
147 |
keymap; non-conflicting changes are always applied implicitly. This |
|
148 |
action is automatically invoked on Isabelle/jEdit startup and thus |
|
149 |
increases chances that users see new keyboard shortcuts when re-using |
|
150 |
old keymaps. |
|
151 |
||
63032
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset
|
152 |
* 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
|
153 |
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
|
154 |
statement. |
e0fa59bbc956
reactivated other_id reports (see also db929027e701, 8eda56033203);
wenzelm
parents:
63022
diff
changeset
|
155 |
|
63513
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset
|
156 |
* Command 'proof' provides information about proof outline with cases, |
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset
|
157 |
e.g. for proof methods "cases", "induct", "goal_cases". |
9f8d06f23c09
information about proof outline with cases (sendback);
wenzelm
parents:
63474
diff
changeset
|
158 |
|
63528
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset
|
159 |
* Completion templates for commands involving "begin ... end" blocks, |
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset
|
160 |
e.g. 'context', 'notepad'. |
0f39f59317c1
completion templates for commands involving "begin ... end" blocks;
wenzelm
parents:
63527
diff
changeset
|
161 |
|
63581 | 162 |
* Additional abbreviations for syntactic completion may be specified |
63871 | 163 |
within the theory header as 'abbrevs'. The theory syntax for 'keywords' |
164 |
has been simplified accordingly: optional abbrevs need to go into the |
|
165 |
new 'abbrevs' section. |
|
166 |
||
167 |
* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and |
|
168 |
$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor |
|
169 |
INCOMPATIBILITY, use 'abbrevs' within theory header instead. |
|
63579 | 170 |
|
63675 | 171 |
* ML and document antiquotations for file-systems paths are more uniform |
172 |
and diverse: |
|
173 |
||
174 |
@{path NAME} -- no file-system check |
|
175 |
@{file NAME} -- check for plain file |
|
176 |
@{dir NAME} -- check for directory |
|
177 |
||
178 |
Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may |
|
179 |
have to be changed. |
|
63669 | 180 |
|
181 |
||
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
182 |
*** Isar *** |
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
183 |
|
63383 | 184 |
* The defining position of a literal fact \<open>prop\<close> is maintained more |
185 |
carefully, and made accessible as hyperlink in the Prover IDE. |
|
186 |
||
187 |
* Commands 'finally' and 'ultimately' used to expose the result as |
|
188 |
literal fact: this accidental behaviour has been discontinued. Rare |
|
189 |
INCOMPATIBILITY, use more explicit means to refer to facts in Isar. |
|
190 |
||
63178 | 191 |
* Command 'axiomatization' has become more restrictive to correspond |
192 |
better to internal axioms as singleton facts with mandatory name. Minor |
|
193 |
INCOMPATIBILITY. |
|
194 |
||
63180 | 195 |
* Many specification elements support structured statements with 'if' / |
196 |
'for' eigen-context, e.g. 'axiomatization', 'abbreviation', |
|
197 |
'definition', 'inductive', 'function'. |
|
198 |
||
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
199 |
* Toplevel theorem statements support eigen-context notation with 'if' / |
63284 | 200 |
'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the |
63094
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
201 |
traditional long statement form (in prefix). Local premises are called |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
202 |
"that" or "assms", respectively. Empty premises are *not* bound in the |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
203 |
context: INCOMPATIBILITY. |
056ea294c256
toplevel theorem statements support 'if'/'for' eigen-context;
wenzelm
parents:
63078
diff
changeset
|
204 |
|
63039 | 205 |
* Command 'define' introduces a local (non-polymorphic) definition, with |
206 |
optional abstraction over local parameters. The syntax resembles |
|
63043 | 207 |
'definition' and 'obtain'. It fits better into the Isar language than |
208 |
old 'def', which is now a legacy feature. |
|
63039 | 209 |
|
63059
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
210 |
* Command 'obtain' supports structured statements with 'if' / 'for' |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
211 |
context. |
3f577308551e
'obtain' supports structured statements (similar to 'define');
wenzelm
parents:
63043
diff
changeset
|
212 |
|
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
213 |
* 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
|
214 |
typesetting. E.g. to produce proof holes in examples and documentation. |
62216 | 215 |
|
62939 | 216 |
* The old proof method "default" has been removed (legacy since |
217 |
Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
|
218 |
||
63259 | 219 |
* Proof methods may refer to the main facts via the dynamic fact |
220 |
"method_facts". This is particularly useful for Eisbach method |
|
221 |
definitions. |
|
222 |
||
63527 | 223 |
* Proof method "use" allows to modify the main facts of a given method |
224 |
expression, e.g. |
|
63259 | 225 |
|
226 |
(use facts in simp) |
|
227 |
(use facts in \<open>simp add: ...\<close>) |
|
228 |
||
62216 | 229 |
|
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset
|
230 |
*** Pure *** |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset
|
231 |
|
63166 | 232 |
* Code generator: config option "code_timing" triggers measurements of |
233 |
different phases of code generation. See src/HOL/ex/Code_Timing.thy for |
|
234 |
examples. |
|
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset
|
235 |
|
63350
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset
|
236 |
* 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
|
237 |
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
|
238 |
some situations where ambiguities may occur. |
705229ed856e
compiling implicit instances into companion objects for classes avoids ambiguities
haftmann
parents:
63343
diff
changeset
|
239 |
|
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63161
diff
changeset
|
240 |
|
62327 | 241 |
*** HOL *** |
242 |
||
63963 | 243 |
* New proof method "argo" using the built-in Argo solver based on SMT technology. |
244 |
The method can be used to prove goals of quantifier-free propositional logic, |
|
245 |
goals based on a combination of quantifier-free propositional logic with equality, |
|
246 |
and goals based on a combination of quantifier-free propositional logic with |
|
247 |
linear real arithmetic including min/max/abs. See HOL/ex/Argo_Examples.thy for |
|
248 |
examples. |
|
249 |
||
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63946
diff
changeset
|
250 |
* Type class "div" with operation "mod" renamed to type class "modulo" with |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63946
diff
changeset
|
251 |
operation "modulo", analogously to type class "divide". This eliminates the |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63946
diff
changeset
|
252 |
need to qualify any of those names in the presence of infix "mod" syntax. |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63946
diff
changeset
|
253 |
INCOMPATIBILITY. |
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
63946
diff
changeset
|
254 |
|
63909 | 255 |
* The unique existence quantifier no longer provides 'binder' syntax, |
256 |
but uses syntax translations (as for bounded unique existence). Thus |
|
257 |
iterated quantification \<exists>!x y. P x y with its slightly confusing |
|
258 |
sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead, |
|
259 |
pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y |
|
63917 | 260 |
(analogous to existing notation \<exists>!(x, y)\<in>A. P x y). Potential |
63909 | 261 |
INCOMPATIBILITY in rare situations. |
262 |
||
63627 | 263 |
* Renamed session HOL-Multivariate_Analysis to HOL-Analysis. |
264 |
||
265 |
* Moved measure theory from HOL-Probability to HOL-Analysis. When importing |
|
266 |
HOL-Analysis some theorems need additional name spaces prefixes due to name |
|
267 |
clashes. |
|
268 |
INCOMPATIBILITY. |
|
269 |
||
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
270 |
* In HOL-Probability the type of emeasure and nn_integral was changed |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
271 |
from ereal to ennreal: |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
272 |
emeasure :: 'a measure => 'a set => ennreal |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
273 |
nn_integral :: 'a measure => ('a => ennreal) => ennreal |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
274 |
INCOMPATIBILITY. |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
275 |
|
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
276 |
* HOL-Analysis: more complex analysis including Cauchy's inequality, Liouville theorem, |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
277 |
open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma. |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
278 |
|
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
279 |
* HOL-Analysis: Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
280 |
Minkowski theorem. |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
281 |
|
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
282 |
* HOL-Analysis: Numerous results ported from the HOL Light libraries: homeomorphisms, |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
283 |
continuous function extensions and other advanced topics in topology |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
284 |
|
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
285 |
* Number_Theory: algebraic foundation for primes: Generalisation of |
63635 | 286 |
predicate "prime" and introduction of predicates "prime_elem", |
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
287 |
"irreducible", a "prime_factorization" function, and the "factorial_ring" |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
288 |
typeclass with instance proofs for nat, int, poly. Some theorems now have |
63635 | 289 |
different names, most notably "prime_def" is now "prime_nat_iff". |
290 |
INCOMPATIBILITY. |
|
63552 | 291 |
|
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
292 |
* Probability: Code generation and QuickCheck for Probability Mass |
63552 | 293 |
Functions. |
294 |
||
63438 | 295 |
* Theory Set_Interval.thy: substantial new theorems on indexed sums |
296 |
and products. |
|
297 |
||
63882
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset
|
298 |
* Theory List.thy: |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset
|
299 |
listsum ~> sum_list |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset
|
300 |
listprod ~> prod_list |
018998c00003
renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents:
63875
diff
changeset
|
301 |
|
63414 | 302 |
* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying |
303 |
equations in functional programming style: variables present on the |
|
304 |
left-hand but not on the righ-hand side are replaced by underscores. |
|
305 |
||
63416
6af79184bef3
avoid to hide equality behind (output) abbreviation
haftmann
parents:
63414
diff
changeset
|
306 |
* "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
|
307 |
term output. Minor INCOMPATIBILITY. |
6af79184bef3
avoid to hide equality behind (output) abbreviation
haftmann
parents:
63414
diff
changeset
|
308 |
|
63377
64adf4ba9526
combinator to build partial equivalence relations from a predicate and an equivalenc relation
haftmann
parents:
63375
diff
changeset
|
309 |
* Theory Library/Combinator_PER.thy: combinator to build partial |
63378 | 310 |
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
|
311 |
|
63375
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset
|
312 |
* Theory Library/Perm.thy: basic facts about almost everywhere fix |
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset
|
313 |
bijections. |
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63374
diff
changeset
|
314 |
|
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
315 |
* Theory Library/Normalized_Fraction.thy: allows viewing an element |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
316 |
of a field of fractions as a normalized fraction (i.e. a pair of |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
317 |
numerator and denominator such that the two are coprime and the |
63923 | 318 |
denominator is normalized w.r.t. unit factors) |
319 |
||
63374 | 320 |
* Locale bijection establishes convenient default simp rules |
321 |
like "inv f (f a) = a" for total bijections. |
|
322 |
||
63343 | 323 |
* Former locale lifting_syntax is now a bundle, which is easier to |
324 |
include in a local context or theorem statement, e.g. "context includes |
|
325 |
lifting_syntax begin ... end". Minor INCOMPATIBILITY. |
|
326 |
||
63303 | 327 |
* Code generation for scala: ambiguous implicts in class diagrams |
328 |
are spelt out explicitly. |
|
329 |
||
63290
9ac558ab0906
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
haftmann
parents:
63284
diff
changeset
|
330 |
* 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
|
331 |
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
|
332 |
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
|
333 |
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
|
334 |
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
|
335 |
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
|
336 |
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
|
337 |
|
63237 | 338 |
* Conventional syntax "%(). t" for unit abstractions. Slight syntactic |
339 |
INCOMPATIBILITY. |
|
340 |
||
63174
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset
|
341 |
* Command 'code_reflect' accepts empty constructor lists for datatypes, |
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset
|
342 |
which renders those abstract effectively. |
57c0d60e491c
do not export abstract constructors in code_reflect
haftmann
parents:
63173
diff
changeset
|
343 |
|
63175
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset
|
344 |
* 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
|
345 |
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
|
346 |
generated code. |
d191892b1c23
explicit check that abstract constructors cannot be part of official interface
haftmann
parents:
63174
diff
changeset
|
347 |
|
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
348 |
* Probability/Random_Permutations.thy contains some theory about |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
349 |
choosing a permutation of a set uniformly at random and folding over a |
63144 | 350 |
list in random order. |
351 |
||
63246 | 352 |
* Probability/SPMF formalises discrete subprobability distributions. |
353 |
||
63283
a59801b7f125
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
wenzelm
parents:
63282
diff
changeset
|
354 |
* 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
|
355 |
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
|
356 |
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
|
357 |
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
|
358 |
|
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
359 |
* Library/Set_Permutations.thy (executably) defines the set of |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
360 |
permutations of a set, i.e. the set of all lists that contain every |
63144 | 361 |
element of the carrier set exactly once. |
362 |
||
63161
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
63155
diff
changeset
|
363 |
* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
63155
diff
changeset
|
364 |
explicitly provided auxiliary definitions for required type class |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
63155
diff
changeset
|
365 |
dictionaries rather than half-working magic. INCOMPATIBILITY, see |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
63155
diff
changeset
|
366 |
the tutorial on code generation for details. |
2660ba498798
delegate inclusion of required dictionaries to user-space instead of half-working magic
haftmann
parents:
63155
diff
changeset
|
367 |
|
62522 | 368 |
* New abbreviations for negated existence (but not bounded existence): |
369 |
||
370 |
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
|
371 |
\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
|
372 |
||
62521 | 373 |
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
374 |
has been removed for output. It is retained for input only, until it is |
|
375 |
eliminated altogether. |
|
376 |
||
63785 | 377 |
* metis: The problem encoding has changed very slightly. This might |
378 |
break existing proofs. INCOMPATIBILITY. |
|
379 |
||
63116 | 380 |
* Sledgehammer: |
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
381 |
- The MaSh relevance filter is now faster than before. |
63116 | 382 |
- Produce syntactically correct Vampire 4.0 problem files. |
383 |
||
63891 | 384 |
* The 'coinductive' command produces a proper coinduction rule for |
385 |
mutual coinductive predicates. This new rule replaces the old rule, |
|
386 |
which exposed details of the internal fixpoint construction and was |
|
387 |
hard to use. INCOMPATIBILITY. |
|
388 |
||
62327 | 389 |
* (Co)datatype package: |
62693 | 390 |
- New commands for defining corecursive functions and reasoning about |
391 |
them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive', |
|
392 |
'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof |
|
62842 | 393 |
method. See 'isabelle doc corec'. |
62693 | 394 |
- The predicator :: ('a => bool) => 'a F => bool is now a first-class |
63855 | 395 |
citizen in bounded natural functors. |
62693 | 396 |
- 'primrec' now allows nested calls through the predicator in addition |
62327 | 397 |
to the map function. |
63855 | 398 |
- 'bnf' automatically discharges reflexive proof obligations. |
62693 | 399 |
- 'bnf' outputs a slightly modified proof obligation expressing rel in |
62332 | 400 |
terms of map and set |
63855 | 401 |
(not giving a specification for rel makes this one reflexive). |
62693 | 402 |
- 'bnf' outputs a new proof obligation expressing pred in terms of set |
63855 | 403 |
(not giving a specification for pred makes this one reflexive). |
404 |
INCOMPATIBILITY: manual 'bnf' declarations may need adjustment. |
|
62335 | 405 |
- Renamed lemmas: |
406 |
rel_prod_apply ~> rel_prod_inject |
|
407 |
pred_prod_apply ~> pred_prod_inject |
|
408 |
INCOMPATIBILITY. |
|
62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
62525
diff
changeset
|
409 |
- The "size" plugin has been made compatible again with locales. |
63855 | 410 |
- The theorems about "rel" and "set" may have a slightly different (but |
411 |
equivalent) form. |
|
412 |
INCOMPATIBILITY. |
|
62327 | 413 |
|
63807 | 414 |
* Some old / obsolete theorems have been renamed / removed, potential |
415 |
INCOMPATIBILITY. |
|
416 |
||
417 |
nat_less_cases -- removed, use linorder_cases instead |
|
418 |
inv_image_comp -- removed, use image_inv_f_f instead |
|
419 |
image_surj_f_inv_f ~> image_f_inv_f |
|
63113 | 420 |
|
63456
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
421 |
* Some theorems about groups and orders have been generalised from |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
422 |
groups to semi-groups that are also monoids: |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
423 |
le_add_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
424 |
le_add_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
425 |
less_add_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
426 |
less_add_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
427 |
add_le_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
428 |
add_le_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
429 |
add_less_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
430 |
add_less_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
431 |
|
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
432 |
* Some simplifications theorems about rings have been removed, since |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
433 |
superseeded by a more general version: |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
434 |
less_add_cancel_left_greater_zero ~> less_add_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
435 |
less_add_cancel_right_greater_zero ~> less_add_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
436 |
less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
437 |
less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
438 |
less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
439 |
less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
440 |
less_add_cancel_left_less_zero ~> add_less_same_cancel1 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
441 |
less_add_cancel_right_less_zero ~> add_less_same_cancel2 |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
442 |
INCOMPATIBILITY. |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
443 |
|
62407 | 444 |
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to |
445 |
resemble the f.split naming convention, INCOMPATIBILITY. |
|
62396 | 446 |
|
62597 | 447 |
* Characters (type char) are modelled as finite algebraic type |
448 |
corresponding to {0..255}. |
|
449 |
||
450 |
- Logical representation: |
|
451 |
* 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
|
452 |
* All other characters are represented as "Char n" |
62597 | 453 |
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
|
454 |
* Expressions of the form "Char n" with n greater than 255 |
62597 | 455 |
are non-canonical. |
456 |
- Printing and parsing: |
|
62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset
|
457 |
* Printable characters are printed and parsed as "CHR ''\<dots>''" |
62597 | 458 |
(as before). |
62645
a2351f82bc48
eliminated spurious Unicode, which is in conflict with Isabelle symbol interpretation;
wenzelm
parents:
62642
diff
changeset
|
459 |
* The ASCII zero character is printed and parsed as "0". |
62678 | 460 |
* All other canonical characters are printed as "CHR 0xXX" |
461 |
with XX being the hexadecimal character code. "CHR n" |
|
62597 | 462 |
is parsable for every numeral expression n. |
62598 | 463 |
* Non-canonical characters have no special syntax and are |
62597 | 464 |
printed as their logical representation. |
465 |
- Explicit conversions from and to the natural numbers are |
|
466 |
provided as char_of_nat, nat_of_char (as before). |
|
467 |
- The auxiliary nibble type has been discontinued. |
|
468 |
||
469 |
INCOMPATIBILITY. |
|
470 |
||
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
471 |
* 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
|
472 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
473 |
- 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
|
474 |
by default. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
475 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
476 |
- Converting between "count M a = 0" and non-membership happens using |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
477 |
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
|
478 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
479 |
- 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
|
480 |
"count M a = n" from membership. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
481 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
482 |
- 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
|
483 |
"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
|
484 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
485 |
INCOMPATIBILITY. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
486 |
|
63310
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
487 |
* The names of multiset theorems have been normalised to distinguish which |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
488 |
ordering the theorems are about |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
489 |
mset_less_eqI ~> mset_subset_eqI |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
490 |
mset_less_insertD ~> mset_subset_insertD |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
491 |
mset_less_eq_count ~> mset_subset_eq_count |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
492 |
mset_less_diff_self ~> mset_subset_diff_self |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
493 |
mset_le_exists_conv ~> mset_subset_eq_exists_conv |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
494 |
mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
495 |
mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
496 |
mset_le_mono_add ~> mset_subset_eq_mono_add |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
497 |
mset_le_add_left ~> mset_subset_eq_add_left |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
498 |
mset_le_add_right ~> mset_subset_eq_add_right |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
499 |
mset_le_single ~> mset_subset_eq_single |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
500 |
mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
501 |
diff_le_self ~> diff_subset_eq_self |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
502 |
mset_leD ~> mset_subset_eqD |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
503 |
mset_lessD ~> mset_subsetD |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
504 |
mset_le_insertD ~> mset_subset_eq_insertD |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
505 |
mset_less_of_empty ~> mset_subset_of_empty |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
506 |
le_empty ~> subset_eq_empty |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
507 |
mset_less_add_bothsides ~> mset_subset_add_bothsides |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
508 |
mset_less_empty_nonempty ~> mset_subset_empty_nonempty |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
509 |
mset_less_size ~> mset_subset_size |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
510 |
wf_less_mset_rel ~> wf_subset_mset_rel |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
511 |
count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
512 |
mset_remdups_le ~> mset_remdups_subset_eq |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
513 |
ms_lesseq_impl ~> subset_eq_mset_impl |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
514 |
|
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
515 |
Some functions have been renamed: |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
516 |
ms_lesseq_impl -> subset_eq_mset_impl |
caaacf37943f
normalising multiset theorem names
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63307
diff
changeset
|
517 |
|
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
518 |
* Multisets are now ordered with the multiset ordering |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
519 |
#\<subseteq># ~> \<le> |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
520 |
#\<subset># ~> < |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
521 |
le_multiset ~> less_eq_multiset |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
522 |
less_multiset ~> le_multiset |
63407
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset
|
523 |
INCOMPATIBILITY. |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
524 |
|
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
525 |
* 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
|
526 |
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
|
527 |
have been discontinued, and the interpretations "multiset_linorder" and |
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset
|
528 |
"multiset_wellorder" have been replaced by instantiations. |
89dd1345a04f
leverage new 'order' type class instantiation in multiset
blanchet
parents:
63388
diff
changeset
|
529 |
INCOMPATIBILITY. |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
530 |
|
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
531 |
* Some theorems about the multiset ordering have been renamed: |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
532 |
le_multiset_def ~> less_eq_multiset_def |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
533 |
less_multiset_def ~> le_multiset_def |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
534 |
less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
535 |
mult_less_not_refl ~> mset_le_not_refl |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
536 |
mult_less_trans ~> mset_le_trans |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
537 |
mult_less_not_sym ~> mset_le_not_sym |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
538 |
mult_less_asym ~> mset_le_asym |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
539 |
mult_less_irrefl ~> mset_le_irrefl |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
540 |
union_less_mono2{,1,2} ~> union_le_mono2{,1,2} |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
541 |
|
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
542 |
le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
543 |
le_multiset_total ~> less_eq_multiset_total |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
544 |
less_multiset_right_total ~> subset_eq_imp_le_multiset |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
545 |
le_multiset_empty_left ~> less_eq_multiset_empty_left |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
546 |
le_multiset_empty_right ~> less_eq_multiset_empty_right |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
547 |
less_multiset_empty_right ~> le_multiset_empty_left |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
548 |
less_multiset_empty_left ~> le_multiset_empty_right |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
549 |
union_less_diff_plus ~> union_le_diff_plus |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
550 |
ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
551 |
less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
552 |
le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
553 |
less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff |
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
554 |
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
|
555 |
INCOMPATIBILITY. |
63388
a095acd4cfbf
instantiate multiset with multiset ordering
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63384
diff
changeset
|
556 |
|
63524
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63513
diff
changeset
|
557 |
* The lemma mset_map has now the attribute [simp]. |
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63513
diff
changeset
|
558 |
INCOMPATIBILITY. |
4ec755485732
adding mset_map to the simp rules
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63513
diff
changeset
|
559 |
|
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
560 |
* Some theorems about multisets have been removed: |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
561 |
le_multiset_plus_plus_left_iff ~> add_less_cancel_right |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
562 |
le_multiset_plus_plus_right_iff ~> add_less_cancel_left |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
563 |
add_eq_self_empty_iff ~> add_cancel_left_right |
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
564 |
mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right |
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
565 |
INCOMPATIBILITY. |
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
566 |
|
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
567 |
* Some typeclass constraints about multisets have been reduced from ordered or |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
568 |
linordered to preorder. Multisets have the additional typeclasses order_bot, |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
569 |
no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add, |
63525
f01d1e393f3f
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63524
diff
changeset
|
570 |
linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le. |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
571 |
INCOMPATIBILITY. |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
572 |
|
63560
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63553
diff
changeset
|
573 |
* There are some new simplification rules about multisets, the multiset |
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63553
diff
changeset
|
574 |
ordering, and the subset ordering on multisets. |
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63553
diff
changeset
|
575 |
INCOMPATIBILITY. |
3e3097ac37d1
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63553
diff
changeset
|
576 |
|
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
577 |
* The subset ordering on multisets has now the interpretations |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
578 |
ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot. |
63410
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
579 |
INCOMPATIBILITY. |
9789ccc2a477
more instantiations for multiset
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63407
diff
changeset
|
580 |
|
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
581 |
* Multiset: single has been removed in favor of add_mset that roughly |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
582 |
corresponds to Set.insert. Some theorems have removed or changed: |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
583 |
single_not_empty ~> add_mset_not_empty or empty_not_add_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
584 |
fold_mset_insert ~> fold_mset_add_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
585 |
image_mset_insert ~> image_mset_add_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
586 |
union_single_eq_diff |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
587 |
multi_self_add_other_not_self |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
588 |
diff_single_eq_union |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
589 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
590 |
|
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
591 |
* Multiset: some theorems have been changed to use add_mset instead of single: |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
592 |
mset_add |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
593 |
multi_self_add_other_not_self |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
594 |
diff_single_eq_union |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
595 |
union_single_eq_diff |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
596 |
union_single_eq_member |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
597 |
add_eq_conv_diff |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
598 |
insert_noteq_member |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
599 |
add_eq_conv_ex |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
600 |
multi_member_split |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
601 |
multiset_add_sub_el_shuffle |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
602 |
mset_subset_eq_insertD |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
603 |
mset_subset_insertD |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
604 |
insert_subset_eq_iff |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
605 |
insert_union_subset_iff |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
606 |
multi_psub_of_add_self |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
607 |
inter_add_left1 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
608 |
inter_add_left2 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
609 |
inter_add_right1 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
610 |
inter_add_right2 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
611 |
sup_union_left1 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
612 |
sup_union_left2 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
613 |
sup_union_right1 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
614 |
sup_union_right2 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
615 |
size_eq_Suc_imp_eq_union |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
616 |
multi_nonempty_split |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
617 |
mset_insort |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
618 |
mset_update |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
619 |
mult1I |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
620 |
less_add |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
621 |
mset_zip_take_Cons_drop_twice |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
622 |
rel_mset_Zero |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
623 |
msed_map_invL |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
624 |
msed_map_invR |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
625 |
msed_rel_invL |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
626 |
msed_rel_invR |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
627 |
le_multiset_right_total |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
628 |
multiset_induct |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
629 |
multiset_induct2_size |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
630 |
multiset_induct2 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
631 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
632 |
|
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
633 |
* Multiset: the definitions of some constants have changed to use add_mset instead |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
634 |
of adding a single element: |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
635 |
image_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
636 |
mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
637 |
replicate_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
638 |
mult1 |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
639 |
pred_mset |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
640 |
rel_mset' |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
641 |
mset_insort |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
642 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
643 |
|
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
644 |
* Due to the above changes, the attributes of some multiset theorems have |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
645 |
been changed: |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
646 |
insert_DiffM [] ~> [simp] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
647 |
insert_DiffM2 [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
648 |
diff_add_mset_swap [simp] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
649 |
fold_mset_add_mset [simp] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
650 |
diff_diff_add [simp] (for multisets only) |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
651 |
diff_cancel [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
652 |
count_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
653 |
set_mset_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
654 |
size_multiset_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
655 |
size_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
656 |
image_mset_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
657 |
mset_subset_eq_mono_add_right_cancel [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
658 |
mset_subset_eq_mono_add_left_cancel [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
659 |
fold_mset_single [simp] ~> [] |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
660 |
subset_eq_empty [simp] ~> [] |
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
661 |
empty_sup [simp] ~> [] |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
662 |
sup_empty [simp] ~> [] |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
663 |
inter_empty [simp] ~> [] |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
664 |
empty_inter [simp] ~> [] |
63793
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
665 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
666 |
|
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
667 |
* The order of the variables in the second cases of multiset_induct, |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
668 |
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@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
669 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
670 |
|
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
671 |
* There is now a simplification procedure on multisets. It mimics the behavior |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
672 |
of the procedure on natural numbers. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
673 |
INCOMPATIBILITY. |
e68a0b651eb5
add_mset constructor in multisets
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63785
diff
changeset
|
674 |
|
63830 | 675 |
* Renamed sums and products of multisets: |
676 |
msetsum ~> sum_mset |
|
677 |
msetprod ~> prod_mset |
|
678 |
||
63919
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63918
diff
changeset
|
679 |
* The symbols for intersection and union of multisets have been changed: |
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63918
diff
changeset
|
680 |
#\<inter> ~> \<inter># |
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63918
diff
changeset
|
681 |
#\<union> ~> \<union># |
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63918
diff
changeset
|
682 |
INCOMPATIBILITY. |
9aed2da07200
# after multiset intersection and union symbol
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63918
diff
changeset
|
683 |
|
63795
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
684 |
* The lemma one_step_implies_mult_aux on multisets has been removed, use |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
685 |
one_step_implies_mult instead. |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
686 |
INCOMPATIBILITY. |
7f6128adfe67
tuning multisets; more interpretations
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63793
diff
changeset
|
687 |
|
63918
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63917
diff
changeset
|
688 |
* The following theorems have been renamed: |
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63917
diff
changeset
|
689 |
setsum_left_distrib ~> setsum_distrib_right |
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63917
diff
changeset
|
690 |
setsum_right_distrib ~> setsum_distrib_left |
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63917
diff
changeset
|
691 |
INCOMPATIBILITY. |
6bf55e6e0b75
left_distrib ~> distrib_right, right_distrib ~> distrib_left
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63917
diff
changeset
|
692 |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
693 |
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
694 |
INCOMPATIBILITY. |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
695 |
|
62358 | 696 |
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional |
697 |
comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". |
|
698 |
||
62345 | 699 |
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. |
700 |
||
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
|
701 |
* 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
|
702 |
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
|
703 |
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
|
704 |
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
|
705 |
|
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
|
706 |
* 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
|
707 |
|
63456
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
708 |
* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
709 |
instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
710 |
instantiation of ordered_ab_semigroup_monoid_add_imp_le might be |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
711 |
required. |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
712 |
INCOMPATIBILITY. |
3365c8ec67bd
sharing simp rules between ordered monoids and rings
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
63455
diff
changeset
|
713 |
|
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
|
714 |
* 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
|
715 |
|
62652
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset
|
716 |
* 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
|
717 |
proofs about monotonicity and continuity in chain-complete partial |
7248d106c607
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
Andreas Lochbihler
parents:
62645
diff
changeset
|
718 |
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
|
719 |
|
62352
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
720 |
* Library/Polynomial.thy contains also derivation of polynomials |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
721 |
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
|
722 |
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
|
723 |
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
|
724 |
for polynomials over factorial rings. INCOMPATIBILITY. |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
725 |
|
63155 | 726 |
* Library/Sublist.thy: added function "prefixes" and renamed |
63173 | 727 |
prefixeq -> prefix |
728 |
prefix -> strict_prefix |
|
729 |
suffixeq -> suffix |
|
730 |
suffix -> strict_suffix |
|
731 |
Added theory of longest common prefixes. |
|
63117 | 732 |
|
62348 | 733 |
* Dropped various legacy fact bindings, whose replacements are often |
734 |
of a more general type also: |
|
735 |
lcm_left_commute_nat ~> lcm.left_commute |
|
736 |
lcm_left_commute_int ~> lcm.left_commute |
|
737 |
gcd_left_commute_nat ~> gcd.left_commute |
|
738 |
gcd_left_commute_int ~> gcd.left_commute |
|
739 |
gcd_greatest_iff_nat ~> gcd_greatest_iff |
|
740 |
gcd_greatest_iff_int ~> gcd_greatest_iff |
|
741 |
coprime_dvd_mult_nat ~> coprime_dvd_mult |
|
742 |
coprime_dvd_mult_int ~> coprime_dvd_mult |
|
743 |
zpower_numeral_even ~> power_numeral_even |
|
744 |
gcd_mult_cancel_nat ~> gcd_mult_cancel |
|
745 |
gcd_mult_cancel_int ~> gcd_mult_cancel |
|
746 |
div_gcd_coprime_nat ~> div_gcd_coprime |
|
747 |
div_gcd_coprime_int ~> div_gcd_coprime |
|
748 |
zpower_numeral_odd ~> power_numeral_odd |
|
749 |
zero_less_int_conv ~> of_nat_0_less_iff |
|
750 |
gcd_greatest_nat ~> gcd_greatest |
|
751 |
gcd_greatest_int ~> gcd_greatest |
|
752 |
coprime_mult_nat ~> coprime_mult |
|
753 |
coprime_mult_int ~> coprime_mult |
|
754 |
lcm_commute_nat ~> lcm.commute |
|
755 |
lcm_commute_int ~> lcm.commute |
|
756 |
int_less_0_conv ~> of_nat_less_0_iff |
|
757 |
gcd_commute_nat ~> gcd.commute |
|
758 |
gcd_commute_int ~> gcd.commute |
|
759 |
Gcd_insert_nat ~> Gcd_insert |
|
760 |
Gcd_insert_int ~> Gcd_insert |
|
761 |
of_int_int_eq ~> of_int_of_nat_eq |
|
762 |
lcm_least_nat ~> lcm_least |
|
763 |
lcm_least_int ~> lcm_least |
|
764 |
lcm_assoc_nat ~> lcm.assoc |
|
765 |
lcm_assoc_int ~> lcm.assoc |
|
766 |
int_le_0_conv ~> of_nat_le_0_iff |
|
767 |
int_eq_0_conv ~> of_nat_eq_0_iff |
|
768 |
Gcd_empty_nat ~> Gcd_empty |
|
769 |
Gcd_empty_int ~> Gcd_empty |
|
770 |
gcd_assoc_nat ~> gcd.assoc |
|
771 |
gcd_assoc_int ~> gcd.assoc |
|
772 |
zero_zle_int ~> of_nat_0_le_iff |
|
773 |
lcm_dvd2_nat ~> dvd_lcm2 |
|
774 |
lcm_dvd2_int ~> dvd_lcm2 |
|
775 |
lcm_dvd1_nat ~> dvd_lcm1 |
|
776 |
lcm_dvd1_int ~> dvd_lcm1 |
|
777 |
gcd_zero_nat ~> gcd_eq_0_iff |
|
778 |
gcd_zero_int ~> gcd_eq_0_iff |
|
779 |
gcd_dvd2_nat ~> gcd_dvd2 |
|
780 |
gcd_dvd2_int ~> gcd_dvd2 |
|
781 |
gcd_dvd1_nat ~> gcd_dvd1 |
|
782 |
gcd_dvd1_int ~> gcd_dvd1 |
|
783 |
int_numeral ~> of_nat_numeral |
|
784 |
lcm_ac_nat ~> ac_simps |
|
785 |
lcm_ac_int ~> ac_simps |
|
786 |
gcd_ac_nat ~> ac_simps |
|
787 |
gcd_ac_int ~> ac_simps |
|
788 |
abs_int_eq ~> abs_of_nat |
|
789 |
zless_int ~> of_nat_less_iff |
|
790 |
zdiff_int ~> of_nat_diff |
|
791 |
zadd_int ~> of_nat_add |
|
792 |
int_mult ~> of_nat_mult |
|
793 |
int_Suc ~> of_nat_Suc |
|
794 |
inj_int ~> inj_of_nat |
|
795 |
int_1 ~> of_nat_1 |
|
796 |
int_0 ~> of_nat_0 |
|
62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
797 |
Lcm_empty_nat ~> Lcm_empty |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
798 |
Lcm_empty_int ~> Lcm_empty |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
799 |
Lcm_insert_nat ~> Lcm_insert |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
800 |
Lcm_insert_int ~> Lcm_insert |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
801 |
comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
802 |
comp_fun_idem_gcd_int ~> comp_fun_idem_gcd |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
803 |
comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
804 |
comp_fun_idem_lcm_int ~> comp_fun_idem_lcm |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
805 |
Lcm_eq_0 ~> Lcm_eq_0_I |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
806 |
Lcm0_iff ~> Lcm_0_iff |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
807 |
Lcm_dvd_int ~> Lcm_least |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
808 |
divides_mult_nat ~> divides_mult |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
809 |
divides_mult_int ~> divides_mult |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
810 |
lcm_0_nat ~> lcm_0_right |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
811 |
lcm_0_int ~> lcm_0_right |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
812 |
lcm_0_left_nat ~> lcm_0_left |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
813 |
lcm_0_left_int ~> lcm_0_left |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
814 |
dvd_gcd_D1_nat ~> dvd_gcdD1 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
815 |
dvd_gcd_D1_int ~> dvd_gcdD1 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
816 |
dvd_gcd_D2_nat ~> dvd_gcdD2 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
817 |
dvd_gcd_D2_int ~> dvd_gcdD2 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
818 |
coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
819 |
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff |
62348 | 820 |
realpow_minus_mult ~> power_minus_mult |
821 |
realpow_Suc_le_self ~> power_Suc_le_self |
|
62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
822 |
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest |
62347 | 823 |
INCOMPATIBILITY. |
824 |
||
62479 | 825 |
* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. |
826 |
||
63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
827 |
* Renamed HOL/Quotient_Examples/FSet.thy to |
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63963
diff
changeset
|
828 |
HOL/Quotient_Examples/Quotient_FSet.thy |
63920
003622e08379
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
kuncar
parents:
63919
diff
changeset
|
829 |
INCOMPATIBILITY. |
63198
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset
|
830 |
|
62498 | 831 |
*** ML *** |
832 |
||
63669 | 833 |
* ML antiquotation @{path} is superseded by @{file}, which ensures that |
834 |
the argument is a plain file. Minor INCOMPATIBILITY. |
|
835 |
||
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset
|
836 |
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML |
63228 | 837 |
library (notably for big integers). Subtle change of semantics: |
838 |
Integer.gcd and Integer.lcm both normalize the sign, results are never |
|
839 |
negative. This coincides with the definitions in HOL/GCD.thy. |
|
840 |
INCOMPATIBILITY. |
|
63227
d3ed7f00e818
Integer.lcm normalizes the sign as in HOL/GCD.thy;
wenzelm
parents:
63226
diff
changeset
|
841 |
|
63212 | 842 |
* Structure Rat for rational numbers is now an integral part of |
63215 | 843 |
Isabelle/ML, with special notation @int/nat or @int for numerals (an |
844 |
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty |
|
63212 | 845 |
printing. Standard operations on type Rat.rat are provided via ad-hoc |
63215 | 846 |
overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to |
63212 | 847 |
use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been |
848 |
superseded by General.Div. |
|
63198
c583ca33076a
ad-hoc overloading for standard operations on type Rat.rat;
wenzelm
parents:
63184
diff
changeset
|
849 |
|
62861 | 850 |
* The ML function "ML" provides easy access to run-time compilation. |
851 |
This is particularly useful for conditional compilation, without |
|
852 |
requiring separate files. |
|
853 |
||
62851 | 854 |
* Low-level 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
|
855 |
exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY. |
62851 | 856 |
|
62662
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset
|
857 |
* Antiquotation @{make_string} is available during Pure bootstrap -- |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset
|
858 |
with approximative output quality. |
291cc01f56f5
@{make_string} is available during Pure bootstrap;
wenzelm
parents:
62645
diff
changeset
|
859 |
|
62498 | 860 |
* Option ML_exception_debugger controls detailed exception trace via the |
861 |
Poly/ML debugger. Relevant ML modules need to be compiled beforehand |
|
862 |
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note |
|
863 |
debugger information requires consirable time and space: main |
|
864 |
Isabelle/HOL with full debugger support may need ML_system_64. |
|
865 |
||
62514 | 866 |
* Local_Theory.restore has been renamed to Local_Theory.reset to |
867 |
emphasize its disruptive impact on the cumulative context, notably the |
|
868 |
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is |
|
869 |
only appropriate when targets are managed, e.g. starting from a global |
|
870 |
theory and returning to it. Regular definitional packages should use |
|
871 |
balanced blocks of Local_Theory.open_target versus |
|
872 |
Local_Theory.close_target instead. Rare INCOMPATIBILITY. |
|
873 |
||
62519 | 874 |
* Structure TimeLimit (originally from the SML/NJ library) has been |
875 |
replaced by structure Timeout, with slightly different signature. |
|
876 |
INCOMPATIBILITY. |
|
877 |
||
62551 | 878 |
* Discontinued cd and pwd operations, which are not well-defined in a |
879 |
multi-threaded environment. Note that files are usually located |
|
880 |
relatively to the master directory of a theory (see also |
|
881 |
File.full_path). Potential INCOMPATIBILITY. |
|
882 |
||
63352 | 883 |
* Binding.empty_atts supersedes Thm.empty_binding and |
884 |
Attrib.empty_binding. Minor INCOMPATIBILITY. |
|
885 |
||
62498 | 886 |
|
62354 | 887 |
*** System *** |
888 |
||
62840
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset
|
889 |
* 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
|
890 |
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
|
891 |
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
|
892 |
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
|
893 |
discontinued. Potential INCOMPATIBILITY. |
d9744f41a4ec
renamed ISABELLE_BUILD_JAVA_OPTIONS to ISABELLE_TOOL_JAVA_OPTIONS;
wenzelm
parents:
62807
diff
changeset
|
894 |
|
62591 | 895 |
* The Isabelle system environment always ensures that the main |
896 |
executables are found within the shell search $PATH: "isabelle" and |
|
897 |
"isabelle_scala_script". |
|
898 |
||
63226 | 899 |
* Isabelle tools may consist of .scala files: the Scala compiler is |
900 |
invoked on the spot. The source needs to define some object that extends |
|
901 |
Isabelle_Tool.Body. |
|
902 |
||
62591 | 903 |
* The Isabelle ML process is now managed directly by Isabelle/Scala, and |
904 |
shell scripts merely provide optional command-line access. In |
|
905 |
particular: |
|
906 |
||
907 |
. Scala module ML_Process to connect to the raw ML process, |
|
908 |
with interaction via stdin/stdout/stderr or in batch mode; |
|
909 |
. command-line tool "isabelle console" as interactive wrapper; |
|
910 |
. command-line tool "isabelle process" as batch mode wrapper. |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
911 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
912 |
* The executable "isabelle_process" has been discontinued. Tools and |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
913 |
prover front-ends should use ML_Process or Isabelle_Process in |
62591 | 914 |
Isabelle/Scala. INCOMPATIBILITY. |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
915 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
916 |
* New command-line tool "isabelle process" supports ML evaluation of |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
917 |
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
|
918 |
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
|
919 |
return code 1. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
920 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
921 |
* Command-line tool "isabelle console" provides option -r to help to |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
922 |
bootstrapping Isabelle/Pure interactively. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
923 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
924 |
* Command-line tool "isabelle yxml" has been discontinued. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
925 |
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
926 |
Isabelle/ML or Isabelle/Scala. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
927 |
|
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
|
928 |
* 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
|
929 |
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
|
930 |
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
|
931 |
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
|
932 |
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
|
933 |
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
|
934 |
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
|
935 |
|
62591 | 936 |
* SML/NJ and old versions of Poly/ML are no longer supported. |
937 |
||
62642 | 938 |
* Poly/ML heaps now follow the hierarchy of sessions, and thus require |
939 |
much less disk space. |
|
940 |
||
63827
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63821
diff
changeset
|
941 |
* System option "checkpoint" helps to fine-tune the global heap space |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63821
diff
changeset
|
942 |
management of isabelle build. This is relevant for big sessions that may |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63821
diff
changeset
|
943 |
exhaust the small 32-bit address space of the ML process (which is used |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63821
diff
changeset
|
944 |
by default). |
b24d0e53dd03
option "checkpoint" helps to fine-tune global heap space management;
wenzelm
parents:
63821
diff
changeset
|
945 |
|
62354 | 946 |
|
947 |
||
62031 | 948 |
New in Isabelle2016 (February 2016) |
62016 | 949 |
----------------------------------- |
60138 | 950 |
|
61337 | 951 |
*** General *** |
952 |
||
62168
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
953 |
* Eisbach is now based on Pure instead of HOL. Objects-logics may import |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
954 |
either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
955 |
~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
956 |
the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
957 |
examples that do require HOL. |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
958 |
|
62157 | 959 |
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for |
960 |
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage. |
|
961 |
||
62017 | 962 |
* Former "xsymbols" syntax with Isabelle symbols is used by default, |
963 |
without any special print mode. Important ASCII replacement syntax |
|
964 |
remains available under print mode "ASCII", but less important syntax |
|
965 |
has been removed (see below). |
|
966 |
||
62109 | 967 |
* Support for more arrow symbols, with rendering in LaTeX and Isabelle |
968 |
fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>. |
|
62017 | 969 |
|
62108
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
970 |
* 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
|
971 |
context has been discontinued. Rare INCOMPATIBILITY, use explicit |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
972 |
structure name instead, notably in indexed notation with block-subscript |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
973 |
(e.g. \<odot>\<^bsub>A\<^esub>). |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
974 |
|
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
975 |
* 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
|
976 |
counterpart \<box> as quantifier-like symbol. A small diamond is available as |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
977 |
\<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
|
978 |
meaning. |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
979 |
|
62017 | 980 |
* Syntax for formal comments "-- text" now also supports the symbolic |
981 |
form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps |
|
982 |
to update old sources. |
|
983 |
||
61337 | 984 |
* Toplevel theorem statements have been simplified as follows: |
985 |
||
986 |
theorems ~> lemmas |
|
987 |
schematic_lemma ~> schematic_goal |
|
988 |
schematic_theorem ~> schematic_goal |
|
989 |
schematic_corollary ~> schematic_goal |
|
990 |
||
991 |
Command-line tool "isabelle update_theorems" updates theory sources |
|
992 |
accordingly. |
|
993 |
||
61338 | 994 |
* Toplevel theorem statement 'proposition' is another alias for |
995 |
'theorem'. |
|
996 |
||
62169 | 997 |
* The old 'defs' command has been removed (legacy since Isabelle2014). |
998 |
INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or |
|
999 |
deferred definitions require a surrounding 'overloading' block. |
|
1000 |
||
61337 | 1001 |
|
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
|
1002 |
*** 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
|
1003 |
|
60986 | 1004 |
* IDE support for the source-level debugger of Poly/ML, to work with |
62253 | 1005 |
Isabelle/ML and official Standard ML. Option "ML_debugger" and commands |
1006 |
'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
|
1007 |
'SML_file_no_debug' control compilation of sources with or without |
|
1008 |
debugging information. The Debugger panel allows to set breakpoints (via |
|
1009 |
context menu), step through stopped threads, evaluate local ML |
|
1010 |
expressions etc. At least one Debugger view needs to be active to have |
|
1011 |
any effect on the running ML program. |
|
60984 | 1012 |
|
61803 | 1013 |
* The State panel manages explicit proof state output, with dynamic |
1014 |
auto-update according to cursor movement. Alternatively, the jEdit |
|
1015 |
action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
|
1016 |
update. |
|
61729 | 1017 |
|
1018 |
* The Output panel no longer shows proof state output by default, to |
|
1019 |
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or |
|
1020 |
enable option "editor_output_state". |
|
61215 | 1021 |
|
61803 | 1022 |
* The text overview column (status of errors, warnings etc.) is updated |
1023 |
asynchronously, leading to much better editor reactivity. Moreover, the |
|
1024 |
full document node content is taken into account. The width of the |
|
1025 |
column is scaled according to the main text area font, for improved |
|
1026 |
visibility. |
|
1027 |
||
1028 |
* The main text area no longer changes its color hue in outdated |
|
1029 |
situations. The text overview column takes over the role to indicate |
|
1030 |
unfinished edits in the PIDE pipeline. This avoids flashing text display |
|
1031 |
due to ad-hoc updates by auxiliary GUI components, such as the State |
|
1032 |
panel. |
|
1033 |
||
62254
81cbea2babd9
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset
|
1034 |
* Slightly improved scheduling for urgent print tasks (e.g. command |
81cbea2babd9
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset
|
1035 |
state output, interactive queries) wrt. long-running background tasks. |
62017 | 1036 |
|
1037 |
* Completion of symbols via prefix of \<name> or \<^name> or \name is |
|
1038 |
always possible, independently of the language context. It is never |
|
1039 |
implicit: a popup will show up unconditionally. |
|
1040 |
||
1041 |
* Additional abbreviations for syntactic completion may be specified in |
|
1042 |
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with |
|
1043 |
support for simple templates using ASCII 007 (bell) as placeholder. |
|
1044 |
||
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
|
1045 |
* 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
|
1046 |
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
|
1047 |
ASCII syntax. INCOMPATIBILITY, use plain backslash-completion 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
|
1048 |
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
|
1049 |
|
61483 | 1050 |
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
1051 |
emphasized text style; the effect is visible in document output, not in |
|
1052 |
the editor. |
|
1053 |
||
1054 |
* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, |
|
1055 |
instead of former C+e LEFT. |
|
1056 |
||
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
1057 |
* The command-line tool "isabelle jedit" and the isabelle.Main |
62027 | 1058 |
application wrapper treat the default $USER_HOME/Scratch.thy more |
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
1059 |
uniformly, and allow the dummy file argument ":" to open an empty buffer |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
1060 |
instead. |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
1061 |
|
62017 | 1062 |
* New command-line tool "isabelle jedit_client" allows to connect to an |
1063 |
already running Isabelle/jEdit process. This achieves the effect of |
|
1064 |
single-instance applications seen on common GUI desktops. |
|
1065 |
||
61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
1066 |
* The default look-and-feel 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
|
1067 |
works better with GUI scaling for very high-resolution displays (e.g. |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
1068 |
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
|
1069 |
|
62163 | 1070 |
* Update to jedit-5.3.0, with improved GUI scaling and support of |
1071 |
high-resolution displays (e.g. 4K). |
|
1072 |
||
62034 | 1073 |
* The main Isabelle executable is managed as single-instance Desktop |
1074 |
application uniformly on all platforms: Linux, Windows, Mac OS X. |
|
1075 |
||
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
|
1076 |
|
61405 | 1077 |
*** Document preparation *** |
1078 |
||
63553
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset
|
1079 |
* Text and ML antiquotation @{locale} for locales, similar to existing |
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset
|
1080 |
antiquotations for classes. |
4a72b37ac4b8
text antiquotation for locales (similar to classes)
haftmann
parents:
63552
diff
changeset
|
1081 |
|
62017 | 1082 |
* Commands 'paragraph' and 'subparagraph' provide additional section |
1083 |
headings. Thus there are 6 levels of standard headings, as in HTML. |
|
1084 |
||
1085 |
* Command 'text_raw' has been clarified: input text is processed as in |
|
1086 |
'text' (with antiquotations and control symbols). The key difference is |
|
1087 |
the lack of the surrounding isabelle markup environment in output. |
|
1088 |
||
1089 |
* Text is structured in paragraphs and nested lists, using notation that |
|
1090 |
is similar to Markdown. The control symbols for list items are as |
|
1091 |
follows: |
|
1092 |
||
1093 |
\<^item> itemize |
|
1094 |
\<^enum> enumerate |
|
1095 |
\<^descr> description |
|
1096 |
||
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1097 |
* 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
|
1098 |
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
61595 | 1099 |
\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
1100 |
\<^name> without following cartouche is equivalent to @{name}. The |
|
61501 | 1101 |
standard Isabelle fonts provide glyphs to render important control |
1102 |
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1103 |
|
61595 | 1104 |
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
1105 |
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
|
1106 |
standard LaTeX macros of the same names. |
|
1107 |
||
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1108 |
* 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
|
1109 |
Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
61492 | 1110 |
text. Command-line tool "isabelle update_cartouches -t" helps to update |
1111 |
old sources, by approximative patching of the content of string and |
|
1112 |
cartouche tokens seen in theory sources. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1113 |
|
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1114 |
* The @{text} antiquotation now ignores the antiquotation option |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1115 |
"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
|
1116 |
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the |
61494 | 1117 |
argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial |
1118 |
or terminal spaces are ignored. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
1119 |
|
62017 | 1120 |
* Antiquotations @{emph} and @{bold} output LaTeX source recursively, |
1121 |
adding appropriate text style markup. These may be used in the short |
|
1122 |
form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
|
1123 |
||
1124 |
* Document antiquotation @{footnote} outputs LaTeX source recursively, |
|
1125 |
marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. |
|
1126 |
||
1127 |
* Antiquotation @{verbatim [display]} supports option "indent". |
|
1128 |
||
1129 |
* Antiquotation @{theory_text} prints uninterpreted theory source text |
|
62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset
|
1130 |
(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
|
1131 |
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". |
62017 | 1132 |
|
1133 |
* Antiquotation @{doc ENTRY} provides a reference to the given |
|
1134 |
documentation, with a hyperlink in the Prover IDE. |
|
1135 |
||
1136 |
* Antiquotations @{command}, @{method}, @{attribute} print checked |
|
1137 |
entities of the Isar language. |
|
1138 |
||
61471 | 1139 |
* HTML presentation uses the standard IsabelleText font and Unicode |
1140 |
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former |
|
61488 | 1141 |
print mode "HTML" loses its special meaning. |
61471 | 1142 |
|
61405 | 1143 |
|
60406 | 1144 |
*** Isar *** |
1145 |
||
62205 | 1146 |
* Local goals ('have', 'show', 'hence', 'thus') allow structured rule |
1147 |
statements like fixes/assumes/shows in theorem specifications, but the |
|
1148 |
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
|
1149 |
example: |
60414 | 1150 |
|
1151 |
have result: "C x y" |
|
1152 |
if "A x" and "B y" |
|
1153 |
for x :: 'a and y :: 'a |
|
1154 |
<proof> |
|
1155 |
||
60449 | 1156 |
The local assumptions are bound to the name "that". The result is |
1157 |
exported from context of the statement as usual. The above roughly |
|
60414 | 1158 |
corresponds to a raw proof block like this: |
1159 |
||
1160 |
{ |
|
1161 |
fix x :: 'a and y :: 'a |
|
60449 | 1162 |
assume that: "A x" "B y" |
60414 | 1163 |
have "C x y" <proof> |
1164 |
} |
|
1165 |
note result = this |
|
60406 | 1166 |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
1167 |
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
|
1168 |
instead of 'assume' above. |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
1169 |
|
61733 | 1170 |
* Assumptions ('assume', 'presume') allow structured rule statements |
1171 |
using 'if' and 'for', similar to 'have' etc. above. For example: |
|
61658 | 1172 |
|
1173 |
assume result: "C x y" |
|
1174 |
if "A x" and "B y" |
|
1175 |
for x :: 'a and y :: 'a |
|
1176 |
||
1177 |
This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general |
|
1178 |
result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y". |
|
1179 |
||
1180 |
Vacuous quantification in assumptions is omitted, i.e. a for-context |
|
1181 |
only effects propositions according to actual use of variables. For |
|
1182 |
example: |
|
1183 |
||
1184 |
assume "A x" and "B y" for x and y |
|
1185 |
||
1186 |
is equivalent to: |
|
1187 |
||
1188 |
assume "\<And>x. A x" and "\<And>y. B y" |
|
1189 |
||
60595 | 1190 |
* The meaning of 'show' with Pure rule statements has changed: premises |
1191 |
are treated in the sense of 'assume', instead of 'presume'. This means, |
|
62205 | 1192 |
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as |
1193 |
follows: |
|
60595 | 1194 |
|
1195 |
show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
1196 |
||
1197 |
or: |
|
1198 |
||
1199 |
show "C x" if "A x" "B x" for x |
|
1200 |
||
1201 |
Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: |
|
1202 |
||
1203 |
show "C x" when "A x" "B x" for x |
|
1204 |
||
60459 | 1205 |
* New command 'consider' states rules for generalized elimination and |
1206 |
case splitting. This is like a toplevel statement "theorem obtains" used |
|
1207 |
within a proof body; or like a multi-branch 'obtain' without activation |
|
1208 |
of the local context elements yet. |
|
1209 |
||
60455 | 1210 |
* Proof method "cases" allows to specify the rule as first entry of |
1211 |
chained facts. This is particularly useful with 'consider': |
|
1212 |
||
1213 |
consider (a) A | (b) B | (c) C <proof> |
|
1214 |
then have something |
|
1215 |
proof cases |
|
1216 |
case a |
|
1217 |
then show ?thesis <proof> |
|
1218 |
next |
|
1219 |
case b |
|
1220 |
then show ?thesis <proof> |
|
1221 |
next |
|
1222 |
case c |
|
1223 |
then show ?thesis <proof> |
|
1224 |
qed |
|
1225 |
||
60565 | 1226 |
* Command 'case' allows fact name and attribute specification like this: |
1227 |
||
1228 |
case a: (c xs) |
|
1229 |
case a [attributes]: (c xs) |
|
1230 |
||
1231 |
Facts that are introduced by invoking the case context are uniformly |
|
1232 |
qualified by "a"; the same name is used for the cumulative fact. The old |
|
1233 |
form "case (c xs) [attributes]" is no longer supported. Rare |
|
1234 |
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, |
|
1235 |
and always put attributes in front. |
|
1236 |
||
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
1237 |
* 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
|
1238 |
"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
|
1239 |
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
|
1240 |
'..' 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
|
1241 |
|
62017 | 1242 |
* Nesting of Isar goal structure has been clarified: the context after |
1243 |
the initial backwards refinement is retained for the whole proof, within |
|
1244 |
all its context sections (as indicated via 'next'). This is e.g. |
|
1245 |
relevant for 'using', 'including', 'supply': |
|
1246 |
||
1247 |
have "A \<and> A" if a: A for A |
|
1248 |
supply [simp] = a |
|
1249 |
proof |
|
1250 |
show A by simp |
|
1251 |
next |
|
1252 |
show A by simp |
|
1253 |
qed |
|
1254 |
||
1255 |
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
|
1256 |
proof body as well, abstracted over relevant parameters. |
|
1257 |
||
1258 |
* Improved type-inference for theorem statement 'obtains': separate |
|
1259 |
parameter scope for of each clause. |
|
1260 |
||
1261 |
* Term abbreviations via 'is' patterns also work for schematic |
|
1262 |
statements: result is abstracted over unknowns. |
|
1263 |
||
60631 | 1264 |
* Command 'subgoal' allows to impose some structure on backward |
1265 |
refinements, to avoid proof scripts degenerating into long of 'apply' |
|
1266 |
sequences. Further explanations and examples are given in the isar-ref |
|
1267 |
manual. |
|
1268 |
||
62017 | 1269 |
* Command 'supply' supports fact definitions during goal refinement |
1270 |
('apply' scripts). |
|
1271 |
||
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
1272 |
* 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
|
1273 |
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
|
1274 |
example: |
60617 | 1275 |
|
1276 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
60622 | 1277 |
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
|
1278 |
proof goal_cases |
60622 | 1279 |
case (1 x) |
1280 |
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry |
|
1281 |
next |
|
1282 |
case (2 y z) |
|
1283 |
then show ?case using \<open>U y\<close> \<open>V z\<close> sorry |
|
1284 |
qed |
|
1285 |
||
1286 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
1287 |
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
|
1288 |
proof goal_cases |
60617 | 1289 |
case prems: 1 |
1290 |
then show ?case using prems sorry |
|
1291 |
next |
|
1292 |
case prems: 2 |
|
1293 |
then show ?case using prems sorry |
|
1294 |
qed |
|
60578 | 1295 |
|
60581 | 1296 |
* The undocumented feature of implicit cases goal1, goal2, goal3, etc. |
60617 | 1297 |
is marked as legacy, and will be removed eventually. The proof method |
1298 |
"goals" achieves a similar effect within regular Isar; often it can be |
|
1299 |
done more adequately by other means (e.g. 'consider'). |
|
60581 | 1300 |
|
62017 | 1301 |
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` |
1302 |
as well, not just "by this" or "." as before. |
|
60551 | 1303 |
|
60554 | 1304 |
* Method "sleep" succeeds after a real-time delay (in seconds). This is |
1305 |
occasionally useful for demonstration and testing purposes. |
|
1306 |
||
60406 | 1307 |
|
60331 | 1308 |
*** Pure *** |
1309 |
||
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
1310 |
* Qualifiers in locale expressions default to mandatory ('!') regardless |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
1311 |
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
|
1312 |
optional ('?'). The old synatx '!' has been discontinued. |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
1313 |
INCOMPATIBILITY, remove '!' and add '?' as required. |
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
1314 |
|
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
1315 |
* Keyword 'rewrites' identifies rewrite morphisms in interpretation |
62017 | 1316 |
commands. Previously, the keyword was 'where'. INCOMPATIBILITY. |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
1317 |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1318 |
* More gentle suppression of syntax along locale morphisms while |
62017 | 1319 |
printing terms. Previously 'abbreviation' and 'notation' declarations |
1320 |
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
|
1321 |
'abbreviation' is also kept for morphims that only change the involved |
62017 | 1322 |
parameters, and only 'notation' is suppressed. This can be of great help |
1323 |
when working with complex locale hierarchies, because proof states are |
|
1324 |
displayed much more succinctly. It also means that only notation needs |
|
1325 |
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
|
1326 |
|
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1327 |
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
|
1328 |
begin |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1329 |
definition derived (infixl "\<odot>" 65) where ... |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1330 |
end |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1331 |
|
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1332 |
locale morphism = |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1333 |
left: struct composition + right: struct composition' |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1334 |
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
|
1335 |
begin |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1336 |
notation right.derived ("\<odot>''") |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1337 |
end |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
1338 |
|
61895 | 1339 |
* Command 'global_interpretation' issues interpretations into global |
1340 |
theories, with optional rewrite definitions following keyword 'defines'. |
|
1341 |
||
1342 |
* Command 'sublocale' accepts optional rewrite definitions after keyword |
|
61675 | 1343 |
'defines'. |
1344 |
||
61895 | 1345 |
* Command 'permanent_interpretation' has been discontinued. Use |
1346 |
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61660
diff
changeset
|
1347 |
|
61252 | 1348 |
* Command 'print_definitions' prints dependencies of definitional |
1349 |
specifications. This functionality used to be part of 'print_theory'. |
|
1350 |
||
60331 | 1351 |
* Configuration option rule_insts_schematic has been discontinued |
62017 | 1352 |
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. |
60331 |