author | wenzelm |
Wed, 07 Aug 2013 15:35:33 +0200 | |
changeset 52896 | 73e32ed924b3 |
parent 52818 | 76e9fbb7c080 |
child 52949 | 90edb0669845 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
50994 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
7 |
*** General *** |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
8 |
|
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
9 |
* Uniform management of "quick_and_dirty" as system option (see also |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
10 |
"isabelle options"), configuration option within the context (see also |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
11 |
Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
12 |
INCOMPATIBILITY, need to use more official Isabelle means to access |
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset
|
13 |
quick_and_dirty, instead of historical poking into mutable reference. |
52059 | 14 |
|
52060 | 15 |
* Renamed command 'print_configs' to 'print_options'. Minor |
16 |
INCOMPATIBILITY. |
|
17 |
||
51417 | 18 |
* Sessions may be organized via 'chapter' specifications in the ROOT |
19 |
file, which determines a two-level hierarchy of browser info. The old |
|
20 |
tree-like organization via implicit sub-session relation, with its |
|
21 |
tendency towards erratic fluctuation of URLs, has been discontinued. |
|
22 |
The default chapter is "Unsorted". Potential INCOMPATIBILITY for HTML |
|
23 |
presentation of theories. |
|
24 |
||
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
25 |
* Discontinued obsolete 'uses' within theory header. Note that |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
26 |
commands like 'ML_file' work without separate declaration of file |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
27 |
dependencies. Minor INCOMPATIBILITY. |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
28 |
|
51295 | 29 |
* Discontinued redundant 'use' command, which was superseded by |
30 |
'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. |
|
31 |
||
52415 | 32 |
* Updated and extended "isar-ref" and "implementation" manual, |
33 |
eliminated old "ref" manual. |
|
34 |
||
52430 | 35 |
* Proper diagnostic command 'print_state'. Old 'pr' (with its |
36 |
implicit change of some global references) is retained for now as |
|
37 |
control command, e.g. for ProofGeneral 3.7.x. |
|
38 |
||
52549 | 39 |
* Discontinued 'print_drafts' command with its old-fashioned PS output |
40 |
and Unix command-line print spooling. Minor INCOMPATIBILITY: use |
|
41 |
'display_drafts' instead and print via the regular document viewer. |
|
42 |
||
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51238
diff
changeset
|
43 |
|
51533 | 44 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
45 |
||
52818 | 46 |
* Improved "Theories" panel: Continuous checking of proof document |
47 |
(visible and required parts) may be controlled explicitly, using check |
|
48 |
box or shortcut "C+e ENTER". Individual theory nodes may be marked |
|
49 |
explicitly as required and checked in full, using check box or |
|
50 |
shortcut "C+e SPACE". |
|
52779 | 51 |
|
52646 | 52 |
* Strictly monotonic document update, without premature cancelation of |
53 |
running transactions that are still needed: avoid reset/restart of |
|
54 |
such command executions while editing. |
|
55 |
||
56 |
* Support for asynchronous print functions, as overlay to existing |
|
57 |
document content. |
|
58 |
||
59 |
* Support for automatic tools in HOL, which try to prove or disprove |
|
60 |
toplevel theorem statements. |
|
61 |
||
52445 | 62 |
* Dockable window "Documentation" provides access to Isabelle |
63 |
documentation. |
|
64 |
||
51533 | 65 |
* Dockable window "Timing" provides an overview of relevant command |
66 |
timing information. |
|
67 |
||
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51551
diff
changeset
|
68 |
* Option to skip over proofs, using implicit 'sorry' internally. |
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51551
diff
changeset
|
69 |
|
51533 | 70 |
|
51313 | 71 |
*** Pure *** |
72 |
||
52788 | 73 |
* Type theory is now immutable, without any special treatment of |
74 |
drafts or linear updates (which could lead to "stale theory" errors in |
|
75 |
the past). Discontinued obsolete operations like Theory.copy, |
|
76 |
Theory.checkpoint, and the auxiliary type theory_ref. Minor |
|
77 |
INCOMPATIBILITY. |
|
78 |
||
52488
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52487
diff
changeset
|
79 |
* System option "proofs" has been discontinued. Instead the global |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52487
diff
changeset
|
80 |
state of Proofterm.proofs is persistently compiled into logic images |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52487
diff
changeset
|
81 |
as required, notably HOL-Proofs. Users no longer need to change |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52487
diff
changeset
|
82 |
Proofterm.proofs dynamically. Minor INCOMPATIBILITY. |
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52487
diff
changeset
|
83 |
|
52143 | 84 |
* Syntax translation functions (print_translation etc.) always depend |
85 |
on Proof.context. Discontinued former "(advanced)" option -- this is |
|
86 |
now the default. Minor INCOMPATIBILITY. |
|
87 |
||
51747 | 88 |
* Target-sensitive commands 'interpretation' and 'sublocale'. |
89 |
Particulary, 'interpretation' now allows for non-persistent |
|
90 |
interpretation within "context ... begin ... end" blocks. |
|
91 |
See "isar-ref" manual for details. |
|
92 |
||
51565 | 93 |
* Improved locales diagnostic command 'print_dependencies'. |
94 |
||
51313 | 95 |
* Discontinued obsolete 'axioms' command, which has been marked as |
96 |
legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization' |
|
97 |
instead, while observing its uniform scope for polymorphism. |
|
98 |
||
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
99 |
* Discontinued empty name bindings in 'axiomatization'. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
100 |
INCOMPATIBILITY. |
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
51313
diff
changeset
|
101 |
|
52463 | 102 |
* SELECT_GOAL now retains the syntactic context of the overall goal |
103 |
state (schematic variables etc.). Potential INCOMPATIBILITY in rare |
|
104 |
situations. |
|
105 |
||
51313 | 106 |
|
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
107 |
*** HOL *** |
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
108 |
|
52896 | 109 |
* Improved support for adhoc overloading of constants (see also |
110 |
isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy). |
|
111 |
||
52637
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52550
diff
changeset
|
112 |
* Attibute 'code': 'code' now declares concrete and abstract code equations uniformly. |
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52550
diff
changeset
|
113 |
Use explicit 'code equation' and 'code abstract' to distinguish both when desired. |
1501ebe39711
attribute "code" declares concrete and abstract code equations uniformly; added explicit "code equation" instead
haftmann
parents:
52550
diff
changeset
|
114 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
115 |
* Code generator: |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
116 |
* 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'. |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
117 |
* 'code_identifier' declares name hints for arbitrary identifiers in generated code, |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
118 |
subsuming 'code_modulename'. |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
119 |
See the Isar reference manual for syntax diagrams, and the HOL theories for examples. |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52430
diff
changeset
|
120 |
|
52380 | 121 |
* Library/Polynomial.thy: |
122 |
* Use lifting for primitive definitions. |
|
123 |
* Explicit conversions from and to lists of coefficients, used for generated code. |
|
124 |
* Replaced recursion operator poly_rec by fold_coeffs. |
|
125 |
* Prefer pre-existing gcd operation for gcd. |
|
126 |
* Fact renames: |
|
127 |
poly_eq_iff ~> poly_eq_poly_eq_iff |
|
128 |
poly_ext ~> poly_eqI |
|
129 |
expand_poly_eq ~> poly_eq_iff |
|
130 |
IMCOMPATIBILTIY. |
|
131 |
||
52286 | 132 |
* Reification and reflection: |
133 |
* Reification is now directly available in HOL-Main in structure "Reification". |
|
134 |
* Reflection now handles multiple lists with variables also. |
|
135 |
* The whole reflection stack has been decomposed into conversions. |
|
136 |
INCOMPATIBILITY. |
|
137 |
||
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
52116
diff
changeset
|
138 |
* Weaker precendence of syntax for big intersection and union on sets, |
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
52116
diff
changeset
|
139 |
in accordance with corresponding lattice operations. INCOMPATIBILITY. |
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
52116
diff
changeset
|
140 |
|
51682 | 141 |
* Nested case expressions are now translated in a separate check |
142 |
phase rather than during parsing. The data for case combinators |
|
143 |
is separated from the datatype package. The declaration attribute |
|
144 |
"case_translation" can be used to register new case combinators: |
|
145 |
||
146 |
declare [[case_translation case_combinator constructor1 ... constructorN]] |
|
147 |
||
51596 | 148 |
* Notation "{p:A. P}" now allows tuple patterns as well. |
149 |
||
51489 | 150 |
* Revised devices for recursive definitions over finite sets: |
151 |
- Only one fundamental fold combinator on finite set remains: |
|
152 |
Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b |
|
153 |
This is now identity on infinite sets. |
|
52745
821ce370b7fc
avoid predefined symbols -- allow editing with Isabelle/jEdit in isabelle-news mode;
wenzelm
parents:
52743
diff
changeset
|
154 |
- Locales ("mini packages") for fundamental definitions with |
51489 | 155 |
Finite_Set.fold: folding, folding_idem. |
156 |
- Locales comm_monoid_set, semilattice_order_set and |
|
157 |
semilattice_neutr_order_set for big operators on sets. |
|
158 |
See theory Big_Operators for canonical examples. |
|
159 |
Note that foundational constants comm_monoid_set.F and |
|
160 |
semilattice_set.F correspond to former combinators fold_image |
|
161 |
and fold1 respectively. These are now gone. You may use |
|
51490 | 162 |
those foundational constants as substitutes, but it is |
51489 | 163 |
preferable to interpret the above locales accordingly. |
164 |
- Dropped class ab_semigroup_idem_mult (special case of lattice, |
|
165 |
no longer needed in connection with Finite_Set.fold etc.) |
|
166 |
- Fact renames: |
|
167 |
card.union_inter ~> card_Un_Int [symmetric] |
|
168 |
card.union_disjoint ~> card_Un_disjoint |
|
169 |
||
170 |
INCOMPATIBILITY. |
|
171 |
||
51487 | 172 |
* Locale hierarchy for abstract orderings and (semi)lattices. |
173 |
||
51382
51957d006677
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
haftmann
parents:
51316
diff
changeset
|
174 |
* Discontinued theory src/HOL/Library/Eval_Witness. |
51957d006677
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
haftmann
parents:
51316
diff
changeset
|
175 |
INCOMPATIBILITY. |
51957d006677
discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
haftmann
parents:
51316
diff
changeset
|
176 |
|
51238 | 177 |
* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since |
178 |
Isabelle2013). Use "isabelle build" to operate on Isabelle sessions. |
|
179 |
||
51168
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
180 |
* Numeric types mapped by default to target language numerals: |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
181 |
natural (replaces former code_numeral) and integer (replaces |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
182 |
former code_int). Conversions are available as integer_of_natural / |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
183 |
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
184 |
Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ML). |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
185 |
INCOMPATIBILITY. |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
186 |
|
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
187 |
* Discontinued theories Code_Integer and Efficient_Nat by a more |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
188 |
fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
189 |
Code_Target_Nat and Code_Target_Numeral. See the tutorial on |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
190 |
code generation for details. INCOMPATIBILITY. |
35d00ce58626
restored proper order of NEWS entries (lost due too long-waiting patches)
haftmann
parents:
51143
diff
changeset
|
191 |
|
51773 | 192 |
* Introduce type class "conditionally_complete_lattice": Like a complete |
51732 | 193 |
lattice but does not assume the existence of the top and bottom elements. |
194 |
Allows to generalize some lemmas about reals and extended reals. |
|
195 |
Removed SupInf and replaced it by the instantiation of |
|
51773 | 196 |
conditionally_complete_lattice for real. Renamed lemmas about |
197 |
conditionally-complete lattice from Sup_... to cSup_... and from Inf_... |
|
198 |
to cInf_... to avoid hidding of similar complete lattice lemmas. |
|
51775
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
199 |
|
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
200 |
Introduce type class linear_continuum as combination of conditionally-complete |
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
201 |
lattices and inner dense linorders which have more than one element. |
51732 | 202 |
INCOMPATIBILITY. |
203 |
||
204 |
* Introduce type classes "no_top" and "no_bot" for orderings without top |
|
205 |
and bottom elements. |
|
206 |
||
207 |
* Split dense_linorder into inner_dense_order and no_top, no_bot. |
|
208 |
||
209 |
* Complex_Main: Unify and move various concepts from |
|
210 |
HOL-Multivariate_Analysis to HOL-Complex_Main. |
|
211 |
||
51775
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
212 |
- Introduce type class (lin)order_topology and linear_continuum_topology. |
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
213 |
Allows to generalize theorems about limits and order. |
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
214 |
Instances are reals and extended reals. |
51732 | 215 |
|
216 |
- continuous and continuos_on from Multivariate_Analysis: |
|
217 |
"continuous" is the continuity of a function at a filter. |
|
218 |
"isCont" is now an abbrevitation: "isCont x f == continuous (at _) f". |
|
219 |
||
220 |
Generalized continuity lemmas from isCont to continuous on an arbitrary |
|
221 |
filter. |
|
222 |
||
223 |
- compact from Multivariate_Analysis. Use Bolzano's lemma |
|
224 |
to prove compactness of closed intervals on reals. Continuous functions |
|
225 |
attain infimum and supremum on compact sets. The inverse of a continuous |
|
226 |
function is continuous, when the function is continuous on a compact set. |
|
227 |
||
228 |
- connected from Multivariate_Analysis. Use it to prove the |
|
51775
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
229 |
intermediate value theorem. Show connectedness of intervals on |
408d937c9486
revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51774
diff
changeset
|
230 |
linear_continuum_topology). |
51732 | 231 |
|
232 |
- first_countable_topology from Multivariate_Analysis. Is used to |
|
233 |
show equivalence of properties on the neighbourhood filter of x and on |
|
234 |
all sequences converging to x. |
|
235 |
||
236 |
- FDERIV: Definition of has_derivative moved to Deriv.thy. Moved theorems |
|
237 |
from Library/FDERIV.thy to Deriv.thy and base the definition of DERIV on |
|
238 |
FDERIV. Add variants of DERIV and FDERIV which are restricted to sets, |
|
239 |
i.e. to represent derivatives from left or right. |
|
240 |
||
241 |
- Removed the within-filter. It is replaced by the principal filter: |
|
242 |
||
243 |
F within X = inf F (principal X) |
|
244 |
||
245 |
- Introduce "at x within U" as a single constant, "at x" is now an |
|
246 |
abbreviation for "at x within UNIV" |
|
247 |
||
248 |
- Introduce named theorem collections tendsto_intros, continuous_intros, |
|
249 |
continuous_on_intros and FDERIV_intros. Theorems in tendsto_intros (or |
|
250 |
FDERIV_intros) are also available as tendsto_eq_intros (or |
|
251 |
FDERIV_eq_intros) where the right-hand side is replaced by a congruence |
|
252 |
rule. This allows to apply them as intro rules and then proving |
|
253 |
equivalence by the simplifier. |
|
254 |
||
255 |
- Restructured theories in HOL-Complex_Main: |
|
256 |
||
257 |
+ Moved RealDef and RComplete into Real |
|
258 |
||
259 |
+ Introduced Topological_Spaces and moved theorems about |
|
260 |
topological spaces, filters, limits and continuity to it |
|
261 |
||
262 |
+ Renamed RealVector to Real_Vector_Spaces |
|
263 |
||
264 |
+ Split Lim, SEQ, Series into Topological_Spaces, Real_Vector_Spaces, and |
|
265 |
Limits |
|
266 |
||
267 |
+ Moved Ln and Log to Transcendental |
|
268 |
||
269 |
+ Moved theorems about continuity from Deriv to Topological_Spaces |
|
270 |
||
271 |
- Remove various auxiliary lemmas. |
|
272 |
||
273 |
INCOMPATIBILITY. |
|
51002
496013a6eb38
remove unnecessary assumption from real_normed_vector
hoelzl
parents:
50994
diff
changeset
|
274 |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
275 |
* Consolidation of library theories on product orders: |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
276 |
|
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
277 |
Product_Lattice ~> Product_Order -- pointwise order on products |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
278 |
Product_ord ~> Product_Lexorder -- lexicographic order on products |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
279 |
|
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
280 |
INCOMPATIBILITY. |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51088
diff
changeset
|
281 |
|
51137 | 282 |
* Sledgehammer: |
283 |
||
284 |
- Renamed option: |
|
285 |
isar_shrink ~> isar_compress |
|
286 |
||
52266 | 287 |
* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment. |
288 |
||
289 |
With HOL-Spec_Check, ML developers can check specifications with the |
|
290 |
ML function check_property. The specifications must be of the form |
|
291 |
"ALL x1 ... xn. Prop x1 ... xn". Simple examples are in |
|
292 |
src/HOL/Spec_Check/Examples.thy. |
|
293 |
||
50994 | 294 |
|
51517
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
295 |
*** HOL-Algebra *** |
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
296 |
|
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
297 |
* Discontinued theories src/HOL/Algebra/abstract and .../poly. |
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
298 |
Existing theories should be based on src/HOL/Library/Polynomial |
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
299 |
instead. The latter provides integration with HOL's type classes for |
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
300 |
rings. INCOMPATIBILITY. |
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
301 |
|
7957d26c3334
Discontinued theories src/HOL/Algebra/abstract and .../poly.
ballarin
parents:
51490
diff
changeset
|
302 |
|
51551 | 303 |
*** ML *** |
304 |
||
305 |
* More uniform naming of goal functions for skipped proofs: |
|
306 |
||
307 |
Skip_Proof.prove ~> Goal.prove_sorry |
|
308 |
Skip_Proof.prove_global ~> Goal.prove_sorry_global |
|
309 |
||
51686 | 310 |
* Antiquotation @{theory_context A} is similar to @{theory A}, but |
311 |
presents the result as initial Proof.context. |
|
312 |
||
51703
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
313 |
* Modifiers for classical wrappers (e.g. addWrapper, delWrapper) |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
314 |
operate on Proof.context instead of claset, for uniformity with addIs, |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
315 |
addEs, addDs etc. Note that claset_of and put_claset allow to manage |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
316 |
clasets separately from the context. |
f2e92fc0c8aa
modifiers for classical wrappers operate on Proof.context instead of claset;
wenzelm
parents:
51689
diff
changeset
|
317 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
318 |
* Simplifier tactics and tools use proper Proof.context instead of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
319 |
historic type simpset. Old-style declarations like addsimps, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
320 |
addsimprocs etc. operate directly on Proof.context. Raw type simpset |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
321 |
retains its use as snapshot of the main Simplifier context, using |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
322 |
simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
323 |
old tools by making them depend on (ctxt : Proof.context) instead of |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
324 |
(ss : simpset), then turn (simpset_of ctxt) into ctxt. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
325 |
|
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
326 |
* Discontinued obsolete ML antiquotations @{claset} and @{simpset}. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
327 |
INCOMPATIBILITY, use @{context} instead. |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51703
diff
changeset
|
328 |
|
51551 | 329 |
|
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
330 |
*** System *** |
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
331 |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
51775
diff
changeset
|
332 |
* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by |
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
51775
diff
changeset
|
333 |
"isabelle build" in Isabelle2013. INCOMPATIBILITY. |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
334 |
|
52054
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
335 |
* Discontinued obsolete isabelle-process options -f and -u (former |
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
336 |
administrative aliases of option -e). Minor INCOMPATIBILITY. |
eaf17514aabd
discontinued obsolete isabelle-process options -f and -u;
wenzelm
parents:
52053
diff
changeset
|
337 |
|
52550 | 338 |
* Discontinued obsolete isabelle print tool, and PRINT_COMMAND |
339 |
settings variable. |
|
340 |
||
52746 | 341 |
* Discontinued ISABELLE_DOC_FORMAT settings variable and historic |
342 |
document formats: dvi.gz, ps, ps.gz -- the default document format is |
|
343 |
always pdf. |
|
52743 | 344 |
|
52053 | 345 |
* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to |
346 |
specify global resources of the JVM process run by isabelle build. |
|
347 |
||
52116
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
348 |
* Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
349 |
to run Isabelle/Scala source files as standalone programs. |
abf9fcfa65cf
added isabelle_scala_script wrapper -- NB: portable hash-bang allows exactly one executable, without additional arguments;
wenzelm
parents:
52060
diff
changeset
|
350 |
|
52439
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
351 |
* Improved "isabelle keywords" tool (for old-style ProofGeneral |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
352 |
keyword tables): use Isabelle/Scala operations, which inspect outer |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
353 |
syntax without requiring to build sessions first. |
4cf3f6153eb8
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
wenzelm
parents:
52435
diff
changeset
|
354 |
|
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
355 |
|
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51382
diff
changeset
|
356 |
|
50993 | 357 |
New in Isabelle2013 (February 2013) |
358 |
----------------------------------- |
|
47887 | 359 |
|
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
360 |
*** General *** |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
361 |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
362 |
* Theorem status about oracles and unfinished/failed future proofs is |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
363 |
no longer printed by default, since it is incompatible with |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
364 |
incremental / parallel checking of the persistent document model. ML |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
365 |
function Thm.peek_status may be used to inspect a snapshot of the |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
366 |
ongoing evaluation process. Note that in batch mode --- notably |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
367 |
isabelle build --- the system ensures that future proofs of all |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
368 |
accessible theorems in the theory context are finished (as before). |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50119
diff
changeset
|
369 |
|
49699 | 370 |
* Configuration option show_markup controls direct inlining of markup |
371 |
into the printed representation of formal entities --- notably type |
|
372 |
and sort constraints. This enables Prover IDE users to retrieve that |
|
373 |
information via tooltips in the output window, for example. |
|
374 |
||
48890
d72ca5742f80
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
wenzelm
parents:
48844
diff
changeset
|
375 |
* 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
|
376 |
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
|
377 |
|
49243 | 378 |
* Old command 'use' command and corresponding keyword 'uses' in the |
379 |
theory header are legacy features and will be discontinued soon. |
|
380 |
Tools that load their additional source files may imitate the |
|
381 |
'ML_file' implementation, such that the system can take care of |
|
382 |
dependencies properly. |
|
383 |
||
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
384 |
* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
385 |
is called fastforce / fast_force_tac already since Isabelle2011-1. |
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
386 |
|
50110 | 387 |
* Updated and extended "isar-ref" and "implementation" manual, reduced |
388 |
remaining material in old "ref" manual. |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
389 |
|
51050 | 390 |
* Improved support for auxiliary contexts that indicate block structure |
391 |
for specifications. Nesting of "context fixes ... context assumes ..." |
|
49841 | 392 |
and "class ... context ...". |
393 |
||
50772
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
394 |
* Attribute "consumes" allows a negative value as well, which is |
50778 | 395 |
interpreted relatively to the total number of premises of the rule in |
50772
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
396 |
the target context. This form of declaration is stable when exported |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
397 |
from a nested 'context' with additional assumptions. It is the |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
398 |
preferred form for definitional packages, notably cases/rules produced |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
399 |
in HOL/inductive and HOL/function. |
6973b3f41334
allow negative argument in "consumes" source format;
wenzelm
parents:
50731
diff
changeset
|
400 |
|
49869
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
401 |
* More informative error messages for Isar proof commands involving |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
402 |
lazy enumerations (method applications etc.). |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
403 |
|
50213 | 404 |
* Refined 'help' command to retrieve outer syntax commands according |
405 |
to name patterns (with clickable results). |
|
406 |
||
47967
c422128d3889
discontinued obsolete method fastsimp / tactic fast_simp_tac;
wenzelm
parents:
47958
diff
changeset
|
407 |
|
49968 | 408 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
409 |
||
410 |
* Parallel terminal proofs ('by') are enabled by default, likewise |
|
411 |
proofs that are built into packages like 'datatype', 'function'. This |
|
412 |
allows to "run ahead" checking the theory specifications on the |
|
413 |
surface, while the prover is still crunching on internal |
|
414 |
justifications. Unfinished / cancelled proofs are restarted as |
|
415 |
required to complete full proof checking eventually. |
|
416 |
||
417 |
* Improved output panel with tooltips, hyperlinks etc. based on the |
|
418 |
same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of |
|
419 |
tooltips leads to some window that supports the same recursively, |
|
420 |
which can lead to stacks of tooltips as the semantic document content |
|
421 |
is explored. ESCAPE closes the whole stack, individual windows may be |
|
422 |
closed separately, or detached to become independent jEdit dockables. |
|
423 |
||
50717 | 424 |
* Improved support for commands that produce graph output: the text |
425 |
message contains a clickable area to open a new instance of the graph |
|
426 |
browser on demand. |
|
427 |
||
49968 | 428 |
* More robust incremental parsing of outer syntax (partial comments, |
429 |
malformed symbols). Changing the balance of open/close quotes and |
|
430 |
comment delimiters works more conveniently with unfinished situations |
|
431 |
that frequently occur in user interaction. |
|
432 |
||
433 |
* More efficient painting and improved reactivity when editing large |
|
434 |
files. More scalable management of formal document content. |
|
435 |
||
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
436 |
* Smarter handling of tracing messages: prover process pauses after |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
437 |
certain number of messages per command transaction, with some user |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50455
diff
changeset
|
438 |
dialog to stop or continue. This avoids swamping the front-end with |
50119
5c370a036de7
more generous tracing_limit, with explicit system option;
wenzelm
parents:
50118
diff
changeset
|
439 |
potentially infinite message streams. |
49968 | 440 |
|
441 |
* More plugin options and preferences, based on Isabelle/Scala. The |
|
442 |
jEdit plugin option panel provides access to some Isabelle/Scala |
|
443 |
options, including tuning parameters for editor reactivity and color |
|
444 |
schemes. |
|
445 |
||
50184 | 446 |
* Dockable window "Symbols" provides some editing support for Isabelle |
447 |
symbols. |
|
448 |
||
51082 | 449 |
* Dockable window "Monitor" shows ML runtime statistics. Note that |
450 |
continuous display of the chart slows down the system. |
|
50701 | 451 |
|
50183 | 452 |
* Improved editing support for control styles: subscript, superscript, |
453 |
bold, reset of style -- operating on single symbols or text |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
454 |
selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT. |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
455 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
456 |
* Actions isabelle.increase-font-size and isabelle.decrease-font-size |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50184
diff
changeset
|
457 |
adjust the main text area font size, and its derivatives for output, |
50836 | 458 |
tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS, which often |
459 |
need to be adapted to local keyboard layouts. |
|
50183 | 460 |
|
50730 | 461 |
* More reactive completion popup by default: use \t (TAB) instead of |
462 |
\n (NEWLINE) to minimize intrusion into regular flow of editing. See |
|
463 |
also "Plugin Options / SideKick / General / Code Completion Options". |
|
464 |
||
50406
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
465 |
* Implicit check and build dialog of the specified logic session |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
466 |
image. For example, HOL, HOLCF, HOL-Nominal can be produced on |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
467 |
demand, without bundling big platform-dependent heap images in the |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
468 |
Isabelle distribution. |
c28753665b8e
documentation for isabelle build_dialog and its implicit use in isabelle jedit;
wenzelm
parents:
50232
diff
changeset
|
469 |
|
49968 | 470 |
* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates |
471 |
from Oracle provide better multi-platform experience. This version is |
|
472 |
now bundled exclusively with Isabelle. |
|
473 |
||
474 |
||
48205 | 475 |
*** Pure *** |
476 |
||
48431
6efff142bb54
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
haftmann
parents:
48428
diff
changeset
|
477 |
* 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
|
478 |
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
|
479 |
|
50646 | 480 |
* Command 'export_code': relative file names are interpreted |
481 |
relatively to master directory of current theory rather than the |
|
482 |
rather arbitrary current working directory. INCOMPATIBILITY. |
|
48371 | 483 |
|
48205 | 484 |
* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
485 |
use regular rule composition via "OF" / "THEN", or explicit proof |
|
486 |
structure instead. Note that Isabelle/ML provides a variety of |
|
487 |
operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
|
488 |
with some care where this is really required. |
|
489 |
||
48792 | 490 |
* Command 'typ' supports an additional variant with explicit sort |
491 |
constraint, to infer and check the most general type conforming to a |
|
51063 | 492 |
given sort. Example (in HOL): |
48792 | 493 |
|
494 |
typ "_ * _ * bool * unit" :: finite |
|
495 |
||
50716 | 496 |
* Command 'locale_deps' visualizes all locales and their relations as |
497 |
a Hasse diagram. |
|
498 |
||
48205 | 499 |
|
48013
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
500 |
*** HOL *** |
44de84112a67
added optimisation for equational premises in Quickcheck; added some Quickcheck examples; NEWS
bulwahn
parents:
47979
diff
changeset
|
501 |
|
50646 | 502 |
* Sledgehammer: |
503 |
||
504 |
- Added MaSh relevance filter based on machine-learning; see the |
|
505 |
Sledgehammer manual for details. |
|
506 |
- Polished Isar proofs generated with "isar_proofs" option. |
|
507 |
- Rationalized type encodings ("type_enc" option). |
|
50720 | 508 |
- Renamed "kill_provers" subcommand to "kill_all". |
50646 | 509 |
- Renamed options: |
510 |
isar_proof ~> isar_proofs |
|
511 |
isar_shrink_factor ~> isar_shrink |
|
512 |
max_relevant ~> max_facts |
|
513 |
relevance_thresholds ~> fact_thresholds |
|
514 |
||
515 |
* Quickcheck: added an optimisation for equality premises. It is |
|
516 |
switched on by default, and can be switched off by setting the |
|
517 |
configuration quickcheck_optimise_equality to false. |
|
518 |
||
50878 | 519 |
* Quotient: only one quotient can be defined by quotient_type |
520 |
INCOMPATIBILITY. |
|
521 |
||
522 |
* Lifting: |
|
523 |
- generation of an abstraction function equation in lift_definition |
|
524 |
- quot_del attribute |
|
525 |
- renamed no_abs_code -> no_code (INCOMPATIBILITY.) |
|
526 |
||
50646 | 527 |
* Simproc "finite_Collect" rewrites set comprehensions into pointfree |
528 |
expressions. |
|
529 |
||
530 |
* Preprocessing of the code generator rewrites set comprehensions into |
|
531 |
pointfree expressions. |
|
532 |
||
533 |
* The SMT solver Z3 has now by default a restricted set of directly |
|
534 |
supported features. For the full set of features (div/mod, nonlinear |
|
535 |
arithmetic, datatypes/records) with potential proof reconstruction |
|
536 |
failures, enable the configuration option "z3_with_extensions". Minor |
|
537 |
INCOMPATIBILITY. |
|
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49918
diff
changeset
|
538 |
|
49836
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
539 |
* Simplified 'typedef' specifications: historical options for implicit |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
540 |
set definition and alternative name have been discontinued. The |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
541 |
former behavior of "typedef (open) t = A" is now the default, but |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
542 |
written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
543 |
accordingly. |
c13b39542972
simplified 'typedef' specifications: discontinued implicit set definition and alternative name;
wenzelm
parents:
49822
diff
changeset
|
544 |
|
50646 | 545 |
* Removed constant "chars"; prefer "Enum.enum" on type "char" |
546 |
directly. INCOMPATIBILITY. |
|
547 |
||
548 |
* Moved operation product, sublists and n_lists from theory Enum to |
|
549 |
List. INCOMPATIBILITY. |
|
49822
0cfc1651be25
simplified construction of fold combinator on multisets;
haftmann
parents:
49770
diff
changeset
|
550 |
|
49739 | 551 |
* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. |
552 |
||
49738 | 553 |
* Class "comm_monoid_diff" formalises properties of bounded |
49388 | 554 |
subtraction, with natural numbers and multisets as typical instances. |
555 |
||
50646 | 556 |
* Added combinator "Option.these" with type "'a option set => 'a set". |
557 |
||
558 |
* Theory "Transitive_Closure": renamed lemmas |
|
559 |
||
560 |
reflcl_tranclp -> reflclp_tranclp |
|
561 |
rtranclp_reflcl -> rtranclp_reflclp |
|
562 |
||
563 |
INCOMPATIBILITY. |
|
564 |
||
565 |
* Theory "Rings": renamed lemmas (in class semiring) |
|
566 |
||
567 |
left_distrib ~> distrib_right |
|
568 |
right_distrib ~> distrib_left |
|
569 |
||
570 |
INCOMPATIBILITY. |
|
571 |
||
572 |
* Generalized the definition of limits: |
|
573 |
||
574 |
- Introduced the predicate filterlim (LIM x F. f x :> G) which |
|
575 |
expresses that when the input values x converge to F then the |
|
576 |
output f x converges to G. |
|
577 |
||
578 |
- Added filters for convergence to positive (at_top) and negative |
|
579 |
infinity (at_bot). |
|
580 |
||
581 |
- Moved infinity in the norm (at_infinity) from |
|
582 |
Multivariate_Analysis to Complex_Main. |
|
583 |
||
584 |
- Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> |
|
585 |
at_top". |
|
586 |
||
587 |
INCOMPATIBILITY. |
|
588 |
||
589 |
* Theory "Library/Option_ord" provides instantiation of option type to |
|
590 |
lattice type classes. |
|
591 |
||
592 |
* Theory "Library/Multiset": renamed |
|
593 |
||
594 |
constant fold_mset ~> Multiset.fold |
|
595 |
fact fold_mset_commute ~> fold_mset_comm |
|
596 |
||
597 |
INCOMPATIBILITY. |
|
598 |
||
599 |
* Renamed theory Library/List_Prefix to Library/Sublist, with related |
|
600 |
changes as follows. |
|
601 |
||
602 |
- Renamed constants (and related lemmas) |
|
49145 | 603 |
|
604 |
prefix ~> prefixeq |
|
605 |
strict_prefix ~> prefix |
|
606 |
||
50646 | 607 |
- Replaced constant "postfix" by "suffixeq" with swapped argument |
608 |
order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped |
|
609 |
old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead. |
|
610 |
Renamed lemmas accordingly. |
|
611 |
||
612 |
- Added constant "list_hembeq" for homeomorphic embedding on |
|
613 |
lists. Added abbreviation "sublisteq" for special case |
|
614 |
"list_hembeq (op =)". |
|
615 |
||
616 |
- Theory Library/Sublist no longer provides "order" and "bot" type |
|
617 |
class instances for the prefix order (merely corresponding locale |
|
618 |
interpretations). The type class instances are now in theory |
|
619 |
Library/Prefix_Order. |
|
620 |
||
621 |
- The sublist relation of theory Library/Sublist_Order is now based |
|
622 |
on "Sublist.sublisteq". Renamed lemmas accordingly: |
|
50516 | 623 |
|
624 |
le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff |
|
625 |
le_list_append_mono ~> Sublist.list_hembeq_append_mono |
|
626 |
le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2 |
|
627 |
le_list_Cons_EX ~> Sublist.list_hembeq_ConsD |
|
628 |
le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2' |
|
629 |
le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq |
|
630 |
le_list_drop_Cons ~> Sublist.sublisteq_Cons' |
|
631 |
le_list_drop_many ~> Sublist.sublisteq_drop_many |
|
632 |
le_list_filter_left ~> Sublist.sublisteq_filter_left |
|
633 |
le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many |
|
634 |
le_list_rev_take_iff ~> Sublist.sublisteq_append |
|
635 |
le_list_same_length ~> Sublist.sublisteq_same_length |
|
636 |
le_list_take_many_iff ~> Sublist.sublisteq_append' |
|
49145 | 637 |
less_eq_list.drop ~> less_eq_list_drop |
638 |
less_eq_list.induct ~> less_eq_list_induct |
|
50516 | 639 |
not_le_list_length ~> Sublist.not_sublisteq_length |
49145 | 640 |
|
50646 | 641 |
INCOMPATIBILITY. |
642 |
||
643 |
* New theory Library/Countable_Set. |
|
644 |
||
645 |
* Theory Library/Debug and Library/Parallel provide debugging and |
|
646 |
parallel execution for code generated towards Isabelle/ML. |
|
647 |
||
648 |
* Theory Library/FuncSet: Extended support for Pi and extensional and |
|
649 |
introduce the extensional dependent function space "PiE". Replaced |
|
650 |
extensional_funcset by an abbreviation, and renamed lemmas from |
|
651 |
extensional_funcset to PiE as follows: |
|
652 |
||
653 |
extensional_empty ~> PiE_empty |
|
654 |
extensional_funcset_empty_domain ~> PiE_empty_domain |
|
655 |
extensional_funcset_empty_range ~> PiE_empty_range |
|
656 |
extensional_funcset_arb ~> PiE_arb |
|
657 |
extensional_funcset_mem ~> PiE_mem |
|
658 |
extensional_funcset_extend_domainI ~> PiE_fun_upd |
|
659 |
extensional_funcset_restrict_domain ~> fun_upd_in_PiE |
|
660 |
extensional_funcset_extend_domain_eq ~> PiE_insert_eq |
|
661 |
card_extensional_funcset ~> card_PiE |
|
662 |
finite_extensional_funcset ~> finite_PiE |
|
663 |
||
664 |
INCOMPATIBILITY. |
|
665 |
||
666 |
* Theory Library/FinFun: theory of almost everywhere constant |
|
667 |
functions (supersedes the AFP entry "Code Generation for Functions as |
|
668 |
Data"). |
|
669 |
||
670 |
* Theory Library/Phantom: generic phantom type to make a type |
|
671 |
parameter appear in a constant's type. This alternative to adding |
|
672 |
TYPE('a) as another parameter avoids unnecessary closures in generated |
|
673 |
code. |
|
674 |
||
675 |
* Theory Library/RBT_Impl: efficient construction of red-black trees |
|
676 |
from sorted associative lists. Merging two trees with rbt_union may |
|
677 |
return a structurally different tree than before. Potential |
|
678 |
INCOMPATIBILITY. |
|
679 |
||
680 |
* Theory Library/IArray: immutable arrays with code generation. |
|
681 |
||
682 |
* Theory Library/Finite_Lattice: theory of finite lattices. |
|
683 |
||
684 |
* HOL/Multivariate_Analysis: replaced |
|
685 |
||
686 |
"basis :: 'a::euclidean_space => nat => real" |
|
687 |
"\<Chi>\<Chi> :: (nat => real) => 'a::euclidean_space" |
|
688 |
||
689 |
on euclidean spaces by using the inner product "_ \<bullet> _" with |
|
690 |
vectors from the Basis set: "\<Chi>\<Chi> i. f i" is superseded by |
|
691 |
"SUM i : Basis. f i * r i". |
|
692 |
||
693 |
With this change the following constants are also changed or removed: |
|
694 |
||
695 |
DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) |
|
696 |
a $$ i ~> inner a i (where i : Basis) |
|
697 |
cart_base i removed |
|
698 |
\<pi>, \<pi>' removed |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
699 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
700 |
Theorems about these constants where removed. |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
701 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
702 |
Renamed lemmas: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
703 |
|
50646 | 704 |
component_le_norm ~> Basis_le_norm |
705 |
euclidean_eq ~> euclidean_eq_iff |
|
706 |
differential_zero_maxmin_component ~> differential_zero_maxmin_cart |
|
707 |
euclidean_simps ~> inner_simps |
|
708 |
independent_basis ~> independent_Basis |
|
709 |
span_basis ~> span_Basis |
|
710 |
in_span_basis ~> in_span_Basis |
|
711 |
norm_bound_component_le ~> norm_boound_Basis_le |
|
712 |
norm_bound_component_lt ~> norm_boound_Basis_lt |
|
713 |
component_le_infnorm ~> Basis_le_infnorm |
|
714 |
||
715 |
INCOMPATIBILITY. |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50525
diff
changeset
|
716 |
|
50141 | 717 |
* HOL/Probability: |
50646 | 718 |
|
719 |
- Added simproc "measurable" to automatically prove measurability. |
|
720 |
||
721 |
- Added induction rules for sigma sets with disjoint union |
|
722 |
(sigma_sets_induct_disjoint) and for Borel-measurable functions |
|
723 |
(borel_measurable_induct). |
|
724 |
||
725 |
- Added the Daniell-Kolmogorov theorem (the existence the limit of a |
|
726 |
projective family). |
|
727 |
||
728 |
* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the |
|
729 |
AFP entry "Ordinals_and_Cardinals"). |
|
730 |
||
731 |
* HOL/BNF: New (co)datatype package based on bounded natural functors |
|
732 |
with support for mixed, nested recursion and interesting non-free |
|
733 |
datatypes. |
|
48094 | 734 |
|
50991 | 735 |
* HOL/Finite_Set and Relation: added new set and relation operations |
50878 | 736 |
expressed by Finite_Set.fold. |
737 |
||
738 |
* New theory HOL/Library/RBT_Set: implementation of sets by red-black |
|
739 |
trees for the code generator. |
|
740 |
||
741 |
* HOL/Library/RBT and HOL/Library/Mapping have been converted to |
|
742 |
Lifting/Transfer. |
|
743 |
possible INCOMPATIBILITY. |
|
744 |
||
745 |
* HOL/Set: renamed Set.project -> Set.filter |
|
746 |
INCOMPATIBILITY. |
|
747 |
||
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
748 |
|
48206 | 749 |
*** Document preparation *** |
750 |
||
50646 | 751 |
* Dropped legacy antiquotations "term_style" and "thm_style", since |
752 |
styles may be given as arguments to "term" and "thm" already. |
|
753 |
Discontinued legacy styles "prem1" .. "prem19". |
|
754 |
||
755 |
* Default LaTeX rendering for \<euro> is now based on eurosym package, |
|
756 |
instead of slightly exotic babel/greek. |
|
48206 | 757 |
|
48616
be8002ee43d8
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
wenzelm
parents:
48586
diff
changeset
|
758 |
* 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
|
759 |
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
|
760 |
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
|
761 |
|
48657
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
762 |
* 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
|
763 |
document/IsaMakefile. Minor INCOMPATIBILITY. |
63ef2f0cf8bb
simplified custom document/build script, instead of old-style document/IsaMakefile;
wenzelm
parents:
48616
diff
changeset
|
764 |
|
48206 | 765 |
|
48992 | 766 |
*** ML *** |
767 |
||
50646 | 768 |
* The default limit for maximum number of worker threads is now 8, |
769 |
instead of 4, in correspondence to capabilities of contemporary |
|
770 |
hardware and Poly/ML runtime system. |
|
771 |
||
49869
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
772 |
* Type Seq.results and related operations support embedded error |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
773 |
messages within lazy enumerations, and thus allow to provide |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
774 |
informative errors in the absence of any usable results. |
bd370af308f0
support for more informative errors in lazy enumerations;
wenzelm
parents:
49841
diff
changeset
|
775 |
|
48992 | 776 |
* Renamed Position.str_of to Position.here to emphasize that this is a |
777 |
formal device to inline positions into message text, but not |
|
778 |
necessarily printing visible text. |
|
779 |
||
780 |
||
48206 | 781 |
*** System *** |
782 |
||
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
783 |
* Advanced support for Isabelle sessions and build management, see |
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
784 |
"system" manual for the chapter of that name, especially the "isabelle |
51056 | 785 |
build" tool and its examples. The "isabelle mkroot" tool prepares |
786 |
session root directories for use with "isabelle build", similar to |
|
787 |
former "isabelle mkdir" for "isabelle usedir". Note that this affects |
|
788 |
document preparation as well. INCOMPATIBILITY, isabelle usedir / |
|
48736 | 789 |
mkdir / make are rendered obsolete. |
790 |
||
51056 | 791 |
* Discontinued obsolete Isabelle/build script, it is superseded by the |
792 |
regular isabelle build tool. For example: |
|
793 |
||
794 |
isabelle build -s -b HOL |
|
795 |
||
48736 | 796 |
* Discontinued obsolete "isabelle makeall". |
48585
a82910dd2270
announce advanced support for Isabelle sessions and build management;
wenzelm
parents:
48574
diff
changeset
|
797 |
|
48722
a5e3ba7cbb2a
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
wenzelm
parents:
48693
diff
changeset
|
798 |
* 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
|
799 |
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
|
800 |
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
|
801 |
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
|
802 |
"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
|
803 |
|
48693
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
804 |
* The "isabelle options" tool prints Isabelle system options, as |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
805 |
required for "isabelle build", for example. |
ceeea46bdeba
"isabelle options" prints Isabelle system options;
wenzelm
parents:
48683
diff
changeset
|
806 |
|
50646 | 807 |
* The "isabelle logo" tool produces EPS and PDF format simultaneously. |
808 |
Minor INCOMPATIBILITY in command-line options. |
|
809 |
||
810 |
* The "isabelle install" tool has now a simpler command-line. Minor |
|
811 |
INCOMPATIBILITY. |
|
812 |
||
48844 | 813 |
* The "isabelle components" tool helps to resolve add-on components |
814 |
that are not bundled, or referenced from a bare-bones repository |
|
815 |
version of Isabelle. |
|
816 |
||
50646 | 817 |
* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general |
818 |
platform family: "linux", "macos", "windows". |
|
819 |
||
820 |
* The ML system is configured as regular component, and no longer |
|
821 |
picked up from some surrounding directory. Potential INCOMPATIBILITY |
|
822 |
for home-made settings. |
|
50132 | 823 |
|
50701 | 824 |
* Improved ML runtime statistics (heap, threads, future tasks etc.). |
825 |
||
48206 | 826 |
* Discontinued support for Poly/ML 5.2.1, which was the last version |
827 |
without exception positions and advanced ML compiler/toplevel |
|
828 |
configuration. |
|
829 |
||
48574 | 830 |
* Discontinued special treatment of Proof General -- no longer guess |
831 |
PROOFGENERAL_HOME based on accidental file-system layout. Minor |
|
832 |
INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS |
|
833 |
settings manually, or use a Proof General version that has been |
|
834 |
bundled as Isabelle component. |
|
48206 | 835 |
|
50182 | 836 |
|
48120
9fe0e71052a0
updated "isar-ref" manual, reduced remaining material in "ref" manual.
wenzelm
parents:
48111
diff
changeset
|
837 |
|
47462 | 838 |
New in Isabelle2012 (May 2012) |
839 |
------------------------------ |
|
45109 | 840 |
|
45593 | 841 |
*** General *** |
842 |
||
45614 | 843 |
* Prover IDE (PIDE) improvements: |
844 |
||
47585 | 845 |
- more robust Sledgehammer integration (as before the sledgehammer |
47806 | 846 |
command-line needs to be typed into the source buffer) |
45614 | 847 |
- markup for bound variables |
47806 | 848 |
- 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
|
849 |
- support for user-defined Isar commands within the running session |
47158 | 850 |
- improved support for Unicode outside original 16bit range |
851 |
e.g. glyph for \<A> (thanks to jEdit 4.5.1) |
|
45614 | 852 |
|
47806 | 853 |
* Forward declaration of outer syntax keywords within the theory |
854 |
header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
|
855 |
commands to be used in the same theory where defined. |
|
46485 | 856 |
|
47482
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
857 |
* 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
|
858 |
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
|
859 |
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
|
860 |
'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
|
861 |
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
|
862 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
863 |
context |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
864 |
fixes x y z :: 'a |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
865 |
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
|
866 |
begin |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
867 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
868 |
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
|
869 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
870 |
end |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
871 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
872 |
thm my_trans |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
873 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
874 |
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
|
875 |
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
|
876 |
~~/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
|
877 |
|
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
878 |
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
|
879 |
... begin ... end" block as well. |
a83b25e5bad3
some coverage of unnamed contexts, which can be nested within other targets;
wenzelm
parents:
47464
diff
changeset
|
880 |
|
47484 | 881 |
* Bundled declarations associate attributed fact expressions with a |
882 |
given name in the context. These may be later included in other |
|
883 |
contexts. This allows to manage context extensions casually, without |
|
47855 | 884 |
the logical dependencies of locales and locale interpretation. See |
885 |
commands 'bundle', 'include', 'including' etc. in the isar-ref manual. |
|
47484 | 886 |
|
47829 | 887 |
* Commands 'lemmas' and 'theorems' allow local variables using 'for' |
888 |
declaration, and results are standardized before being stored. Thus |
|
889 |
old-style "standard" after instantiation or composition of facts |
|
890 |
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of |
|
891 |
indices of schematic variables. |
|
892 |
||
893 |
* Rule attributes in local theory declarations (e.g. locale or class) |
|
894 |
are now statically evaluated: the resulting theorem is stored instead |
|
895 |
of the original expression. INCOMPATIBILITY in rare situations, where |
|
896 |
the historic accident of dynamic re-evaluation in interpretations |
|
897 |
etc. was exploited. |
|
898 |
||
899 |
* New tutorial "Programming and Proving in Isabelle/HOL" |
|
900 |
("prog-prove"). It completely supersedes "A Tutorial Introduction to |
|
901 |
Structured Isar Proofs" ("isar-overview"), which has been removed. It |
|
902 |
also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order |
|
903 |
Logic" as the recommended beginners tutorial, but does not cover all |
|
904 |
of the material of that old tutorial. |
|
905 |
||
906 |
* Updated and extended reference manuals: "isar-ref", |
|
907 |
"implementation", "system"; reduced remaining material in old "ref" |
|
908 |
manual. |
|
909 |
||
910 |
||
911 |
*** Pure *** |
|
912 |
||
46976
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
913 |
* Command 'definition' no longer exports the foundational "raw_def" |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
914 |
into the user context. Minor INCOMPATIBILITY, may use the regular |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
915 |
"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
|
916 |
|
47855 | 917 |
* Attribute "abs_def" turns an equation of the form "f x y == t" into |
918 |
"f == %x y. t", which ensures that "simp" or "unfold" steps always |
|
919 |
expand it. This also works for object-logic equality. (Formerly |
|
920 |
undocumented feature.) |
|
921 |
||
47856 | 922 |
* Sort constraints are now propagated in simultaneous statements, just |
923 |
like type constraints. INCOMPATIBILITY in rare situations, where |
|
924 |
distinct sorts used to be assigned accidentally. For example: |
|
925 |
||
926 |
lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
|
927 |
||
928 |
lemma "P (x::'a)" and "Q (y::'a::bar)" |
|
929 |
-- "now uniform 'a::bar instead of default sort for first occurrence (!)" |
|
930 |
||
931 |
* Rule composition via attribute "OF" (or ML functions OF/MRS) is more |
|
932 |
tolerant against multiple unifiers, as long as the final result is |
|
933 |
unique. (As before, rules are composed in canonical right-to-left |
|
934 |
order to accommodate newly introduced premises.) |
|
935 |
||
47806 | 936 |
* Renamed some inner syntax categories: |
937 |
||
938 |
num ~> num_token |
|
939 |
xnum ~> xnum_token |
|
940 |
xstr ~> str_token |
|
941 |
||
942 |
Minor INCOMPATIBILITY. Note that in practice "num_const" or |
|
943 |
"num_position" etc. are mainly used instead (which also include |
|
944 |
position information via constraints). |
|
945 |
||
47829 | 946 |
* Simplified configuration options for syntax ambiguity: see |
947 |
"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref |
|
948 |
manual. Minor INCOMPATIBILITY. |
|
949 |
||
47856 | 950 |
* Discontinued configuration option "syntax_positions": atomic terms |
951 |
in parse trees are always annotated by position constraints. |
|
45134 | 952 |
|
47464 | 953 |
* Old code generator for SML and its commands 'code_module', |
45383 | 954 |
'code_library', 'consts_code', 'types_code' have been discontinued. |
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
955 |
Use commands of the generic code generator instead. INCOMPATIBILITY. |
45383 | 956 |
|
47464 | 957 |
* Redundant attribute "code_inline" has been discontinued. Use |
958 |
"code_unfold" instead. INCOMPATIBILITY. |
|
959 |
||
960 |
* Dropped attribute "code_unfold_post" in favor of the its dual |
|
961 |
"code_abbrev", which yields a common pattern in definitions like |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
962 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
963 |
definition [code_abbrev]: "f = t" |
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
964 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
965 |
INCOMPATIBILITY. |
45383 | 966 |
|
47856 | 967 |
* Obsolete 'types' command has been discontinued. Use 'type_synonym' |
968 |
instead. INCOMPATIBILITY. |
|
969 |
||
970 |
* Discontinued old "prems" fact, which used to refer to the accidental |
|
971 |
collection of foundational premises in the context (already marked as |
|
972 |
legacy since Isabelle2011). |
|
47855 | 973 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
974 |
|
45122 | 975 |
*** HOL *** |
976 |
||
47464 | 977 |
* Type 'a set is now a proper type constructor (just as before |
978 |
Isabelle2008). Definitions mem_def and Collect_def have disappeared. |
|
979 |
Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
|
47855 | 980 |
sets separate, it is often sufficient to rephrase some set S that has |
981 |
been accidentally used as predicates by "%x. x : S", and some |
|
982 |
predicate P that has been accidentally used as set by "{x. P x}". |
|
983 |
Corresponding proofs in a first step should be pruned from any |
|
984 |
tinkering with former theorems mem_def and Collect_def as far as |
|
985 |
possible. |
|
986 |
||
987 |
For developments which deliberately mix predicates and sets, a |
|
47464 | 988 |
planning step is necessary to determine what should become a predicate |
989 |
and what a set. It can be helpful to carry out that step in |
|
990 |
Isabelle2011-1 before jumping right into the current release. |
|
991 |
||
47855 | 992 |
* Code generation by default implements sets as container type rather |
993 |
than predicates. INCOMPATIBILITY. |
|
994 |
||
995 |
* New type synonym 'a rel = ('a * 'a) set |
|
996 |
||
47464 | 997 |
* The representation of numerals has changed. Datatype "num" |
998 |
represents strictly positive binary numerals, along with functions |
|
999 |
"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent |
|
47855 | 1000 |
positive and negated numeric literals, respectively. See also |
1001 |
definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some |
|
1002 |
user theories may require adaptations as follows: |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1003 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1004 |
- Theorems with number_ring or number_semiring constraints: These |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1005 |
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
|
1006 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1007 |
- Theories defining numeric types: Remove number, number_semiring, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1008 |
and number_ring instances. Defer all theorems about numerals until |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1009 |
after classes one and semigroup_add have been instantiated. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1010 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1011 |
- 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
|
1012 |
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
|
1013 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1014 |
- 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
|
1015 |
automatically support numerals now, so more simp rules and |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1016 |
simprocs may now apply within the proof. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1017 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1018 |
- Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1019 |
Redefine using other integer operations. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
1020 |
|
47855 | 1021 |
* Transfer: New package intended to generalize the existing |
1022 |
"descending" method and related theorem attributes from the Quotient |
|
1023 |
package. (Not all functionality is implemented yet, but future |
|
1024 |
development will focus on Transfer as an eventual replacement for the |
|
1025 |
corresponding parts of the Quotient package.) |
|
47809 | 1026 |
|
1027 |
- transfer_rule attribute: Maintains a collection of transfer rules, |
|
1028 |
which relate constants at two different types. Transfer rules may |
|
1029 |
relate different type instances of the same polymorphic constant, |
|
1030 |
or they may relate an operation on a raw type to a corresponding |
|
1031 |
operation on an abstract type (quotient or subtype). For example: |
|
1032 |
||
1033 |
((A ===> B) ===> list_all2 A ===> list_all2 B) map map |
|
1034 |
(cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int |
|
1035 |
||
1036 |
- transfer method: Replaces a subgoal on abstract types with an |
|
1037 |
equivalent subgoal on the corresponding raw types. Constants are |
|
1038 |
replaced with corresponding ones according to the transfer rules. |
|
1039 |
Goals are generalized over all free variables by default; this is |
|
47851 | 1040 |
necessary for variables whose types change, but can be overridden |
47855 | 1041 |
for specific variables with e.g. "transfer fixing: x y z". The |
47809 | 1042 |
variant transfer' method allows replacing a subgoal with one that |
1043 |
is logically stronger (rather than equivalent). |
|
1044 |
||
1045 |
- relator_eq attribute: Collects identity laws for relators of |
|
1046 |
various type constructors, e.g. "list_all2 (op =) = (op =)". The |
|
1047 |
transfer method uses these lemmas to infer transfer rules for |
|
1048 |
non-polymorphic constants on the fly. |
|
1049 |
||
1050 |
- transfer_prover method: Assists with proving a transfer rule for a |
|
1051 |
new constant, provided the constant is defined in terms of other |
|
1052 |
constants that already have transfer rules. It should be applied |
|
1053 |
after unfolding the constant definitions. |
|
1054 |
||
1055 |
- HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer |
|
1056 |
from type nat to type int. |
|
1057 |
||
47851 | 1058 |
* Lifting: New package intended to generalize the quotient_definition |
1059 |
facility of the Quotient package; designed to work with Transfer. |
|
47809 | 1060 |
|
1061 |
- lift_definition command: Defines operations on an abstract type in |
|
1062 |
terms of a corresponding operation on a representation |
|
1063 |
type. Example syntax: |
|
1064 |
||
1065 |
lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" |
|
1066 |
is List.insert |
|
1067 |
||
1068 |
Users must discharge a respectfulness proof obligation when each |
|
1069 |
constant is defined. (For a type copy, i.e. a typedef with UNIV, |
|
1070 |
the proof is discharged automatically.) The obligation is |
|
1071 |
presented in a user-friendly, readable form; a respectfulness |
|
1072 |
theorem in the standard format and a transfer rule are generated |
|
1073 |
by the package. |
|
1074 |
||
1075 |
- Integration with code_abstype: For typedefs (e.g. subtypes |
|
1076 |
corresponding to a datatype invariant, such as dlist), |
|
1077 |
lift_definition generates a code certificate theorem and sets up |
|
1078 |
code generation for each constant. |
|
1079 |
||
1080 |
- setup_lifting command: Sets up the Lifting package to work with a |
|
1081 |
user-defined type. The user must provide either a quotient theorem |
|
1082 |
or a type_definition theorem. The package configures transfer |
|
1083 |
rules for equality and quantifiers on the type, and sets up the |
|
1084 |
lift_definition command to work with the type. |
|
1085 |
||
1086 |
- Usage examples: See Quotient_Examples/Lift_DList.thy, |
|
47851 | 1087 |
Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy, |
1088 |
Word/Word.thy and Library/Float.thy. |
|
47809 | 1089 |
|
1090 |
* Quotient package: |
|
1091 |
||
1092 |
- The 'quotient_type' command now supports a 'morphisms' option with |
|
1093 |
rep and abs functions, similar to typedef. |
|
1094 |
||
1095 |
- 'quotient_type' sets up new types to work with the Lifting and |
|
1096 |
Transfer packages, as with 'setup_lifting'. |
|
1097 |
||
1098 |
- The 'quotient_definition' command now requires the user to prove a |
|
1099 |
respectfulness property at the point where the constant is |
|
1100 |
defined, similar to lift_definition; INCOMPATIBILITY. |
|
1101 |
||
1102 |
- Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems |
|
1103 |
accordingly, INCOMPATIBILITY. |
|
1104 |
||
1105 |
* New diagnostic command 'find_unused_assms' to find potentially |
|
1106 |
superfluous assumptions in theorems using Quickcheck. |
|
1107 |
||
1108 |
* Quickcheck: |
|
1109 |
||
1110 |
- Quickcheck returns variable assignments as counterexamples, which |
|
1111 |
allows to reveal the underspecification of functions under test. |
|
1112 |
For example, refuting "hd xs = x", it presents the variable |
|
1113 |
assignment xs = [] and x = a1 as a counterexample, assuming that |
|
1114 |
any property is false whenever "hd []" occurs in it. |
|
1115 |
||
1116 |
These counterexample are marked as potentially spurious, as |
|
1117 |
Quickcheck also returns "xs = []" as a counterexample to the |
|
1118 |
obvious theorem "hd xs = hd xs". |
|
1119 |
||
1120 |
After finding a potentially spurious counterexample, Quickcheck |
|
1121 |
continues searching for genuine ones. |
|
1122 |
||
1123 |
By default, Quickcheck shows potentially spurious and genuine |
|
1124 |
counterexamples. The option "genuine_only" sets quickcheck to only |
|
1125 |
show genuine counterexamples. |
|
1126 |
||
1127 |
- The command 'quickcheck_generator' creates random and exhaustive |
|
1128 |
value generators for a given type and operations. |
|
1129 |
||
1130 |
It generates values by using the operations as if they were |
|
1131 |
constructors of that type. |
|
1132 |
||
1133 |
- Support for multisets. |
|
1134 |
||
1135 |
- Added "use_subtype" options. |
|
1136 |
||
1137 |
- Added "quickcheck_locale" configuration to specify how to process |
|
1138 |
conjectures in a locale context. |
|
1139 |
||
47855 | 1140 |
* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option |
1141 |
and affecting 'rat' and 'real'. |
|
47809 | 1142 |
|
1143 |
* Sledgehammer: |
|
1144 |
- Integrated more tightly with SPASS, as described in the ITP 2012 |
|
1145 |
paper "More SPASS with Isabelle". |
|
1146 |
- Made it try "smt" as a fallback if "metis" fails or times out. |
|
1147 |
- Added support for the following provers: Alt-Ergo (via Why3 and |
|
1148 |
TFF1), iProver, iProver-Eq. |
|
1149 |
- Sped up the minimizer. |
|
1150 |
- Added "lam_trans", "uncurry_aliases", and "minimize" options. |
|
1151 |
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). |
|
1152 |
- Renamed "sound" option to "strict". |
|
1153 |
||
47855 | 1154 |
* Metis: Added possibility to specify lambda translations scheme as a |
1155 |
parenthesized argument (e.g., "by (metis (lifting) ...)"). |
|
1156 |
||
1157 |
* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates". |
|
1158 |
||
1159 |
* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY. |
|
47809 | 1160 |
|
47856 | 1161 |
* New "case_product" attribute to generate a case rule doing multiple |
1162 |
case distinctions at the same time. E.g. |
|
1163 |
||
1164 |
list.exhaust [case_product nat.exhaust] |
|
1165 |
||
1166 |
produces a rule which can be used to perform case distinction on both |
|
1167 |
a list and a nat. |
|
1168 |
||
47809 | 1169 |
* New "eventually_elim" method as a generalized variant of the |
47855 | 1170 |
eventually_elim* rules. Supports structured proofs. |
1171 |
||
47702
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
1172 |
* Typedef with implicit set definition is considered legacy. Use |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
1173 |
"typedef (open)" form instead, which will eventually become the |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
1174 |
default. |
5f9ce06f281e
typedef with implicit set definition is considered legacy;
wenzelm
parents:
47694
diff
changeset
|
1175 |
|
47856 | 1176 |
* Record: code generation can be switched off manually with |
1177 |
||
1178 |
declare [[record_coden = false]] -- "default true" |
|
1179 |
||
1180 |
* Datatype: type parameters allow explicit sort constraints. |
|
1181 |
||
47855 | 1182 |
* Concrete syntax for case expressions includes constraints for source |
1183 |
positions, and thus produces Prover IDE markup for its bindings. |
|
1184 |
INCOMPATIBILITY for old-style syntax translations that augment the |
|
1185 |
pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
|
1186 |
one_case. |
|
1187 |
||
1188 |
* Clarified attribute "mono_set": pure declaration without modifying |
|
1189 |
the result of the fact expression. |
|
1190 |
||
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
|
1191 |
* More default pred/set conversions on a couple of relation operations |
47464 | 1192 |
and predicates. Added powers of predicate relations. Consolidation |
1193 |
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
|
1194 |
|
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
|
1195 |
converse_def ~> converse_unfold |
47549 | 1196 |
rel_comp_def ~> relcomp_unfold |
47820 | 1197 |
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
|
1198 |
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
|
1199 |
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
|
1200 |
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
|
1201 |
|
46981 | 1202 |
Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. |
1203 |
||
47464 | 1204 |
See theory "Relation" for examples for making use of pred/set |
1205 |
conversions by means of attributes "to_set" and "to_pred". |
|
47086 | 1206 |
|
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
|
1207 |
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
|
1208 |
|
46363 | 1209 |
* Renamed facts about the power operation on relations, i.e., relpow |
47464 | 1210 |
to match the constant's name: |
47463 | 1211 |
|
46458 | 1212 |
rel_pow_1 ~> relpow_1 |
46363 | 1213 |
rel_pow_0_I ~> relpow_0_I |
1214 |
rel_pow_Suc_I ~> relpow_Suc_I |
|
1215 |
rel_pow_Suc_I2 ~> relpow_Suc_I2 |
|
1216 |
rel_pow_0_E ~> relpow_0_E |
|
1217 |
rel_pow_Suc_E ~> relpow_Suc_E |
|
1218 |
rel_pow_E ~> relpow_E |
|
46458 | 1219 |
rel_pow_Suc_D2 ~> relpow_Suc_D2 |
47463 | 1220 |
rel_pow_Suc_E2 ~> relpow_Suc_E2 |
46363 | 1221 |
rel_pow_Suc_D2' ~> relpow_Suc_D2' |
1222 |
rel_pow_E2 ~> relpow_E2 |
|
1223 |
rel_pow_add ~> relpow_add |
|
1224 |
rel_pow_commute ~> relpow |
|
1225 |
rel_pow_empty ~> relpow_empty: |
|
1226 |
rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow |
|
1227 |
rel_pow_imp_rtrancl ~> relpow_imp_rtrancl |
|
1228 |
rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow |
|
1229 |
rtrancl_imp_rel_pow ~> rtrancl_imp_relpow |
|
1230 |
rel_pow_fun_conv ~> relpow_fun_conv |
|
1231 |
rel_pow_finite_bounded1 ~> relpow_finite_bounded1 |
|
1232 |
rel_pow_finite_bounded ~> relpow_finite_bounded |
|
1233 |
rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow |
|
1234 |
trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow |
|
1235 |
single_valued_rel_pow ~> single_valued_relpow |
|
47463 | 1236 |
|
46363 | 1237 |
INCOMPATIBILITY. |
1238 |
||
47448 | 1239 |
* Theory Relation: Consolidated constant name for relation composition |
47464 | 1240 |
and corresponding theorem names: |
1241 |
||
47549 | 1242 |
- Renamed constant rel_comp to relcomp. |
47464 | 1243 |
|
47448 | 1244 |
- Dropped abbreviation pred_comp. Use relcompp instead. |
47464 | 1245 |
|
47448 | 1246 |
- Renamed theorems: |
47464 | 1247 |
|
47448 | 1248 |
rel_compI ~> relcompI |
1249 |
rel_compEpair ~> relcompEpair |
|
1250 |
rel_compE ~> relcompE |
|
1251 |
pred_comp_rel_comp_eq ~> relcompp_relcomp_eq |
|
1252 |
rel_comp_empty1 ~> relcomp_empty1 |
|
1253 |
rel_comp_mono ~> relcomp_mono |
|
1254 |
rel_comp_subset_Sigma ~> relcomp_subset_Sigma |
|
1255 |
rel_comp_distrib ~> relcomp_distrib |
|
1256 |
rel_comp_distrib2 ~> relcomp_distrib2 |
|
1257 |
rel_comp_UNION_distrib ~> relcomp_UNION_distrib |
|
1258 |
rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2 |
|
1259 |
single_valued_rel_comp ~> single_valued_relcomp |
|
47549 | 1260 |
rel_comp_def ~> relcomp_unfold |
47448 | 1261 |
converse_rel_comp ~> converse_relcomp |
1262 |
pred_compI ~> relcomppI |
|
1263 |
pred_compE ~> relcomppE |
|
1264 |
pred_comp_bot1 ~> relcompp_bot1 |
|
1265 |
pred_comp_bot2 ~> relcompp_bot2 |
|
1266 |
transp_pred_comp_less_eq ~> transp_relcompp_less_eq |
|
1267 |
pred_comp_mono ~> relcompp_mono |
|
1268 |
pred_comp_distrib ~> relcompp_distrib |
|
1269 |
pred_comp_distrib2 ~> relcompp_distrib2 |
|
1270 |
converse_pred_comp ~> converse_relcompp |
|
47464 | 1271 |
|
47448 | 1272 |
finite_rel_comp ~> finite_relcomp |
47464 | 1273 |
|
47448 | 1274 |
set_rel_comp ~> set_relcomp |
1275 |
||
1276 |
INCOMPATIBILITY. |
|
1277 |
||
47550 | 1278 |
* Theory Divides: Discontinued redundant theorems about div and mod. |
1279 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
1280 |
||
1281 |
DIVISION_BY_ZERO ~> div_by_0, mod_by_0 |
|
1282 |
zdiv_self ~> div_self |
|
1283 |
zmod_self ~> mod_self |
|
1284 |
zdiv_zero ~> div_0 |
|
1285 |
zmod_zero ~> mod_0 |
|
1286 |
zdiv_zmod_equality ~> div_mod_equality2 |
|
1287 |
zdiv_zmod_equality2 ~> div_mod_equality |
|
1288 |
zmod_zdiv_trivial ~> mod_div_trivial |
|
1289 |
zdiv_zminus_zminus ~> div_minus_minus |
|
1290 |
zmod_zminus_zminus ~> mod_minus_minus |
|
1291 |
zdiv_zminus2 ~> div_minus_right |
|
1292 |
zmod_zminus2 ~> mod_minus_right |
|
1293 |
zdiv_minus1_right ~> div_minus1_right |
|
1294 |
zmod_minus1_right ~> mod_minus1_right |
|
1295 |
zdvd_mult_div_cancel ~> dvd_mult_div_cancel |
|
1296 |
zmod_zmult1_eq ~> mod_mult_right_eq |
|
1297 |
zpower_zmod ~> power_mod |
|
1298 |
zdvd_zmod ~> dvd_mod |
|
1299 |
zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd |
|
1300 |
mod_mult_distrib ~> mult_mod_left |
|
1301 |
mod_mult_distrib2 ~> mult_mod_right |
|
1302 |
||
1303 |
* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use |
|
1304 |
generic mult_2 and mult_2_right instead. INCOMPATIBILITY. |
|
1305 |
||
47551 | 1306 |
* Finite_Set.fold now qualified. INCOMPATIBILITY. |
1307 |
||
47552 | 1308 |
* Consolidated theorem names concerning fold combinators: |
47550 | 1309 |
|
1310 |
inf_INFI_fold_inf ~> inf_INF_fold_inf |
|
1311 |
sup_SUPR_fold_sup ~> sup_SUP_fold_sup |
|
1312 |
INFI_fold_inf ~> INF_fold_inf |
|
1313 |
SUPR_fold_sup ~> SUP_fold_sup |
|
1314 |
union_set ~> union_set_fold |
|
1315 |
minus_set ~> minus_set_fold |
|
1316 |
INFI_set_fold ~> INF_set_fold |
|
1317 |
SUPR_set_fold ~> SUP_set_fold |
|
1318 |
INF_code ~> INF_set_foldr |
|
1319 |
SUP_code ~> SUP_set_foldr |
|
1320 |
foldr.simps ~> foldr.simps (in point-free formulation) |
|
1321 |
foldr_fold_rev ~> foldr_conv_fold |
|
1322 |
foldl_fold ~> foldl_conv_fold |
|
1323 |
foldr_foldr ~> foldr_conv_foldl |
|
1324 |
foldl_foldr ~> foldl_conv_foldr |
|
47552 | 1325 |
fold_set_remdups ~> fold_set_fold_remdups |
1326 |
fold_set ~> fold_set_fold |
|
1327 |
fold1_set ~> fold1_set_fold |
|
47550 | 1328 |
|
1329 |
INCOMPATIBILITY. |
|
1330 |
||
1331 |
* Dropped rarely useful theorems concerning fold combinators: |
|
1332 |
foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant, |
|
1333 |
rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, |
|
1334 |
concat_conv_foldl, foldl_weak_invariant, foldl_invariant, |
|
1335 |
foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, |
|
1336 |
listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, |
|
1337 |
foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. |
|
1338 |
INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" |
|
1339 |
and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be |
|
1340 |
useful to boil down "List.foldr" and "List.foldl" to "List.fold" by |
|
1341 |
unfolding "foldr_conv_fold" and "foldl_conv_fold". |
|
1342 |
||
1343 |
* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, |
|
1344 |
inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, |
|
1345 |
Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr, |
|
1346 |
INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding |
|
1347 |
lemmas over fold rather than foldr, or make use of lemmas |
|
1348 |
fold_conv_foldr and fold_rev. |
|
1349 |
||
1350 |
* Congruence rules Option.map_cong and Option.bind_cong for recursion |
|
1351 |
through option types. |
|
1352 |
||
47856 | 1353 |
* "Transitive_Closure.ntrancl": bounded transitive closure on |
1354 |
relations. |
|
1355 |
||
1356 |
* Constant "Set.not_member" now qualified. INCOMPATIBILITY. |
|
1357 |
||
1358 |
* Theory Int: Discontinued many legacy theorems specific to type int. |
|
1359 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
1360 |
||
1361 |
zminus_zminus ~> minus_minus |
|
1362 |
zminus_0 ~> minus_zero |
|
1363 |
zminus_zadd_distrib ~> minus_add_distrib |
|
1364 |
zadd_commute ~> add_commute |
|
1365 |
zadd_assoc ~> add_assoc |
|
1366 |
zadd_left_commute ~> add_left_commute |
|
1367 |
zadd_ac ~> add_ac |
|
1368 |
zmult_ac ~> mult_ac |
|
1369 |
zadd_0 ~> add_0_left |
|
1370 |
zadd_0_right ~> add_0_right |
|
1371 |
zadd_zminus_inverse2 ~> left_minus |
|
1372 |
zmult_zminus ~> mult_minus_left |
|
1373 |
zmult_commute ~> mult_commute |
|
1374 |
zmult_assoc ~> mult_assoc |
|
1375 |
zadd_zmult_distrib ~> left_distrib |
|
1376 |
zadd_zmult_distrib2 ~> right_distrib |
|
1377 |
zdiff_zmult_distrib ~> left_diff_distrib |
|
1378 |
zdiff_zmult_distrib2 ~> right_diff_distrib |
|
1379 |
zmult_1 ~> mult_1_left |
|
1380 |
zmult_1_right ~> mult_1_right |
|
1381 |
zle_refl ~> order_refl |
|
1382 |
zle_trans ~> order_trans |
|
1383 |
zle_antisym ~> order_antisym |
|
1384 |
zle_linear ~> linorder_linear |
|
1385 |
zless_linear ~> linorder_less_linear |
|
1386 |
zadd_left_mono ~> add_left_mono |
|
1387 |
zadd_strict_right_mono ~> add_strict_right_mono |
|
1388 |
zadd_zless_mono ~> add_less_le_mono |
|
1389 |
int_0_less_1 ~> zero_less_one |
|
1390 |
int_0_neq_1 ~> zero_neq_one |
|
1391 |
zless_le ~> less_le |
|
1392 |
zpower_zadd_distrib ~> power_add |
|
1393 |
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
|
1394 |
zero_le_zpower_abs ~> zero_le_power_abs |
|
1395 |
||
1396 |
* Theory Deriv: Renamed |
|
1397 |
||
1398 |
DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing |
|
1399 |
||
1400 |
* Theory Library/Multiset: Improved code generation of multisets. |
|
1401 |
||
47855 | 1402 |
* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets |
47703 | 1403 |
are expressed via type classes again. The special syntax |
1404 |
\<oplus>/\<otimes> has been replaced by plain +/*. Removed constant |
|
1405 |
setsum_set, which is now subsumed by Big_Operators.setsum. |
|
1406 |
INCOMPATIBILITY. |
|
1407 |
||
46160 | 1408 |
* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, |
1409 |
use theory HOL/Library/Nat_Bijection instead. |
|
1410 |
||
47464 | 1411 |
* Theory HOL/Library/RBT_Impl: Backing implementation of red-black |
1412 |
trees is now inside a type class context. Names of affected |
|
1413 |
operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for |
|
1414 |
theories working directly with raw red-black trees, adapt the names as |
|
1415 |
follows: |
|
47452 | 1416 |
|
1417 |
Operations: |
|
1418 |
bulkload -> rbt_bulkload |
|
1419 |
del_from_left -> rbt_del_from_left |
|
1420 |
del_from_right -> rbt_del_from_right |
|
1421 |
del -> rbt_del |
|
1422 |
delete -> rbt_delete |
|
1423 |
ins -> rbt_ins |
|
1424 |
insert -> rbt_insert |
|
1425 |
insertw -> rbt_insert_with |
|
1426 |
insert_with_key -> rbt_insert_with_key |
|
1427 |
map_entry -> rbt_map_entry |
|
1428 |
lookup -> rbt_lookup |
|
1429 |
sorted -> rbt_sorted |
|
1430 |
tree_greater -> rbt_greater |
|