author | wenzelm |
Wed, 22 Aug 2012 22:47:16 +0200 | |
changeset 48890 | d72ca5742f80 |
parent 48844 | 6408fb6f7d81 |
child 48936 | e6d9e46ff7bc |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
47887 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
7 |
*** General *** |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
8 |
|
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
9 |
* Command 'ML_file' evaluates ML text from a file directly within the |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
10 |
theory, without any predeclaration via 'uses' in the theory header. |
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
11 |
|
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
12 |
* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
13 |
is called fastforce / fast_force_tac already since Isabelle2011-1. |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
14 |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
15 |
* Updated and extended "isar-ref" manual, reduced remaining material |
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
16 |
in old "ref" manual. |
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
17 |
|
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
18 |
|
48205 | 19 |
*** Pure *** |
20 |
||
48431
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
21 |
* Code generation for Haskell: restrict unqualified imports from |
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
22 |
Haskell Prelude to a small set of fundamental operations. |
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
23 |
|
48371 | 24 |
* Command "export_code": relative file names are interpreted |
25 |
relatively to master directory of current theory rather than |
|
26 |
the rather arbitrary current working directory. |
|
27 |
INCOMPATIBILITY. |
|
28 |
||
48205 | 29 |
* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
30 |
use regular rule composition via "OF" / "THEN", or explicit proof |
|
31 |
structure instead. Note that Isabelle/ML provides a variety of |
|
32 |
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
|
33 |
with some care where this is really required. |
|
34 |
||
48792 | 35 |
* Command 'typ' supports an additional variant with explicit sort |
36 |
constraint, to infer and check the most general type conforming to a |
|
37 |
given given sort. Example (in HOL): |
|
38 |
||
39 |
typ "_ * _ * bool * unit" :: finite |
|
40 |
||
48205 | 41 |
|
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
42 |
*** HOL *** |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
43 |
|
48428 | 44 |
* Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
45 |
execution for code generated towards Isabelle/ML. |
|
46 |
||
48206 | 47 |
* Simproc "finite_Collect" rewrites set comprehensions into pointfree |
48 |
expressions. |
|
48111 | 49 |
|
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
50 |
* Quickcheck: |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
51 |
|
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
52 |
- added an optimisation for equality premises. |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
53 |
It is switched on by default, and can be switched off by setting |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
54 |
the configuration quickcheck_optimise_equality to false. |
47887 | 55 |
|
48069
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
56 |
* The SMT solver Z3 has now by default a restricted set of directly |
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
57 |
supported features. For the full set of features (div/mod, nonlinear |
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
58 |
arithmetic, datatypes/records) with potential proof reconstruction |
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
59 |
failures, enable the configuration option "z3_with_extensions". |
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
60 |
Minor INCOMPATIBILITY. |
e9b2782c4f99
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
boehmes
parents:
48013
diff
changeset
|
61 |
|
48094 | 62 |
* Sledgehammer: |
63 |
||
48402 | 64 |
- Added MaSh relevance filter based on machine-learning; see the |
65 |
Sledgehammer manual for details. |
|
48094 | 66 |
- Rationalized type encodings ("type_enc" option). |
48294 | 67 |
- Renamed options: |
68 |
max_relevant ~> max_facts |
|
69 |
relevance_thresholds ~> fact_thresholds |
|
48094 | 70 |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
71 |
|
48206 | 72 |
*** Document preparation *** |
73 |
||
74 |
* Default for \<euro> is now based on eurosym package, instead of |
|
75 |
slightly exotic babel/greek. |
|
76 |
||
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
77 |
* Document variant NAME may use different LaTeX entry point |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
78 |
document/root_NAME.tex if that file exists, instead of the common |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
79 |
document/root.tex. |
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
80 |
|
48657
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
81 |
* Simplified custom document/build script, instead of old-style |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
82 |
document/IsaMakefile. Minor INCOMPATIBILITY. |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
83 |
|
48206 | 84 |
|
85 |
*** System *** |
|
86 |
||
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
87 |
* Advanced support for Isabelle sessions and build management, see |
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
88 |
"system" manual for the chapter of that name, especially the "isabelle |
48736 | 89 |
build" tool and its examples. INCOMPATIBILITY, isabelle usedir / |
90 |
mkdir / make are rendered obsolete. |
|
91 |
||
92 |
* Discontinued obsolete "isabelle makeall". |
|
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
93 |
|
48722
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
94 |
* Discontinued obsolete IsaMakefile and ROOT.ML files from the |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
95 |
Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
96 |
provides some traditional targets that invoke "isabelle build". Note |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
97 |
that this is inefficient! Applications of Isabelle/HOL involving |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
98 |
"isabelle make" should be upgraded to use "isabelle build" directly. |
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
99 |
|
48586 | 100 |
* Discontinued obsolete Isabelle/build script, it is superseded by the |
101 |
regular isabelle build tool. For example: |
|
102 |
||
103 |
isabelle build -s -b HOLCF |
|
104 |
||
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
105 |
* The "isabelle options" tool prints Isabelle system options, as |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
106 |
required for "isabelle build", for example. |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
107 |
|
48683 | 108 |
* The "isabelle mkroot" tool prepares session root directories for use |
109 |
with "isabelle build", similar to former "isabelle mkdir" for |
|
110 |
"isabelle usedir". |
|
111 |
||
48844 | 112 |
* The "isabelle components" tool helps to resolve add-on components |
113 |
that are not bundled, or referenced from a bare-bones repository |
|
114 |
version of Isabelle. |
|
115 |
||
48206 | 116 |
* Discontinued support for Poly/ML 5.2.1, which was the last version |
117 |
without exception positions and advanced ML compiler/toplevel |
|
118 |
configuration. |
|
119 |
||
48574 | 120 |
* Discontinued special treatment of Proof General -- no longer guess |
121 |
PROOFGENERAL_HOME based on accidental file-system layout. Minor |
|
122 |
INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS |
|
123 |
settings manually, or use a Proof General version that has been |
|
124 |
bundled as Isabelle component. |
|
48206 | 125 |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
126 |
|
47462 | 127 |
New in Isabelle2012 (May 2012) |
128 |
------------------------------ |
|
45109 | 129 |
|
45593 | 130 |
*** General *** |
131 |
||
45614 | 132 |
* Prover IDE (PIDE) improvements: |
133 |
||
47585 | 134 |
- more robust Sledgehammer integration (as before the sledgehammer |
47806 | 135 |
command-line needs to be typed into the source buffer) |
45614 | 136 |
- markup for bound variables |
47806 | 137 |
- markup for types of term variables (displayed as tooltips) |
46956
9ff441f295c2
Isabelle/jEdit supports user-defined Isar commands within the running session;
wenzelm
parents:
46948
diff
changeset
|
138 |
- support for user-defined Isar commands within the running session |
47158 | 139 |
- improved support for Unicode outside original 16bit range |
140 |
e.g. glyph for \<A> (thanks to jEdit 4.5.1) |
|
45614 | 141 |
|
47806 | 142 |
* Forward declaration of outer syntax keywords within the theory |
143 |
header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
|
144 |
commands to be used in the same theory where defined. |
|
46485 | 145 |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
146 |
* Auxiliary contexts indicate block structure for specifications with |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
147 |
additional parameters and assumptions. Such unnamed contexts may be |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
148 |
nested within other targets, like 'theory', 'locale', 'class', |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
149 |
'instantiation' etc. Results from the local context are generalized |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
150 |
accordingly and applied to the enclosing target context. Example: |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
151 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
152 |
context |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
153 |
fixes x y z :: 'a |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
154 |
assumes xy: "x = y" and yz: "y = z" |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
155 |
begin |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
156 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
157 |
lemma my_trans: "x = z" using xy yz by simp |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
158 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
159 |
end |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
160 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
161 |
thm my_trans |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
162 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
163 |
The most basic application is to factor-out context elements of |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
164 |
several fixes/assumes/shows theorem statements, e.g. see |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
165 |
~~/src/HOL/Isar_Examples/Group_Context.thy |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
166 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
167 |
Any other local theory specification element works within the "context |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
168 |
... begin ... end" block as well. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
169 |
|
47484 | 170 |
* Bundled declarations associate attributed fact expressions with a |
171 |
given name in the context. These may be later included in other |
|
172 |
contexts. This allows to manage context extensions casually, without |
|
47855 | 173 |
the logical dependencies of locales and locale interpretation. See |
174 |
commands 'bundle', 'include', 'including' etc. in the isar-ref manual. |
|
47484 | 175 |
|
47829 | 176 |
* Commands 'lemmas' and 'theorems' allow local variables using 'for' |
177 |
declaration, and results are standardized before being stored. Thus |
|
178 |
old-style "standard" after instantiation or composition of facts |
|
179 |
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of |
|
180 |
indices of schematic variables. |
|
181 |
||
182 |
* Rule attributes in local theory declarations (e.g. locale or class) |
|
183 |
are now statically evaluated: the resulting theorem is stored instead |
|
184 |
of the original expression. INCOMPATIBILITY in rare situations, where |
|
185 |
the historic accident of dynamic re-evaluation in interpretations |
|
186 |
etc. was exploited. |
|
187 |
||
188 |
* New tutorial "Programming and Proving in Isabelle/HOL" |
|
189 |
("prog-prove"). It completely supersedes "A Tutorial Introduction to |
|
190 |
Structured Isar Proofs" ("isar-overview"), which has been removed. It |
|
191 |
also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order |
|
192 |
Logic" as the recommended beginners tutorial, but does not cover all |
|
193 |
of the material of that old tutorial. |
|
194 |
||
195 |
* Updated and extended reference manuals: "isar-ref", |
|
196 |
"implementation", "system"; reduced remaining material in old "ref" |
|
197 |
manual. |
|
198 |
||
199 |
||
200 |
*** Pure *** |
|
201 |
||
46976
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
202 |
* Command 'definition' no longer exports the foundational "raw_def" |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
203 |
into the user context. Minor INCOMPATIBILITY, may use the regular |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
204 |
"def" result with attribute "abs_def" to imitate the old version. |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
205 |
|
47855 | 206 |
* Attribute "abs_def" turns an equation of the form "f x y == t" into |
207 |
"f == %x y. t", which ensures that "simp" or "unfold" steps always |
|
208 |
expand it. This also works for object-logic equality. (Formerly |
|
209 |
undocumented feature.) |
|
210 |
||
47856 | 211 |
* Sort constraints are now propagated in simultaneous statements, just |
212 |
like type constraints. INCOMPATIBILITY in rare situations, where |
|
213 |
distinct sorts used to be assigned accidentally. For example: |
|
214 |
||
215 |
lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
|
216 |
||
217 |
lemma "P (x::'a)" and "Q (y::'a::bar)" |
|
218 |
-- "now uniform 'a::bar instead of default sort for first occurrence (!)" |
|
219 |
||
220 |
* Rule composition via attribute "OF" (or ML functions OF/MRS) is more |
|
221 |
tolerant against multiple unifiers, as long as the final result is |
|
222 |
unique. (As before, rules are composed in canonical right-to-left |
|
223 |
order to accommodate newly introduced premises.) |
|
224 |
||
47806 | 225 |
* Renamed some inner syntax categories: |
226 |
||
227 |
num ~> num_token |
|
228 |
xnum ~> xnum_token |
|
229 |
xstr ~> str_token |
|
230 |
||
231 |
Minor INCOMPATIBILITY. Note that in practice "num_const" or |
|
232 |
"num_position" etc. are mainly used instead (which also include |
|
233 |
position information via constraints). |
|
234 |
||
47829 | 235 |
* Simplified configuration options for syntax ambiguity: see |
236 |
"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref |
|
237 |
manual. Minor INCOMPATIBILITY. |
|
238 |
||
47856 | 239 |
* Discontinued configuration option "syntax_positions": atomic terms |
240 |
in parse trees are always annotated by position constraints. |
|
45134 | 241 |
|
47464 | 242 |
* Old code generator for SML and its commands 'code_module', |
45383 | 243 |
'code_library', 'consts_code', 'types_code' have been discontinued. |
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
244 |
Use commands of the generic code generator instead. INCOMPATIBILITY. |
45383 | 245 |
|
47464 | 246 |
* Redundant attribute "code_inline" has been discontinued. Use |
247 |
"code_unfold" instead. INCOMPATIBILITY. |
|
248 |
||
249 |
* Dropped attribute "code_unfold_post" in favor of the its dual |
|
250 |
"code_abbrev", which yields a common pattern in definitions like |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
251 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
252 |
definition [code_abbrev]: "f = t" |
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
253 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
254 |
INCOMPATIBILITY. |
45383 | 255 |
|
47856 | 256 |
* Obsolete 'types' command has been discontinued. Use 'type_synonym' |
257 |
instead. INCOMPATIBILITY. |
|
258 |
||
259 |
* Discontinued old "prems" fact, which used to refer to the accidental |
|
260 |
collection of foundational premises in the context (already marked as |
|
261 |
legacy since Isabelle2011). |
|
47855 | 262 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
263 |
|
45122 | 264 |
*** HOL *** |
265 |
||
47464 | 266 |
* Type 'a set is now a proper type constructor (just as before |
267 |
Isabelle2008). Definitions mem_def and Collect_def have disappeared. |
|
268 |
Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
|
47855 | 269 |
sets separate, it is often sufficient to rephrase some set S that has |
270 |
been accidentally used as predicates by "%x. x : S", and some |
|
271 |
predicate P that has been accidentally used as set by "{x. P x}". |
|
272 |
Corresponding proofs in a first step should be pruned from any |
|
273 |
tinkering with former theorems mem_def and Collect_def as far as |
|
274 |
possible. |
|
275 |
||
276 |
For developments which deliberately mix predicates and sets, a |
|
47464 | 277 |
planning step is necessary to determine what should become a predicate |
278 |
and what a set. It can be helpful to carry out that step in |
|
279 |
Isabelle2011-1 before jumping right into the current release. |
|
280 |
||
47855 | 281 |
* Code generation by default implements sets as container type rather |
282 |
than predicates. INCOMPATIBILITY. |
|
283 |
||
284 |
* New type synonym 'a rel = ('a * 'a) set |
|
285 |
||
47464 | 286 |
* The representation of numerals has changed. Datatype "num" |
287 |
represents strictly positive binary numerals, along with functions |
|
288 |
"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent |
|
47855 | 289 |
positive and negated numeric literals, respectively. See also |
290 |
definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some |
|
291 |
user theories may require adaptations as follows: |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
292 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
293 |
- Theorems with number_ring or number_semiring constraints: These |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
294 |
classes are gone; use comm_ring_1 or comm_semiring_1 instead. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
295 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
296 |
- Theories defining numeric types: Remove number, number_semiring, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
297 |
and number_ring instances. Defer all theorems about numerals until |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
298 |
after classes one and semigroup_add have been instantiated. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
299 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
300 |
- Numeral-only simp rules: Replace each rule having a "number_of v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
301 |
pattern with two copies, one for numeral and one for neg_numeral. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
302 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
303 |
- Theorems about subclasses of semiring_1 or ring_1: These classes |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
304 |
automatically support numerals now, so more simp rules and |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
305 |
simprocs may now apply within the proof. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
306 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
307 |
- Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
308 |
Redefine using other integer operations. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
309 |
|
47855 | 310 |
* Transfer: New package intended to generalize the existing |
311 |
"descending" method and related theorem attributes from the Quotient |
|
312 |
package. (Not all functionality is implemented yet, but future |
|
313 |
development will focus on Transfer as an eventual replacement for the |
|
314 |
corresponding parts of the Quotient package.) |
|
47809 | 315 |
|
316 |
- transfer_rule attribute: Maintains a collection of transfer rules, |
|
317 |
which relate constants at two different types. Transfer rules may |
|
318 |
relate different type instances of the same polymorphic constant, |
|
319 |
or they may relate an operation on a raw type to a corresponding |
|
320 |
operation on an abstract type (quotient or subtype). For example: |
|
321 |
||
322 |
((A ===> B) ===> list_all2 A ===> list_all2 B) map map |
|
323 |
(cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int |
|
324 |
||
325 |
- transfer method: Replaces a subgoal on abstract types with an |
|
326 |
equivalent subgoal on the corresponding raw types. Constants are |
|
327 |
replaced with corresponding ones according to the transfer rules. |
|
328 |
Goals are generalized over all free variables by default; this is |
|
47851 | 329 |
necessary for variables whose types change, but can be overridden |
47855 | 330 |
for specific variables with e.g. "transfer fixing: x y z". The |
47809 | 331 |
variant transfer' method allows replacing a subgoal with one that |
332 |
is logically stronger (rather than equivalent). |
|
333 |
||
334 |
- relator_eq attribute: Collects identity laws for relators of |
|
335 |
various type constructors, e.g. "list_all2 (op =) = (op =)". The |
|
336 |
transfer method uses these lemmas to infer transfer rules for |
|
337 |
non-polymorphic constants on the fly. |
|
338 |
||
339 |
- transfer_prover method: Assists with proving a transfer rule for a |
|
340 |
new constant, provided the constant is defined in terms of other |
|
341 |
constants that already have transfer rules. It should be applied |
|
342 |
after unfolding the constant definitions. |
|
343 |
||
344 |
- HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer |
|
345 |
from type nat to type int. |
|
346 |
||
47851 | 347 |
* Lifting: New package intended to generalize the quotient_definition |
348 |
facility of the Quotient package; designed to work with Transfer. |
|
47809 | 349 |
|
350 |
- lift_definition command: Defines operations on an abstract type in |
|
351 |
terms of a corresponding operation on a representation |
|
352 |
type. Example syntax: |
|
353 |
||
354 |
lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" |
|
355 |
is List.insert |
|
356 |
||
357 |
Users must discharge a respectfulness proof obligation when each |
|
358 |
constant is defined. (For a type copy, i.e. a typedef with UNIV, |
|
359 |
the proof is discharged automatically.) The obligation is |
|
360 |
presented in a user-friendly, readable form; a respectfulness |
|
361 |
theorem in the standard format and a transfer rule are generated |
|
362 |
by the package. |
|
363 |
||
364 |
- Integration with code_abstype: For typedefs (e.g. subtypes |
|
365 |
corresponding to a datatype invariant, such as dlist), |
|
366 |
lift_definition generates a code certificate theorem and sets up |
|
367 |
code generation for each constant. |
|
368 |
||
369 |
- setup_lifting command: Sets up the Lifting package to work with a |
|
370 |
user-defined type. The user must provide either a quotient theorem |
|
371 |
or a type_definition theorem. The package configures transfer |
|
372 |
rules for equality and quantifiers on the type, and sets up the |
|
373 |
lift_definition command to work with the type. |
|
374 |
||
375 |
- Usage examples: See Quotient_Examples/Lift_DList.thy, |
|
47851 | 376 |
Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy, |
377 |
Word/Word.thy and Library/Float.thy. |
|
47809 | 378 |
|
379 |
* Quotient package: |
|
380 |
||
381 |
- The 'quotient_type' command now supports a 'morphisms' option with |
|
382 |
rep and abs functions, similar to typedef. |
|
383 |
||
384 |
- 'quotient_type' sets up new types to work with the Lifting and |
|
385 |
Transfer packages, as with 'setup_lifting'. |
|
386 |
||
387 |
- The 'quotient_definition' command now requires the user to prove a |
|
388 |
respectfulness property at the point where the constant is |
|
389 |
defined, similar to lift_definition; INCOMPATIBILITY. |
|
390 |
||
391 |
- Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems |
|
392 |
accordingly, INCOMPATIBILITY. |
|
393 |
||
394 |
* New diagnostic command 'find_unused_assms' to find potentially |
|
395 |
superfluous assumptions in theorems using Quickcheck. |
|
396 |
||
397 |
* Quickcheck: |
|
398 |
||
399 |
- Quickcheck returns variable assignments as counterexamples, which |
|
400 |
allows to reveal the underspecification of functions under test. |
|
401 |
For example, refuting "hd xs = x", it presents the variable |
|
402 |
assignment xs = [] and x = a1 as a counterexample, assuming that |
|
403 |
any property is false whenever "hd []" occurs in it. |
|
404 |
||
405 |
These counterexample are marked as potentially spurious, as |
|
406 |
Quickcheck also returns "xs = []" as a counterexample to the |
|
407 |
obvious theorem "hd xs = hd xs". |
|
408 |
||
409 |
After finding a potentially spurious counterexample, Quickcheck |
|
410 |
continues searching for genuine ones. |
|
411 |
||
412 |
By default, Quickcheck shows potentially spurious and genuine |
|
413 |
counterexamples. The option "genuine_only" sets quickcheck to only |
|
414 |
show genuine counterexamples. |
|
415 |
||
416 |
- The command 'quickcheck_generator' creates random and exhaustive |
|
417 |
value generators for a given type and operations. |
|
418 |
||
419 |
It generates values by using the operations as if they were |
|
420 |
constructors of that type. |
|
421 |
||
422 |
- Support for multisets. |
|
423 |
||
424 |
- Added "use_subtype" options. |
|
425 |
||
426 |
- Added "quickcheck_locale" configuration to specify how to process |
|
427 |
conjectures in a locale context. |
|
428 |
||
47855 | 429 |
* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option |
430 |
and affecting 'rat' and 'real'. |
|
47809 | 431 |
|
432 |
* Sledgehammer: |
|
433 |
- Integrated more tightly with SPASS, as described in the ITP 2012 |
|
434 |
paper "More SPASS with Isabelle". |
|
435 |
- Made it try "smt" as a fallback if "metis" fails or times out. |
|
436 |
- Added support for the following provers: Alt-Ergo (via Why3 and |
|
437 |
TFF1), iProver, iProver-Eq. |
|
438 |
- Sped up the minimizer. |
|
439 |
- Added "lam_trans", "uncurry_aliases", and "minimize" options. |
|
440 |
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). |
|
441 |
- Renamed "sound" option to "strict". |
|
442 |
||
47855 | 443 |
* Metis: Added possibility to specify lambda translations scheme as a |
444 |
parenthesized argument (e.g., "by (metis (lifting) ...)"). |
|
445 |
||
446 |
* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates". |
|
447 |
||
448 |
* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY. |
|
47809 | 449 |
|
47856 | 450 |
* New "case_product" attribute to generate a case rule doing multiple |
451 |
case distinctions at the same time. E.g. |
|
452 |
||
453 |
list.exhaust [case_product nat.exhaust] |
|
454 |
||
455 |
produces a rule which can be used to perform case distinction on both |
|
456 |
a list and a nat. |
|
457 |
||
47809 | 458 |
* New "eventually_elim" method as a generalized variant of the |
47855 | 459 |
eventually_elim* rules. Supports structured proofs. |
460 |
||
47702
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
461 |
* Typedef with implicit set definition is considered legacy. Use |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
462 |
"typedef (open)" form instead, which will eventually become the |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
463 |
default. |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
464 |
|
47856 | 465 |
* Record: code generation can be switched off manually with |
466 |
||
467 |
declare [[record_coden = false]] -- "default true" |
|
468 |
||
469 |
* Datatype: type parameters allow explicit sort constraints. |
|
470 |
||
47855 | 471 |
* Concrete syntax for case expressions includes constraints for source |
472 |
positions, and thus produces Prover IDE markup for its bindings. |
|
473 |
INCOMPATIBILITY for old-style syntax translations that augment the |
|
474 |
pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
|
475 |
one_case. |
|
476 |
||
477 |
* Clarified attribute "mono_set": pure declaration without modifying |
|
478 |
the result of the fact expression. |
|
479 |
||
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
480 |
* More default pred/set conversions on a couple of relation operations |
47464 | 481 |
and predicates. Added powers of predicate relations. Consolidation |
482 |
of some relation theorems: |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
483 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
484 |
converse_def ~> converse_unfold |
47549 | 485 |
rel_comp_def ~> relcomp_unfold |
47820 | 486 |
symp_def ~> (modified, use symp_def and sym_def instead) |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
487 |
transp_def ~> transp_trans |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
488 |
Domain_def ~> Domain_unfold |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
489 |
Range_def ~> Domain_converse [symmetric] |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
490 |
|
46981 | 491 |
Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. |
492 |
||
47464 | 493 |
See theory "Relation" for examples for making use of pred/set |
494 |
conversions by means of attributes "to_set" and "to_pred". |
|
47086 | 495 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
496 |
INCOMPATIBILITY. |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
497 |
|
46363 | 498 |
* Renamed facts about the power operation on relations, i.e., relpow |
47464 | 499 |
to match the constant's name: |
47463 | 500 |
|
46458 | 501 |
rel_pow_1 ~> relpow_1 |
46363 | 502 |
rel_pow_0_I ~> relpow_0_I |
503 |
rel_pow_Suc_I ~> relpow_Suc_I |
|
504 |
rel_pow_Suc_I2 ~> relpow_Suc_I2 |
|
505 |
rel_pow_0_E ~> relpow_0_E |
|
506 |
rel_pow_Suc_E ~> relpow_Suc_E |
|
507 |
rel_pow_E ~> relpow_E |
|
46458 | 508 |
rel_pow_Suc_D2 ~> relpow_Suc_D2 |
47463 | 509 |
rel_pow_Suc_E2 ~> relpow_Suc_E2 |
46363 | 510 |
rel_pow_Suc_D2' ~> relpow_Suc_D2' |
511 |
rel_pow_E2 ~> relpow_E2 |
|
512 |
rel_pow_add ~> relpow_add |
|
513 |
rel_pow_commute ~> relpow |
|
514 |
rel_pow_empty ~> relpow_empty: |
|
515 |
rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow |
|
516 |
rel_pow_imp_rtrancl ~> relpow_imp_rtrancl |
|
517 |
rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow |
|
518 |
rtrancl_imp_rel_pow ~> rtrancl_imp_relpow |
|
519 |
rel_pow_fun_conv ~> relpow_fun_conv |
|
520 |
rel_pow_finite_bounded1 ~> relpow_finite_bounded1 |
|
521 |
rel_pow_finite_bounded ~> relpow_finite_bounded |
|
522 |
rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow |
|
523 |
trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow |
|
524 |
single_valued_rel_pow ~> single_valued_relpow |
|
47463 | 525 |
|
46363 | 526 |
INCOMPATIBILITY. |
527 |
||
47448 | 528 |
* Theory Relation: Consolidated constant name for relation composition |
47464 | 529 |
and corresponding theorem names: |
530 |
||
47549 | 531 |
- Renamed constant rel_comp to relcomp. |
47464 | 532 |
|
47448 | 533 |
- Dropped abbreviation pred_comp. Use relcompp instead. |
47464 | 534 |
|
47448 | 535 |
- Renamed theorems: |
47464 | 536 |
|
47448 | 537 |
rel_compI ~> relcompI |
538 |
rel_compEpair ~> relcompEpair |
|
539 |
rel_compE ~> relcompE |
|
540 |
pred_comp_rel_comp_eq ~> relcompp_relcomp_eq |
|
541 |
rel_comp_empty1 ~> relcomp_empty1 |
|
542 |
rel_comp_mono ~> relcomp_mono |
|
543 |
rel_comp_subset_Sigma ~> relcomp_subset_Sigma |
|
544 |
rel_comp_distrib ~> relcomp_distrib |
|
545 |
rel_comp_distrib2 ~> relcomp_distrib2 |
|
546 |
rel_comp_UNION_distrib ~> relcomp_UNION_distrib |
|
547 |
rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2 |
|
548 |
single_valued_rel_comp ~> single_valued_relcomp |
|
47549 | 549 |
rel_comp_def ~> relcomp_unfold |
47448 | 550 |
converse_rel_comp ~> converse_relcomp |
551 |
pred_compI ~> relcomppI |
|
552 |
pred_compE ~> relcomppE |
|
553 |
pred_comp_bot1 ~> relcompp_bot1 |
|
554 |
pred_comp_bot2 ~> relcompp_bot2 |
|
555 |
transp_pred_comp_less_eq ~> transp_relcompp_less_eq |
|
556 |
pred_comp_mono ~> relcompp_mono |
|
557 |
pred_comp_distrib ~> relcompp_distrib |
|
558 |
pred_comp_distrib2 ~> relcompp_distrib2 |
|
559 |
converse_pred_comp ~> converse_relcompp |
|
47464 | 560 |
|
47448 | 561 |
finite_rel_comp ~> finite_relcomp |
47464 | 562 |
|
47448 | 563 |
set_rel_comp ~> set_relcomp |
564 |
||
565 |
INCOMPATIBILITY. |
|
566 |
||
47550 | 567 |
* Theory Divides: Discontinued redundant theorems about div and mod. |
568 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
569 |
||
570 |
DIVISION_BY_ZERO ~> div_by_0, mod_by_0 |
|
571 |
zdiv_self ~> div_self |
|
572 |
zmod_self ~> mod_self |
|
573 |
zdiv_zero ~> div_0 |
|
574 |
zmod_zero ~> mod_0 |
|
575 |
zdiv_zmod_equality ~> div_mod_equality2 |
|
576 |
zdiv_zmod_equality2 ~> div_mod_equality |
|
577 |
zmod_zdiv_trivial ~> mod_div_trivial |
|
578 |
zdiv_zminus_zminus ~> div_minus_minus |
|
579 |
zmod_zminus_zminus ~> mod_minus_minus |
|
580 |
zdiv_zminus2 ~> div_minus_right |
|
581 |
zmod_zminus2 ~> mod_minus_right |
|
582 |
zdiv_minus1_right ~> div_minus1_right |
|
583 |
zmod_minus1_right ~> mod_minus1_right |
|
584 |
zdvd_mult_div_cancel ~> dvd_mult_div_cancel |
|
585 |
zmod_zmult1_eq ~> mod_mult_right_eq |
|
586 |
zpower_zmod ~> power_mod |
|
587 |
zdvd_zmod ~> dvd_mod |
|
588 |
zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd |
|
589 |
mod_mult_distrib ~> mult_mod_left |
|
590 |
mod_mult_distrib2 ~> mult_mod_right |
|
591 |
||
592 |
* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use |
|
593 |
generic mult_2 and mult_2_right instead. INCOMPATIBILITY. |
|
594 |
||
47551 | 595 |
* Finite_Set.fold now qualified. INCOMPATIBILITY. |
596 |
||
47552 | 597 |
* Consolidated theorem names concerning fold combinators: |
47550 | 598 |
|
599 |
inf_INFI_fold_inf ~> inf_INF_fold_inf |
|
600 |
sup_SUPR_fold_sup ~> sup_SUP_fold_sup |
|
601 |
INFI_fold_inf ~> INF_fold_inf |
|
602 |
SUPR_fold_sup ~> SUP_fold_sup |
|
603 |
union_set ~> union_set_fold |
|
604 |
minus_set ~> minus_set_fold |
|
605 |
INFI_set_fold ~> INF_set_fold |
|
606 |
SUPR_set_fold ~> SUP_set_fold |
|
607 |
INF_code ~> INF_set_foldr |
|
608 |
SUP_code ~> SUP_set_foldr |
|
609 |
foldr.simps ~> foldr.simps (in point-free formulation) |
|
610 |
foldr_fold_rev ~> foldr_conv_fold |
|
611 |
foldl_fold ~> foldl_conv_fold |
|
612 |
foldr_foldr ~> foldr_conv_foldl |
|
613 |
foldl_foldr ~> foldl_conv_foldr |
|
47552 | 614 |
fold_set_remdups ~> fold_set_fold_remdups |
615 |
fold_set ~> fold_set_fold |
|
616 |
fold1_set ~> fold1_set_fold |
|
47550 | 617 |
|
618 |
INCOMPATIBILITY. |
|
619 |
||
620 |
* Dropped rarely useful theorems concerning fold combinators: |
|
621 |
foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant, |
|
622 |
rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, |
|
623 |
concat_conv_foldl, foldl_weak_invariant, foldl_invariant, |
|
624 |
foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, |
|
625 |
listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, |
|
626 |
foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. |
|
627 |
INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" |
|
628 |
and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be |
|
629 |
useful to boil down "List.foldr" and "List.foldl" to "List.fold" by |
|
630 |
unfolding "foldr_conv_fold" and "foldl_conv_fold". |
|
631 |
||
632 |
* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, |
|
633 |
inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, |
|
634 |
Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr, |
|
635 |
INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding |
|
636 |
lemmas over fold rather than foldr, or make use of lemmas |
|
637 |
fold_conv_foldr and fold_rev. |
|
638 |
||
639 |
* Congruence rules Option.map_cong and Option.bind_cong for recursion |
|
640 |
through option types. |
|
641 |
||
47856 | 642 |
* "Transitive_Closure.ntrancl": bounded transitive closure on |
643 |
relations. |
|
644 |
||
645 |
* Constant "Set.not_member" now qualified. INCOMPATIBILITY. |
|
646 |
||
647 |
* Theory Int: Discontinued many legacy theorems specific to type int. |
|
648 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
649 |
||
650 |
zminus_zminus ~> minus_minus |
|
651 |
zminus_0 ~> minus_zero |
|
652 |
zminus_zadd_distrib ~> minus_add_distrib |
|
653 |
zadd_commute ~> add_commute |
|
654 |
zadd_assoc ~> add_assoc |
|
655 |
zadd_left_commute ~> add_left_commute |
|
656 |
zadd_ac ~> add_ac |
|
657 |
zmult_ac ~> mult_ac |
|
658 |
zadd_0 ~> add_0_left |
|
659 |
zadd_0_right ~> add_0_right |
|
660 |
zadd_zminus_inverse2 ~> left_minus |
|
661 |
zmult_zminus ~> mult_minus_left |
|
662 |
zmult_commute ~> mult_commute |
|
663 |
zmult_assoc ~> mult_assoc |
|
664 |
zadd_zmult_distrib ~> left_distrib |
|
665 |
zadd_zmult_distrib2 ~> right_distrib |
|
666 |
zdiff_zmult_distrib ~> left_diff_distrib |
|
667 |
zdiff_zmult_distrib2 ~> right_diff_distrib |
|
668 |
zmult_1 ~> mult_1_left |
|
669 |
zmult_1_right ~> mult_1_right |
|
670 |
zle_refl ~> order_refl |
|
671 |
zle_trans ~> order_trans |
|
672 |
zle_antisym ~> order_antisym |
|
673 |
zle_linear ~> linorder_linear |
|
674 |
zless_linear ~> linorder_less_linear |
|
675 |
zadd_left_mono ~> add_left_mono |
|
676 |
zadd_strict_right_mono ~> add_strict_right_mono |
|
677 |
zadd_zless_mono ~> add_less_le_mono |
|
678 |
int_0_less_1 ~> zero_less_one |
|
679 |
int_0_neq_1 ~> zero_neq_one |
|
680 |
zless_le ~> less_le |
|
681 |
zpower_zadd_distrib ~> power_add |
|
682 |
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
|
683 |
zero_le_zpower_abs ~> zero_le_power_abs |
|
684 |
||
685 |
* Theory Deriv: Renamed |
|
686 |
||
687 |
DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing |
|
688 |
||
689 |
* Theory Library/Multiset: Improved code generation of multisets. |
|
690 |
||
47855 | 691 |
* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets |
47703 | 692 |
are expressed via type classes again. The special syntax |
693 |
\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant |
|
694 |
setsum_set, which is now subsumed by Big_Operators.setsum. |
|
695 |
INCOMPATIBILITY. |
|
696 |
||
46160 | 697 |
* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, |
698 |
use theory HOL/Library/Nat_Bijection instead. |
|
699 |
||
47464 | 700 |
* Theory HOL/Library/RBT_Impl: Backing implementation of red-black |
701 |
trees is now inside a type class context. Names of affected |
|
702 |
operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for |
|
703 |
theories working directly with raw red-black trees, adapt the names as |
|
704 |
follows: |
|
47452 | 705 |
|
706 |
Operations: |
|
707 |
bulkload -> rbt_bulkload |
|
708 |
del_from_left -> rbt_del_from_left |
|
709 |
del_from_right -> rbt_del_from_right |
|
710 |
del -> rbt_del |
|
711 |
delete -> rbt_delete |
|
712 |
ins -> rbt_ins |
|
713 |
insert -> rbt_insert |
|
714 |
insertw -> rbt_insert_with |
|
715 |
insert_with_key -> rbt_insert_with_key |
|
716 |
map_entry -> rbt_map_entry |
|
717 |
lookup -> rbt_lookup |
|
718 |
sorted -> rbt_sorted |
|
719 |
tree_greater -> rbt_greater |
|
720 |
tree_less -> rbt_less |
|
721 |
tree_less_symbol -> rbt_less_symbol |
|
722 |
union -> rbt_union |
|
723 |
union_with -> rbt_union_with |
|
724 |
union_with_key -> rbt_union_with_key |
|
725 |
||
726 |
Lemmas: |
|
727 |
balance_left_sorted -> balance_left_rbt_sorted |
|
728 |
balance_left_tree_greater -> balance_left_rbt_greater |
|
729 |
balance_left_tree_less -> balance_left_rbt_less |
|
730 |
balance_right_sorted -> balance_right_rbt_sorted |
|
731 |
balance_right_tree_greater -> balance_right_rbt_greater |
|
732 |
balance_right_tree_less -> balance_right_rbt_less |
|
733 |
balance_sorted -> balance_rbt_sorted |
|
734 |
balance_tree_greater -> balance_rbt_greater |
|
735 |
balance_tree_less -> balance_rbt_less |
|
736 |
bulkload_is_rbt -> rbt_bulkload_is_rbt |
|
737 |
combine_sorted -> combine_rbt_sorted |
|
738 |
combine_tree_greater -> combine_rbt_greater |
|
739 |
combine_tree_less -> combine_rbt_less |
|
740 |
delete_in_tree -> rbt_delete_in_tree |
|
741 |
delete_is_rbt -> rbt_delete_is_rbt |
|
742 |
del_from_left_tree_greater -> rbt_del_from_left_rbt_greater |
|
743 |
del_from_left_tree_less -> rbt_del_from_left_rbt_less |
|
744 |
del_from_right_tree_greater -> rbt_del_from_right_rbt_greater |
|
745 |
del_from_right_tree_less -> rbt_del_from_right_rbt_less |
|
746 |
del_in_tree -> rbt_del_in_tree |
|
747 |
del_inv1_inv2 -> rbt_del_inv1_inv2 |
|
748 |
del_sorted -> rbt_del_rbt_sorted |
|
749 |
del_tree_greater -> rbt_del_rbt_greater |
|
750 |
del_tree_less -> rbt_del_rbt_less |
|
751 |
dom_lookup_Branch -> dom_rbt_lookup_Branch |
|
752 |
entries_lookup -> entries_rbt_lookup |
|
753 |
finite_dom_lookup -> finite_dom_rbt_lookup |
|
754 |
insert_sorted -> rbt_insert_rbt_sorted |
|
755 |
insertw_is_rbt -> rbt_insertw_is_rbt |
|
756 |
insertwk_is_rbt -> rbt_insertwk_is_rbt |
|
757 |
insertwk_sorted -> rbt_insertwk_rbt_sorted |
|
758 |
insertw_sorted -> rbt_insertw_rbt_sorted |
|
759 |
ins_sorted -> ins_rbt_sorted |
|
760 |
ins_tree_greater -> ins_rbt_greater |
|
761 |
ins_tree_less -> ins_rbt_less |
|
762 |
is_rbt_sorted -> is_rbt_rbt_sorted |
|
763 |
lookup_balance -> rbt_lookup_balance |
|
764 |
lookup_bulkload -> rbt_lookup_rbt_bulkload |
|
765 |
lookup_delete -> rbt_lookup_rbt_delete |
|
766 |
lookup_Empty -> rbt_lookup_Empty |
|
767 |
lookup_from_in_tree -> rbt_lookup_from_in_tree |
|
768 |
lookup_in_tree -> rbt_lookup_in_tree |
|
769 |
lookup_ins -> rbt_lookup_ins |
|
770 |
lookup_insert -> rbt_lookup_rbt_insert |
|
771 |
lookup_insertw -> rbt_lookup_rbt_insertw |
|
772 |
lookup_insertwk -> rbt_lookup_rbt_insertwk |
|
773 |
lookup_keys -> rbt_lookup_keys |
|
774 |
lookup_map -> rbt_lookup_map |
|
775 |
lookup_map_entry -> rbt_lookup_rbt_map_entry |
|
776 |
lookup_tree_greater -> rbt_lookup_rbt_greater |
|
777 |
lookup_tree_less -> rbt_lookup_rbt_less |
|
778 |
lookup_union -> rbt_lookup_rbt_union |
|
779 |
map_entry_color_of -> rbt_map_entry_color_of |
|
780 |
map_entry_inv1 -> rbt_map_entry_inv1 |
|
781 |
map_entry_inv2 -> rbt_map_entry_inv2 |
|
782 |
map_entry_is_rbt -> rbt_map_entry_is_rbt |
|
783 |
map_entry_sorted -> rbt_map_entry_rbt_sorted |
|
784 |
map_entry_tree_greater -> rbt_map_entry_rbt_greater |
|
785 |
map_entry_tree_less -> rbt_map_entry_rbt_less |
|
786 |
map_tree_greater -> map_rbt_greater |
|
787 |
map_tree_less -> map_rbt_less |
|
788 |
map_sorted -> map_rbt_sorted |
|
789 |
paint_sorted -> paint_rbt_sorted |
|
790 |
paint_lookup -> paint_rbt_lookup |
|
791 |
paint_tree_greater -> paint_rbt_greater |
|
792 |
paint_tree_less -> paint_rbt_less |
|
793 |
sorted_entries -> rbt_sorted_entries |
|
794 |
tree_greater_eq_trans -> rbt_greater_eq_trans |
|
795 |
tree_greater_nit -> rbt_greater_nit |
|
796 |
tree_greater_prop -> rbt_greater_prop |
|
797 |
tree_greater_simps -> rbt_greater_simps |
|
798 |
tree_greater_trans -> rbt_greater_trans |
|
799 |
tree_less_eq_trans -> rbt_less_eq_trans |
|
800 |
tree_less_nit -> rbt_less_nit |
|
801 |
tree_less_prop -> rbt_less_prop |
|
802 |
tree_less_simps -> rbt_less_simps |
|
803 |
tree_less_trans -> rbt_less_trans |
|
804 |
tree_ord_props -> rbt_ord_props |
|
805 |
union_Branch -> rbt_union_Branch |
|
806 |
union_is_rbt -> rbt_union_is_rbt |
|
807 |
unionw_is_rbt -> rbt_unionw_is_rbt |
|
808 |
unionwk_is_rbt -> rbt_unionwk_is_rbt |
|
809 |
unionwk_sorted -> rbt_unionwk_rbt_sorted |
|
810 |
||
47807 | 811 |
* Theory HOL/Library/Float: Floating point numbers are now defined as |
812 |
a subset of the real numbers. All operations are defined using the |
|
813 |
lifing-framework and proofs use the transfer method. INCOMPATIBILITY. |
|
47616 | 814 |
|
815 |
Changed Operations: |
|
47622 | 816 |
float_abs -> abs |
817 |
float_nprt -> nprt |
|
818 |
float_pprt -> pprt |
|
819 |
pow2 -> use powr |
|
820 |
round_down -> float_round_down |
|
821 |
round_up -> float_round_up |
|
822 |
scale -> exponent |
|
823 |
||
824 |
Removed Operations: |
|
825 |
ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod |
|
826 |
||
827 |
Renamed Lemmas: |
|
828 |
abs_float_def -> Float.compute_float_abs |
|
829 |
bitlen_ge0 -> bitlen_nonneg |
|
830 |
bitlen.simps -> Float.compute_bitlen |
|
831 |
float_components -> Float_mantissa_exponent |
|
832 |
float_divl.simps -> Float.compute_float_divl |
|
833 |
float_divr.simps -> Float.compute_float_divr |
|
834 |
float_eq_odd -> mult_powr_eq_mult_powr_iff |
|
835 |
float_power -> real_of_float_power |
|
836 |
lapprox_posrat_def -> Float.compute_lapprox_posrat |
|
837 |
lapprox_rat.simps -> Float.compute_lapprox_rat |
|
838 |
le_float_def' -> Float.compute_float_le |
|
839 |
le_float_def -> less_eq_float.rep_eq |
|
840 |
less_float_def' -> Float.compute_float_less |
|
841 |
less_float_def -> less_float.rep_eq |
|
842 |
normfloat_def -> Float.compute_normfloat |
|
843 |
normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0 |
|
844 |
normfloat -> normfloat_def |
|
845 |
normfloat_unique -> use normfloat_def |
|
846 |
number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral |
|
847 |
one_float_def -> Float.compute_float_one |
|
848 |
plus_float_def -> Float.compute_float_plus |
|
849 |
rapprox_posrat_def -> Float.compute_rapprox_posrat |
|
850 |
rapprox_rat.simps -> Float.compute_rapprox_rat |
|
851 |
real_of_float_0 -> zero_float.rep_eq |
|
852 |
real_of_float_1 -> one_float.rep_eq |
|
853 |
real_of_float_abs -> abs_float.rep_eq |
|
854 |
real_of_float_add -> plus_float.rep_eq |
|
855 |
real_of_float_minus -> uminus_float.rep_eq |
|
856 |
real_of_float_mult -> times_float.rep_eq |
|
857 |
real_of_float_simp -> Float.rep_eq |
|
858 |
real_of_float_sub -> minus_float.rep_eq |
|
859 |
round_down.simps -> Float.compute_float_round_down |
|
860 |
round_up.simps -> Float.compute_float_round_up |
|
861 |
times_float_def -> Float.compute_float_times |
|
862 |
uminus_float_def -> Float.compute_float_uminus |
|
863 |
zero_float_def -> Float.compute_float_zero |
|
864 |
||
865 |
Lemmas not necessary anymore, use the transfer method: |
|
866 |
bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl, |
|
867 |
float_divr, float_le_simp, float_less1_mantissa_bound, |
|
868 |
float_less_simp, float_less_zero, float_le_zero, |
|
869 |
float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2, |
|
870 |
floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat, |
|
871 |
lapprox_rat_bottom, normalized_float, rapprox_posrat, |
|
872 |
rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp, |
|
873 |
real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl, |
|
874 |
round_up, zero_le_float, zero_less_float |
|
47616 | 875 |
|
47856 | 876 |
* New theory HOL/Library/DAList provides an abstract type for |
877 |
association lists with distinct keys. |
|
45791 | 878 |
|
47866 | 879 |
* Session HOL/IMP: Added new theory of abstract interpretation of |
880 |
annotated commands. |
|
881 |
||
47855 | 882 |
* Session HOL-Import: Re-implementation from scratch is faster, |
883 |
simpler, and more scalable. Requires a proof bundle, which is |
|
884 |
available as an external component. Discontinued old (and mostly |
|
885 |
dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY. |
|
886 |
||
887 |
* Session HOL-Word: Discontinued many redundant theorems specific to |
|
888 |
type 'a word. INCOMPATIBILITY, use the corresponding generic theorems |
|
889 |
instead. |
|
890 |
||
891 |
word_sub_alt ~> word_sub_wi |
|
892 |
word_add_alt ~> word_add_def |
|
893 |
word_mult_alt ~> word_mult_def |
|
894 |
word_minus_alt ~> word_minus_def |
|
895 |
word_0_alt ~> word_0_wi |
|
896 |
word_1_alt ~> word_1_wi |
|
897 |
word_add_0 ~> add_0_left |
|
898 |
word_add_0_right ~> add_0_right |
|
899 |
word_mult_1 ~> mult_1_left |
|
900 |
word_mult_1_right ~> mult_1_right |
|
901 |
word_add_commute ~> add_commute |
|
902 |
word_add_assoc ~> add_assoc |
|
903 |
word_add_left_commute ~> add_left_commute |
|
904 |
word_mult_commute ~> mult_commute |
|
905 |
word_mult_assoc ~> mult_assoc |
|
906 |
word_mult_left_commute ~> mult_left_commute |
|
907 |
word_left_distrib ~> left_distrib |
|
908 |
word_right_distrib ~> right_distrib |
|
909 |
word_left_minus ~> left_minus |
|
910 |
word_diff_0_right ~> diff_0_right |
|
911 |
word_diff_self ~> diff_self |
|
912 |
word_sub_def ~> diff_minus |
|
913 |
word_diff_minus ~> diff_minus |
|
914 |
word_add_ac ~> add_ac |
|
915 |
word_mult_ac ~> mult_ac |
|
916 |
word_plus_ac0 ~> add_0_left add_0_right add_ac |
|
917 |
word_times_ac1 ~> mult_1_left mult_1_right mult_ac |
|
918 |
word_order_trans ~> order_trans |
|
919 |
word_order_refl ~> order_refl |
|
920 |
word_order_antisym ~> order_antisym |
|
921 |
word_order_linear ~> linorder_linear |
|
922 |
lenw1_zero_neq_one ~> zero_neq_one |
|
923 |
word_number_of_eq ~> number_of_eq |
|
924 |
word_of_int_add_hom ~> wi_hom_add |
|
925 |
word_of_int_sub_hom ~> wi_hom_sub |
|
926 |
word_of_int_mult_hom ~> wi_hom_mult |
|
927 |
word_of_int_minus_hom ~> wi_hom_neg |
|
928 |
word_of_int_succ_hom ~> wi_hom_succ |
|
929 |
word_of_int_pred_hom ~> wi_hom_pred |
|
930 |
word_of_int_0_hom ~> word_0_wi |
|
931 |
word_of_int_1_hom ~> word_1_wi |
|
932 |
||
47809 | 933 |
* Session HOL-Word: New proof method "word_bitwise" for splitting |
934 |
machine word equalities and inequalities into logical circuits, |
|
935 |
defined in HOL/Word/WordBitwise.thy. Supports addition, subtraction, |
|
936 |
multiplication, shifting by constants, bitwise operators and numeric |
|
937 |
constants. Requires fixed-length word types, not 'a word. Solves |
|
47854 | 938 |
many standard word identities outright and converts more into first |
47809 | 939 |
order problems amenable to blast or similar. See also examples in |
940 |
HOL/Word/Examples/WordExamples.thy. |
|
941 |
||
47807 | 942 |
* Session HOL-Probability: Introduced the type "'a measure" to |
943 |
represent measures, this replaces the records 'a algebra and 'a |
|
944 |
measure_space. The locales based on subset_class now have two |
|
47856 | 945 |
locale-parameters the space \<Omega> and the set of measurable sets M. |
946 |
The product of probability spaces uses now the same constant as the |
|
947 |
finite product of sigma-finite measure spaces "PiM :: ('i => 'a) |
|
47807 | 948 |
measure". Most constants are defined now outside of locales and gain |
949 |
an additional parameter, like null_sets, almost_eventually or \<mu>'. |
|
950 |
Measure space constructions for distributions and densities now got |
|
951 |
their own constants distr and density. Instead of using locales to |
|
952 |
describe measure spaces with a finite space, the measure count_space |
|
953 |
and point_measure is introduced. INCOMPATIBILITY. |
|
47694 | 954 |
|
955 |
Renamed constants: |
|
956 |
measure -> emeasure |
|
957 |
finite_measure.\<mu>' -> measure |
|
958 |
product_algebra_generator -> prod_algebra |
|
959 |
product_prob_space.emb -> prod_emb |
|
960 |
product_prob_space.infprod_algebra -> PiM |
|
961 |
||
962 |
Removed locales: |
|
963 |
completeable_measure_space |
|
964 |
finite_measure_space |
|
965 |
finite_prob_space |
|
966 |
finite_product_finite_prob_space |
|
967 |
finite_product_sigma_algebra |
|
968 |
finite_sigma_algebra |
|
969 |
measure_space |
|
970 |
pair_finite_prob_space |
|
971 |
pair_finite_sigma_algebra |
|
972 |
pair_finite_space |
|
973 |
pair_sigma_algebra |
|
974 |
product_sigma_algebra |
|
975 |
||
976 |
Removed constants: |
|
47751 | 977 |
conditional_space |
47694 | 978 |
distribution -> use distr measure, or distributed predicate |
47751 | 979 |
image_space |
47694 | 980 |
joint_distribution -> use distr measure, or distributed predicate |
47751 | 981 |
pair_measure_generator |
47694 | 982 |
product_prob_space.infprod_algebra -> use PiM |
983 |
subvimage |
|
984 |
||
985 |
Replacement theorems: |
|
47751 | 986 |
finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite |
987 |
finite_measure.empty_measure -> measure_empty |
|
988 |
finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq |
|
989 |
finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq |
|
990 |
finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably |
|
991 |
finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure |
|
992 |
finite_measure.finite_measure -> finite_measure.emeasure_finite |
|
993 |
finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton |
|
994 |
finite_measure.positive_measure' -> measure_nonneg |
|
995 |
finite_measure.real_measure -> finite_measure.emeasure_real |
|
996 |
finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb |
|
997 |
finite_product_sigma_algebra.in_P -> sets_PiM_I_finite |
|
998 |
finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty |
|
999 |
information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed |
|
1000 |
information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple |
|
1001 |
information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple |
|
1002 |
information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple |
|
1003 |
information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple |
|
1004 |
information_space.entropy_commute -> information_space.entropy_commute_simple |
|
1005 |
information_space.entropy_eq -> information_space.entropy_simple_distributed |
|
1006 |
information_space.entropy_generic_eq -> information_space.entropy_simple_distributed |
|
1007 |
information_space.entropy_positive -> information_space.entropy_nonneg_simple |
|
1008 |
information_space.entropy_uniform_max -> information_space.entropy_uniform |
|
1009 |
information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq |
|
1010 |
information_space.KL_eq_0 -> information_space.KL_same_eq_0 |
|
1011 |
information_space.KL_ge_0 -> information_space.KL_nonneg |
|
1012 |
information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed |
|
1013 |
information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple |
|
1014 |
Int_stable_cuboids -> Int_stable_atLeastAtMost |
|
1015 |
Int_stable_product_algebra_generator -> positive_integral |
|
1016 |
measure_preserving -> equality "distr M N f = N" "f : measurable M N" |
|
47694 | 1017 |
measure_space.additive -> emeasure_additive |
47751 | 1018 |
measure_space.AE_iff_null_set -> AE_iff_null |
1019 |
measure_space.almost_everywhere_def -> eventually_ae_filter |
|
1020 |
measure_space.almost_everywhere_vimage -> AE_distrD |
|
1021 |
measure_space.continuity_from_above -> INF_emeasure_decseq |
|
1022 |
measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq |
|
1023 |
measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq |
|
47694 | 1024 |
measure_space.continuity_from_below -> SUP_emeasure_incseq |
47751 | 1025 |
measure_space_density -> emeasure_density |
1026 |
measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density |
|
1027 |
measure_space.integrable_vimage -> integrable_distr |
|
1028 |
measure_space.integral_translated_density -> integral_density |
|
1029 |
measure_space.integral_vimage -> integral_distr |
|
1030 |
measure_space.measure_additive -> plus_emeasure |
|
1031 |
measure_space.measure_compl -> emeasure_compl |
|
1032 |
measure_space.measure_countable_increasing -> emeasure_countable_increasing |
|
1033 |
measure_space.measure_countably_subadditive -> emeasure_subadditive_countably |
|
47694 | 1034 |
measure_space.measure_decseq -> decseq_emeasure |
47751 | 1035 |
measure_space.measure_Diff -> emeasure_Diff |
1036 |
measure_space.measure_Diff_null_set -> emeasure_Diff_null_set |
|
47694 | 1037 |
measure_space.measure_eq_0 -> emeasure_eq_0 |
1038 |
measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite |
|
47751 | 1039 |
measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton |
1040 |
measure_space.measure_incseq -> incseq_emeasure |
|
1041 |
measure_space.measure_insert -> emeasure_insert |
|
1042 |
measure_space.measure_mono -> emeasure_mono |
|
1043 |
measure_space.measure_not_negative -> emeasure_not_MInf |
|
1044 |
measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq |
|
1045 |
measure_space.measure_setsum -> setsum_emeasure |
|
1046 |
measure_space.measure_setsum_split -> setsum_emeasure_cover |
|
47694 | 1047 |
measure_space.measure_space_vimage -> emeasure_distr |
47751 | 1048 |
measure_space.measure_subadditive_finite -> emeasure_subadditive_finite |
1049 |
measure_space.measure_subadditive -> subadditive |
|
1050 |
measure_space.measure_top -> emeasure_space |
|
1051 |
measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0 |
|
1052 |
measure_space.measure_Un_null_set -> emeasure_Un_null_set |
|
1053 |
measure_space.positive_integral_translated_density -> positive_integral_density |
|
1054 |
measure_space.positive_integral_vimage -> positive_integral_distr |
|
47694 | 1055 |
measure_space.real_continuity_from_above -> Lim_measure_decseq |
47751 | 1056 |
measure_space.real_continuity_from_below -> Lim_measure_incseq |
47694 | 1057 |
measure_space.real_measure_countably_subadditive -> measure_subadditive_countably |
47751 | 1058 |
measure_space.real_measure_Diff -> measure_Diff |
1059 |
measure_space.real_measure_finite_Union -> measure_finite_Union |
|
1060 |
measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton |
|
1061 |
measure_space.real_measure_subadditive -> measure_subadditive |
|
1062 |
measure_space.real_measure_Union -> measure_Union |
|
1063 |
measure_space.real_measure_UNION -> measure_UNION |
|
47694 | 1064 |
measure_space.simple_function_vimage -> simple_function_comp |
1065 |
measure_space.simple_integral_vimage -> simple_integral_distr |
|
47751 | 1066 |
measure_space.simple_integral_vimage -> simple_integral_distr |
1067 |
measure_unique_Int_stable -> measure_eqI_generator_eq |
|
1068 |
measure_unique_Int_stable_vimage -> measure_eqI_generator_eq |
|
47694 | 1069 |
pair_sigma_algebra.measurable_cut_fst -> sets_Pair1 |
1070 |
pair_sigma_algebra.measurable_cut_snd -> sets_Pair2 |
|
1071 |
pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1 |
|
1072 |
pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2 |
|
1073 |
pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff |
|
1074 |
pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap |
|
1075 |
pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap' |
|
1076 |
pair_sigma_algebra.sets_swap -> sets_pair_swap |
|
47751 | 1077 |
pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1 |
1078 |
pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2 |
|
1079 |
pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap |
|
1080 |
pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2 |
|
1081 |
pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt |
|
1082 |
pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times |
|
1083 |
prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM |
|
1084 |
prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq |
|
47694 | 1085 |
prob_space.measure_space_1 -> prob_space.emeasure_space_1 |
1086 |
prob_space.prob_space_vimage -> prob_space_distr |
|
1087 |
prob_space.random_variable_restrict -> measurable_restrict |
|
47751 | 1088 |
prob_space_unique_Int_stable -> measure_eqI_prob_space |
1089 |
product_algebraE -> prod_algebraE_all |
|
1090 |
product_algebra_generator_der -> prod_algebra_eq_finite |
|
1091 |
product_algebra_generator_into_space -> prod_algebra_sets_into_space |
|
1092 |
product_algebraI -> sets_PiM_I_finite |
|
1093 |
product_measure_exists -> product_sigma_finite.sigma_finite |
|
47694 | 1094 |
product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator |
1095 |
product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb |
|
1096 |
product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty |
|
1097 |
product_prob_space.measurable_component -> measurable_component_singleton |
|
1098 |
product_prob_space.measurable_emb -> measurable_prod_emb |
|
1099 |
product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single |
|
1100 |
product_prob_space.measurable_singleton_infprod -> measurable_component_singleton |
|
1101 |
product_prob_space.measure_emb -> emeasure_prod_emb |
|
47751 | 1102 |
product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict |
1103 |
product_sigma_algebra.product_algebra_into_space -> space_closed |
|
1104 |
product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge |
|
1105 |
product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton |
|
1106 |
product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge |
|
47694 | 1107 |
sequence_space.measure_infprod -> sequence_space.measure_PiM_countable |
47751 | 1108 |
sets_product_algebra -> sets_PiM |
1109 |
sigma_algebra.measurable_sigma -> measurable_measure_of |
|
1110 |
sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint |
|
1111 |
sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr |
|
1112 |
sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq |
|
1113 |
space_product_algebra -> space_PiM |
|
47694 | 1114 |
|
47855 | 1115 |
* Session HOL-TPTP: support to parse and import TPTP problems (all |
1116 |
languages) into Isabelle/HOL. |
|
47413 | 1117 |
|
45398
7dbb7b044a11
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
blanchet
parents:
45384
diff
changeset
|
1118 |
|
45160 | 1119 |
*** FOL *** |
1120 |
||
45383 | 1121 |
* New "case_product" attribute (see HOL). |
45160 | 1122 |
|
45109 | 1123 |
|
47463 | 1124 |
*** ZF *** |
1125 |
||
1126 |
* Greater support for structured proofs involving induction or case |
|
1127 |
analysis. |
|
1128 |
||
1129 |
* Much greater use of mathematical symbols. |
|
1130 |
||
1131 |
* Removal of many ML theorem bindings. INCOMPATIBILITY. |
|
1132 |
||
1133 |
||
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1134 |
*** ML *** |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1135 |
|
46948 | 1136 |
* Antiquotation @{keyword "name"} produces a parser for outer syntax |
1137 |
from a minor keyword introduced via theory header declaration. |
|
1138 |
||
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
1139 |
* Antiquotation @{command_spec "name"} produces the |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
1140 |
Outer_Syntax.command_spec from a major keyword introduced via theory |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
1141 |
header declaration; it can be passed to Outer_Syntax.command etc. |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
1142 |
|
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
46903
diff
changeset
|
1143 |
* Local_Theory.define no longer hard-wires default theorem name |
46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1144 |
"foo_def", but retains the binding as given. If that is Binding.empty |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1145 |
/ Attrib.empty_binding, the result is not registered as user-level |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1146 |
fact. The Local_Theory.define_internal variant allows to specify a |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1147 |
non-empty name (used for the foundation in the background theory), |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1148 |
while omitting the fact binding in the user-context. Potential |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1149 |
INCOMPATIBILITY for derived definitional packages: need to specify |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
1150 |
naming policy for primitive definitions more explicitly. |
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
46903
diff
changeset
|
1151 |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
1152 |
* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
1153 |
conformance with similar operations in structure Term and Logic. |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
1154 |
|
45592 | 1155 |
* Antiquotation @{attributes [...]} embeds attribute source |
1156 |
representation into the ML text, which is particularly useful with |
|
1157 |
declarations like Local_Theory.note. |
|
1158 |
||
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1159 |
* Structure Proof_Context follows standard naming scheme. Old |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1160 |
ProofContext has been discontinued. INCOMPATIBILITY. |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1161 |
|
45293
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
1162 |
* Refined Local_Theory.declaration {syntax, pervasive}, with subtle |
45298
aa35859c8741
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
wenzelm
parents:
45293
diff
changeset
|
1163 |
change of semantics: update is applied to auxiliary local theory |
45293
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
1164 |
context as well. |
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
1165 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1166 |
* Modernized some old-style infix operations: |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1167 |
|
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1168 |
addeqcongs ~> Simplifier.add_eqcong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1169 |
deleqcongs ~> Simplifier.del_eqcong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1170 |
addcongs ~> Simplifier.add_cong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1171 |
delcongs ~> Simplifier.del_cong |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1172 |
setmksimps ~> Simplifier.set_mksimps |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1173 |
setmkcong ~> Simplifier.set_mkcong |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1174 |
setmksym ~> Simplifier.set_mksym |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1175 |
setmkeqTrue ~> Simplifier.set_mkeqTrue |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1176 |
settermless ~> Simplifier.set_termless |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
1177 |
setsubgoaler ~> Simplifier.set_subgoaler |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1178 |
addsplits ~> Splitter.add_split |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1179 |
delsplits ~> Splitter.del_split |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
1180 |
|
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
1181 |
|
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
1182 |
*** System *** |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
1183 |
|
47661
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1184 |
* USER_HOME settings variable points to cross-platform user home |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1185 |
directory, which coincides with HOME on POSIX systems only. Likewise, |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1186 |
the Isabelle path specification "~" now expands to $USER_HOME, instead |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1187 |
of former $HOME. A different default for USER_HOME may be set |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1188 |
explicitly in shell environment, before Isabelle settings are |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1189 |
evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1190 |
the generic user home was intended. |
012a887997f3
USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents:
47659
diff
changeset
|
1191 |
|
47807 | 1192 |
* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name |
1193 |
notation, which is useful for the jEdit file browser, for example. |
|
1194 |
||
47464 | 1195 |
* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar |
1196 |
(not just JRE). |
|
1197 |
||
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
1198 |
|
45109 | 1199 |
|
44801 | 1200 |
New in Isabelle2011-1 (October 2011) |
1201 |
------------------------------------ |
|
41651 | 1202 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1203 |
*** General *** |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1204 |
|
44760 | 1205 |
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as |
44968 | 1206 |
"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line. |
44760 | 1207 |
|
44777 | 1208 |
- Management of multiple theory files directly from the editor |
44760 | 1209 |
buffer store -- bypassing the file-system (no requirement to save |
1210 |
files for checking). |
|
1211 |
||
44777 | 1212 |
- Markup of formal entities within the text buffer, with semantic |
44760 | 1213 |
highlighting, tooltips and hyperlinks to jump to defining source |
1214 |
positions. |
|
1215 |
||
44777 | 1216 |
- Improved text rendering, with sub/superscripts in the source |
1217 |
buffer (including support for copy/paste wrt. output panel, HTML |
|
1218 |
theory output and other non-Isabelle text boxes). |
|
1219 |
||
1220 |
- Refined scheduling of proof checking and printing of results, |
|
44760 | 1221 |
based on interactive editor view. (Note: jEdit folding and |
1222 |
narrowing allows to restrict buffer perspectives explicitly.) |
|
1223 |
||
44777 | 1224 |
- Reduced CPU performance requirements, usable on machines with few |
44760 | 1225 |
cores. |
1226 |
||
44777 | 1227 |
- Reduced memory requirements due to pruning of unused document |
44760 | 1228 |
versions (garbage collection). |
1229 |
||
1230 |
See also ~~/src/Tools/jEdit/README.html for further information, |
|
1231 |
including some remaining limitations. |
|
1232 |
||
44800 | 1233 |
* Theory loader: source files are exclusively located via the master |
1234 |
directory of each theory node (where the .thy file itself resides). |
|
1235 |
The global load path (such as src/HOL/Library) has been discontinued. |
|
1236 |
Note that the path element ~~ may be used to reference theories in the |
|
1237 |
Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". |
|
1238 |
INCOMPATIBILITY. |
|
1239 |
||
41955
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
1240 |
* Theory loader: source files are identified by content via SHA1 |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
1241 |
digests. Discontinued former path/modtime identification and optional |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
1242 |
ISABELLE_FILE_IDENT plugin scripts. |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
1243 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1244 |
* Parallelization of nested Isar proofs is subject to |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1245 |
Goal.parallel_proofs_threshold (default 100). See also isabelle |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1246 |
usedir option -Q. |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1247 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1248 |
* Name space: former unsynchronized references are now proper |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1249 |
configuration options, with more conventional names: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1250 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1251 |
long_names ~> names_long |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1252 |
short_names ~> names_short |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1253 |
unique_names ~> names_unique |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1254 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1255 |
Minor INCOMPATIBILITY, need to declare options in context like this: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1256 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
1257 |
declare [[names_unique = false]] |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42290
diff
changeset
|
1258 |
|
42502 | 1259 |
* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note |
1260 |
that the result needs to be unique, which means fact specifications |
|
1261 |
may have to be refined after enriching a proof context. |
|
1262 |
||
44800 | 1263 |
* Attribute "case_names" has been refined: the assumptions in each case |
1264 |
can be named now by following the case name with [name1 name2 ...]. |
|
1265 |
||
44968 | 1266 |
* Isabelle/Isar reference manual has been updated and extended: |
1267 |
- "Synopsis" provides a catalog of main Isar language concepts. |
|
1268 |
- Formal references in syntax diagrams, via @{rail} antiquotation. |
|
1269 |
- Updated material from classic "ref" manual, notably about |
|
1270 |
"Classical Reasoner". |
|
42633 | 1271 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1272 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
1273 |
*** HOL *** |
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
1274 |
|
44968 | 1275 |
* Class bot and top require underlying partial order rather than |
44800 | 1276 |
preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
43752
diff
changeset
|
1277 |
|
43940 | 1278 |
* Class complete_lattice: generalized a couple of lemmas from sets; |
44800 | 1279 |
generalized theorems INF_cong and SUP_cong. New type classes for |
1280 |
complete boolean algebras and complete linear orders. Lemmas |
|
1281 |
Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in |
|
1282 |
class complete_linorder. |
|
1283 |
||
1284 |
Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
|
1285 |
Sup_fun_def, Inf_apply, Sup_apply. |
|
1286 |
||
45088 | 1287 |
Removed redundant lemmas (the right hand side gives hints how to |
1288 |
replace them for (metis ...), or (simp only: ...) proofs): |
|
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1289 |
|
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1290 |
Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1291 |
Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1292 |
Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1293 |
Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1294 |
Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1295 |
Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1296 |
Inter_def ~> INF_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1297 |
Union_def ~> SUP_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1298 |
INT_eq ~> INF_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1299 |
UN_eq ~> SUP_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1300 |
INF_subset ~> INF_superset_mono [OF _ order_refl] |
44800 | 1301 |
|
1302 |
More consistent and comprehensive names: |
|
1303 |
||
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1304 |
INTER_eq_Inter_image ~> INF_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
1305 |
UNION_eq_Union_image ~> SUP_def |
43872 | 1306 |
INFI_def ~> INF_def |
1307 |
SUPR_def ~> SUP_def |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1308 |
INF_leI ~> INF_lower |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1309 |
INF_leI2 ~> INF_lower2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1310 |
le_INFI ~> INF_greatest |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1311 |
le_SUPI ~> SUP_upper |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1312 |
le_SUPI2 ~> SUP_upper2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1313 |
SUP_leI ~> SUP_least |
43873 | 1314 |
INFI_bool_eq ~> INF_bool_eq |
1315 |
SUPR_bool_eq ~> SUP_bool_eq |
|
1316 |
INFI_apply ~> INF_apply |
|
1317 |
SUPR_apply ~> SUP_apply |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1318 |
INTER_def ~> INTER_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1319 |
UNION_def ~> UNION_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
1320 |
|
43865
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
1321 |
INCOMPATIBILITY. |
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
1322 |
|
44973
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1323 |
* Renamed theory Complete_Lattice to Complete_Lattices. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1324 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1325 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1326 |
* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1327 |
INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1328 |
Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1329 |
Sup_insert are now declared as [simp]. INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1330 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1331 |
* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1332 |
compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1333 |
sup_inf_absob, sup_left_idem are now declared as [simp]. Minor |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1334 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
1335 |
|
44845 | 1336 |
* Added syntactic classes "inf" and "sup" for the respective |
1337 |
constants. INCOMPATIBILITY: Changes in the argument order of the |
|
1338 |
(mostly internal) locale predicates for some derived classes. |
|
1339 |
||
44800 | 1340 |
* Theorem collections ball_simps and bex_simps do not contain theorems |
1341 |
referring to UNION any longer; these have been moved to collection |
|
1342 |
UN_ball_bex_simps. INCOMPATIBILITY. |
|
1343 |
||
1344 |
* Theory Archimedean_Field: floor now is defined as parameter of a |
|
1345 |
separate type class floor_ceiling. |
|
1346 |
||
1347 |
* Theory Finite_Set: more coherent development of fold_set locales: |
|
42874 | 1348 |
|
1349 |
locale fun_left_comm ~> locale comp_fun_commute |
|
1350 |
locale fun_left_comm_idem ~> locale comp_fun_idem |
|
44800 | 1351 |
|
1352 |
Both use point-free characterization; interpretation proofs may need |
|
1353 |
adjustment. INCOMPATIBILITY. |
|
42874 | 1354 |
|
44800 | 1355 |
* Theory Limits: Type "'a net" has been renamed to "'a filter", in |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
1356 |
accordance with standard mathematical terminology. INCOMPATIBILITY. |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
1357 |
|
44800 | 1358 |
* Theory Complex_Main: The locale interpretations for the |
1359 |
bounded_linear and bounded_bilinear locales have been removed, in |
|
1360 |
order to reduce the number of duplicate lemmas. Users must use the |
|
1361 |
original names for distributivity theorems, potential INCOMPATIBILITY. |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1362 |
|
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1363 |
divide.add ~> add_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1364 |
divide.diff ~> diff_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1365 |
divide.setsum ~> setsum_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1366 |
mult.add_right ~> right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1367 |
mult.diff_right ~> right_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1368 |
mult_right.setsum ~> setsum_right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1369 |
mult_left.diff ~> left_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
1370 |
|
44800 | 1371 |
* Theory Complex_Main: Several redundant theorems have been removed or |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1372 |
replaced by more general versions. INCOMPATIBILITY. |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1373 |
|
45051
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1374 |
real_diff_def ~> minus_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1375 |
real_divide_def ~> divide_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1376 |
real_less_def ~> less_le |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1377 |
real_abs_def ~> abs_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1378 |
real_sgn_def ~> sgn_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1379 |
real_mult_commute ~> mult_commute |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1380 |
real_mult_assoc ~> mult_assoc |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1381 |
real_mult_1 ~> mult_1_left |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1382 |
real_add_mult_distrib ~> left_distrib |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1383 |
real_zero_not_eq_one ~> zero_neq_one |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1384 |
real_mult_inverse_left ~> left_inverse |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1385 |
INVERSE_ZERO ~> inverse_zero |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1386 |
real_le_refl ~> order_refl |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1387 |
real_le_antisym ~> order_antisym |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1388 |
real_le_trans ~> order_trans |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1389 |
real_le_linear ~> linear |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1390 |
real_le_eq_diff ~> le_iff_diff_le_0 |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1391 |
real_add_left_mono ~> add_left_mono |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1392 |
real_mult_order ~> mult_pos_pos |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
1393 |
real_mult_less_mono2 ~> mult_strict_left_mono |
44822
2690b6de5021
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
huffman
parents:
44777
diff
changeset
|
1394 |
real_of_int_real_of_nat ~> real_of_int_of_nat_eq |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1395 |
real_0_le_divide_iff ~> zero_le_divide_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1396 |
realpow_two_disj ~> power2_eq_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1397 |
real_squared_diff_one_factored ~> square_diff_one_factored |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1398 |
realpow_two_diff ~> square_diff_square_factored |
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
44666
diff
changeset
|
1399 |
reals_complete2 ~> complete_real |
44749
5b1e1432c320
remove redundant lemma real_sum_squared_expand in favor of power2_sum
huffman
parents:
44748
diff
changeset
|
1400 |
real_sum_squared_expand ~> power2_sum |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1401 |
exp_ln_eq ~> ln_unique |
44711 | 1402 |
expi_add ~> exp_add |
1403 |
expi_zero ~> exp_zero |
|
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
1404 |
lemma_DERIV_subst ~> DERIV_cong |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1405 |
LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1406 |
LIMSEQ_const ~> tendsto_const |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1407 |
LIMSEQ_norm ~> tendsto_norm |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1408 |
LIMSEQ_add ~> tendsto_add |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1409 |
LIMSEQ_minus ~> tendsto_minus |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1410 |
LIMSEQ_minus_cancel ~> tendsto_minus_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1411 |
LIMSEQ_diff ~> tendsto_diff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1412 |
bounded_linear.LIMSEQ ~> bounded_linear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1413 |
bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
1414 |
LIMSEQ_mult ~> tendsto_mult |
e6f291cb5810
discontinue |