author | huffman |
Sun, 09 Oct 2011 11:13:53 +0200 | |
changeset 45122 | 49e305100097 |
parent 45109 | 20b3377b08d7 |
child 45128 | 5af3a3203a76 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
45109 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
45122 | 7 |
*** HOL *** |
8 |
||
9 |
* Theory Int: Discontinued many legacy theorems specific to type int. |
|
10 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
11 |
||
12 |
zminus_zminus ~> minus_minus |
|
13 |
zminus_0 ~> minus_zero |
|
14 |
zminus_zadd_distrib ~> minus_add_distrib |
|
15 |
zadd_commute ~> add_commute |
|
16 |
zadd_assoc ~> add_assoc |
|
17 |
zadd_left_commute ~> add_left_commute |
|
18 |
zmult_ac ~> mult_ac |
|
19 |
zadd_0 ~> add_0_left |
|
20 |
zadd_0_right ~> add_0_right |
|
21 |
zadd_zminus_inverse2 ~> left_minus |
|
22 |
zmult_zminus ~> mult_minus_left |
|
23 |
zmult_commute ~> mult_commute |
|
24 |
zmult_assoc ~> mult_assoc |
|
25 |
zadd_zmult_distrib ~> left_distrib |
|
26 |
zadd_zmult_distrib2 ~> right_distrib |
|
27 |
zdiff_zmult_distrib ~> left_diff_distrib |
|
28 |
zdiff_zmult_distrib2 ~> right_diff_distrib |
|
29 |
zmult_1 ~> mult_1_left |
|
30 |
zmult_1_right ~> mult_1_right |
|
31 |
zle_refl ~> order_refl |
|
32 |
zle_trans ~> order_trans |
|
33 |
zle_antisym ~> order_antisym |
|
34 |
zle_linear ~> linorder_linear |
|
35 |
zless_linear ~> linorder_less_linear |
|
36 |
zadd_left_mono ~> add_left_mono |
|
37 |
zadd_strict_right_mono ~> add_strict_right_mono |
|
38 |
zadd_zless_mono ~> add_less_le_mono |
|
39 |
int_0_less_1 ~> zero_less_one |
|
40 |
int_0_neq_1 ~> zero_neq_one |
|
41 |
zless_le ~> less_le |
|
42 |
zpower_zadd_distrib ~> power_add |
|
43 |
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
|
44 |
zero_le_zpower_abs ~> zero_le_power_abs |
|
45 |
||
45109 | 46 |
|
47 |
||
44801 | 48 |
New in Isabelle2011-1 (October 2011) |
49 |
------------------------------------ |
|
41651 | 50 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
51 |
*** General *** |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
52 |
|
44760 | 53 |
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as |
44968 | 54 |
"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line. |
44760 | 55 |
|
44777 | 56 |
- Management of multiple theory files directly from the editor |
44760 | 57 |
buffer store -- bypassing the file-system (no requirement to save |
58 |
files for checking). |
|
59 |
||
44777 | 60 |
- Markup of formal entities within the text buffer, with semantic |
44760 | 61 |
highlighting, tooltips and hyperlinks to jump to defining source |
62 |
positions. |
|
63 |
||
44777 | 64 |
- Improved text rendering, with sub/superscripts in the source |
65 |
buffer (including support for copy/paste wrt. output panel, HTML |
|
66 |
theory output and other non-Isabelle text boxes). |
|
67 |
||
68 |
- Refined scheduling of proof checking and printing of results, |
|
44760 | 69 |
based on interactive editor view. (Note: jEdit folding and |
70 |
narrowing allows to restrict buffer perspectives explicitly.) |
|
71 |
||
44777 | 72 |
- Reduced CPU performance requirements, usable on machines with few |
44760 | 73 |
cores. |
74 |
||
44777 | 75 |
- Reduced memory requirements due to pruning of unused document |
44760 | 76 |
versions (garbage collection). |
77 |
||
78 |
See also ~~/src/Tools/jEdit/README.html for further information, |
|
79 |
including some remaining limitations. |
|
80 |
||
44800 | 81 |
* Theory loader: source files are exclusively located via the master |
82 |
directory of each theory node (where the .thy file itself resides). |
|
83 |
The global load path (such as src/HOL/Library) has been discontinued. |
|
84 |
Note that the path element ~~ may be used to reference theories in the |
|
85 |
Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". |
|
86 |
INCOMPATIBILITY. |
|
87 |
||
41955
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
88 |
* Theory loader: source files are identified by content via SHA1 |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
89 |
digests. Discontinued former path/modtime identification and optional |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
90 |
ISABELLE_FILE_IDENT plugin scripts. |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
91 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
92 |
* Parallelization of nested Isar proofs is subject to |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
93 |
Goal.parallel_proofs_threshold (default 100). See also isabelle |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
94 |
usedir option -Q. |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
95 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
96 |
* Name space: former unsynchronized references are now proper |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
97 |
configuration options, with more conventional names: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
98 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
99 |
long_names ~> names_long |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
100 |
short_names ~> names_short |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
101 |
unique_names ~> names_unique |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
102 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
103 |
Minor INCOMPATIBILITY, need to declare options in context like this: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
104 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
105 |
declare [[names_unique = false]] |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42290
diff
changeset
|
106 |
|
42502 | 107 |
* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note |
108 |
that the result needs to be unique, which means fact specifications |
|
109 |
may have to be refined after enriching a proof context. |
|
110 |
||
44800 | 111 |
* Attribute "case_names" has been refined: the assumptions in each case |
112 |
can be named now by following the case name with [name1 name2 ...]. |
|
113 |
||
44968 | 114 |
* Isabelle/Isar reference manual has been updated and extended: |
115 |
- "Synopsis" provides a catalog of main Isar language concepts. |
|
116 |
- Formal references in syntax diagrams, via @{rail} antiquotation. |
|
117 |
- Updated material from classic "ref" manual, notably about |
|
118 |
"Classical Reasoner". |
|
42633 | 119 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
120 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
121 |
*** HOL *** |
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
122 |
|
44968 | 123 |
* Class bot and top require underlying partial order rather than |
44800 | 124 |
preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
43752
diff
changeset
|
125 |
|
43940 | 126 |
* Class complete_lattice: generalized a couple of lemmas from sets; |
44800 | 127 |
generalized theorems INF_cong and SUP_cong. New type classes for |
128 |
complete boolean algebras and complete linear orders. Lemmas |
|
129 |
Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in |
|
130 |
class complete_linorder. |
|
131 |
||
132 |
Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
|
133 |
Sup_fun_def, Inf_apply, Sup_apply. |
|
134 |
||
45088 | 135 |
Removed redundant lemmas (the right hand side gives hints how to |
136 |
replace them for (metis ...), or (simp only: ...) proofs): |
|
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
137 |
|
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
138 |
Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
139 |
Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
140 |
Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
141 |
Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
142 |
Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
143 |
Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
144 |
Inter_def ~> INF_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
145 |
Union_def ~> SUP_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
146 |
INT_eq ~> INF_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
147 |
UN_eq ~> SUP_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
148 |
INF_subset ~> INF_superset_mono [OF _ order_refl] |
44800 | 149 |
|
150 |
More consistent and comprehensive names: |
|
151 |
||
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
152 |
INTER_eq_Inter_image ~> INF_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
153 |
UNION_eq_Union_image ~> SUP_def |
43872 | 154 |
INFI_def ~> INF_def |
155 |
SUPR_def ~> SUP_def |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
156 |
INF_leI ~> INF_lower |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
157 |
INF_leI2 ~> INF_lower2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
158 |
le_INFI ~> INF_greatest |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
159 |
le_SUPI ~> SUP_upper |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
160 |
le_SUPI2 ~> SUP_upper2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
161 |
SUP_leI ~> SUP_least |
43873 | 162 |
INFI_bool_eq ~> INF_bool_eq |
163 |
SUPR_bool_eq ~> SUP_bool_eq |
|
164 |
INFI_apply ~> INF_apply |
|
165 |
SUPR_apply ~> SUP_apply |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
166 |
INTER_def ~> INTER_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
167 |
UNION_def ~> UNION_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
168 |
|
43865
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
169 |
INCOMPATIBILITY. |
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
170 |
|
44973
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
171 |
* Renamed theory Complete_Lattice to Complete_Lattices. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
172 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
173 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
174 |
* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
175 |
INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
176 |
Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
177 |
Sup_insert are now declared as [simp]. INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
178 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
179 |
* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
180 |
compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
181 |
sup_inf_absob, sup_left_idem are now declared as [simp]. Minor |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
182 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
183 |
|
44845 | 184 |
* Added syntactic classes "inf" and "sup" for the respective |
185 |
constants. INCOMPATIBILITY: Changes in the argument order of the |
|
186 |
(mostly internal) locale predicates for some derived classes. |
|
187 |
||
44800 | 188 |
* Theorem collections ball_simps and bex_simps do not contain theorems |
189 |
referring to UNION any longer; these have been moved to collection |
|
190 |
UN_ball_bex_simps. INCOMPATIBILITY. |
|
191 |
||
192 |
* Theory Archimedean_Field: floor now is defined as parameter of a |
|
193 |
separate type class floor_ceiling. |
|
194 |
||
195 |
* Theory Finite_Set: more coherent development of fold_set locales: |
|
42874 | 196 |
|
197 |
locale fun_left_comm ~> locale comp_fun_commute |
|
198 |
locale fun_left_comm_idem ~> locale comp_fun_idem |
|
44800 | 199 |
|
200 |
Both use point-free characterization; interpretation proofs may need |
|
201 |
adjustment. INCOMPATIBILITY. |
|
42874 | 202 |
|
44800 | 203 |
* Theory Limits: Type "'a net" has been renamed to "'a filter", in |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
204 |
accordance with standard mathematical terminology. INCOMPATIBILITY. |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
205 |
|
44800 | 206 |
* Theory Complex_Main: The locale interpretations for the |
207 |
bounded_linear and bounded_bilinear locales have been removed, in |
|
208 |
order to reduce the number of duplicate lemmas. Users must use the |
|
209 |
original names for distributivity theorems, potential INCOMPATIBILITY. |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
210 |
|
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
211 |
divide.add ~> add_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
212 |
divide.diff ~> diff_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
213 |
divide.setsum ~> setsum_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
214 |
mult.add_right ~> right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
215 |
mult.diff_right ~> right_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
216 |
mult_right.setsum ~> setsum_right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
217 |
mult_left.diff ~> left_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
218 |
|
44800 | 219 |
* Theory Complex_Main: Several redundant theorems have been removed or |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
220 |
replaced by more general versions. INCOMPATIBILITY. |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
221 |
|
45051
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
222 |
real_diff_def ~> minus_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
223 |
real_divide_def ~> divide_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
224 |
real_less_def ~> less_le |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
225 |
real_abs_def ~> abs_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
226 |
real_sgn_def ~> sgn_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
227 |
real_mult_commute ~> mult_commute |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
228 |
real_mult_assoc ~> mult_assoc |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
229 |
real_mult_1 ~> mult_1_left |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
230 |
real_add_mult_distrib ~> left_distrib |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
231 |
real_zero_not_eq_one ~> zero_neq_one |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
232 |
real_mult_inverse_left ~> left_inverse |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
233 |
INVERSE_ZERO ~> inverse_zero |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
234 |
real_le_refl ~> order_refl |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
235 |
real_le_antisym ~> order_antisym |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
236 |
real_le_trans ~> order_trans |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
237 |
real_le_linear ~> linear |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
238 |
real_le_eq_diff ~> le_iff_diff_le_0 |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
239 |
real_add_left_mono ~> add_left_mono |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
240 |
real_mult_order ~> mult_pos_pos |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
241 |
real_mult_less_mono2 ~> mult_strict_left_mono |
44822
2690b6de5021
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
huffman
parents:
44777
diff
changeset
|
242 |
real_of_int_real_of_nat ~> real_of_int_of_nat_eq |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
243 |
real_0_le_divide_iff ~> zero_le_divide_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
244 |
realpow_two_disj ~> power2_eq_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
245 |
real_squared_diff_one_factored ~> square_diff_one_factored |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
246 |
realpow_two_diff ~> square_diff_square_factored |
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
44666
diff
changeset
|
247 |
reals_complete2 ~> complete_real |
44749
5b1e1432c320
remove redundant lemma real_sum_squared_expand in favor of power2_sum
huffman
parents:
44748
diff
changeset
|
248 |
real_sum_squared_expand ~> power2_sum |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
249 |
exp_ln_eq ~> ln_unique |
44711 | 250 |
expi_add ~> exp_add |
251 |
expi_zero ~> exp_zero |
|
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
252 |
lemma_DERIV_subst ~> DERIV_cong |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
253 |
LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
254 |
LIMSEQ_const ~> tendsto_const |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
255 |
LIMSEQ_norm ~> tendsto_norm |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
256 |
LIMSEQ_add ~> tendsto_add |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
257 |
LIMSEQ_minus ~> tendsto_minus |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
258 |
LIMSEQ_minus_cancel ~> tendsto_minus_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
259 |
LIMSEQ_diff ~> tendsto_diff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
260 |
bounded_linear.LIMSEQ ~> bounded_linear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
261 |
bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
262 |
LIMSEQ_mult ~> tendsto_mult |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
263 |
LIMSEQ_inverse ~> tendsto_inverse |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
264 |
LIMSEQ_divide ~> tendsto_divide |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
265 |
LIMSEQ_pow ~> tendsto_power |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
266 |
LIMSEQ_setsum ~> tendsto_setsum |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
267 |
LIMSEQ_setprod ~> tendsto_setprod |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
268 |
LIMSEQ_norm_zero ~> tendsto_norm_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
269 |
LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
270 |
LIMSEQ_imp_rabs ~> tendsto_rabs |
44710 | 271 |
LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] |
272 |
LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] |
|
273 |
LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] |
|
44748
7f6838b3474a
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
huffman
parents:
44711
diff
changeset
|
274 |
LIMSEQ_Complex ~> tendsto_Complex |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
275 |
LIM_ident ~> tendsto_ident_at |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
276 |
LIM_const ~> tendsto_const |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
277 |
LIM_add ~> tendsto_add |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
278 |
LIM_add_zero ~> tendsto_add_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
279 |
LIM_minus ~> tendsto_minus |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
280 |
LIM_diff ~> tendsto_diff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
281 |
LIM_norm ~> tendsto_norm |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
282 |
LIM_norm_zero ~> tendsto_norm_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
283 |
LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
284 |
LIM_norm_zero_iff ~> tendsto_norm_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
285 |
LIM_rabs ~> tendsto_rabs |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
286 |
LIM_rabs_zero ~> tendsto_rabs_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
287 |
LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
288 |
LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
289 |
LIM_compose ~> tendsto_compose |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
290 |
LIM_mult ~> tendsto_mult |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
291 |
LIM_scaleR ~> tendsto_scaleR |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
292 |
LIM_of_real ~> tendsto_of_real |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
293 |
LIM_power ~> tendsto_power |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
294 |
LIM_inverse ~> tendsto_inverse |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
295 |
LIM_sgn ~> tendsto_sgn |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
296 |
isCont_LIM_compose ~> isCont_tendsto_compose |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
297 |
bounded_linear.LIM ~> bounded_linear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
298 |
bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
299 |
bounded_bilinear.LIM ~> bounded_bilinear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
300 |
bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
301 |
bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
302 |
bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
303 |
LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
304 |
|
44967 | 305 |
* Theory Complex_Main: The definition of infinite series was |
306 |
generalized. Now it is defined on the type class {topological_space, |
|
307 |
comm_monoid_add}. Hence it is useable also for extended real numbers. |
|
42484 | 308 |
|
44908 | 309 |
* Theory Complex_Main: The complex exponential function "expi" is now |
310 |
a type-constrained abbreviation for "exp :: complex => complex"; thus |
|
311 |
several polymorphic lemmas about "exp" are now applicable to "expi". |
|
312 |
||
44968 | 313 |
* Code generation: |
314 |
||
315 |
- Theory Library/Code_Char_ord provides native ordering of |
|
316 |
characters in the target language. |
|
317 |
||
318 |
- Commands code_module and code_library are legacy, use export_code |
|
319 |
instead. |
|
320 |
||
321 |
- Method "evaluation" is legacy, use method "eval" instead. |
|
322 |
||
323 |
- Legacy evaluator "SML" is deactivated by default. May be |
|
324 |
reactivated by the following theory command: |
|
325 |
||
326 |
setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} |
|
327 |
||
328 |
* Declare ext [intro] by default. Rare INCOMPATIBILITY. |
|
329 |
||
45088 | 330 |
* New proof method "induction" that gives induction hypotheses the |
331 |
name "IH", thus distinguishing them from further hypotheses that come |
|
332 |
from rule induction. The latter are still called "hyps". Method |
|
333 |
"induction" is a thin wrapper around "induct" and follows the same |
|
334 |
syntax. |
|
335 |
||
44968 | 336 |
* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is |
337 |
still available as a legacy feature for some time. |
|
338 |
||
339 |
* Nitpick: |
|
340 |
- Added "need" and "total_consts" options. |
|
341 |
- Reintroduced "show_skolems" option by popular demand. |
|
342 |
- Renamed attribute: nitpick_def ~> nitpick_unfold. |
|
343 |
INCOMPATIBILITY. |
|
344 |
||
345 |
* Sledgehammer: |
|
346 |
- Use quasi-sound (and efficient) translations by default. |
|
347 |
- Added support for the following provers: E-ToFoF, LEO-II, |
|
348 |
Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. |
|
349 |
- Automatically preplay and minimize proofs before showing them if |
|
350 |
this can be done within reasonable time. |
|
351 |
- sledgehammer available_provers ~> sledgehammer supported_provers. |
|
352 |
INCOMPATIBILITY. |
|
353 |
- Added "preplay_timeout", "slicing", "type_enc", "sound", |
|
354 |
"max_mono_iters", and "max_new_mono_instances" options. |
|
355 |
- Removed "explicit_apply" and "full_types" options as well as "Full |
|
356 |
Types" Proof General menu item. INCOMPATIBILITY. |
|
357 |
||
358 |
* Metis: |
|
359 |
- Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. |
|
360 |
- Obsoleted "metisFT" -- use "metis (full_types)" instead. |
|
361 |
INCOMPATIBILITY. |
|
362 |
||
363 |
* Command 'try': |
|
364 |
- Renamed 'try_methods' and added "simp:", "intro:", "dest:", and |
|
365 |
"elim:" options. INCOMPATIBILITY. |
|
366 |
- Introduced 'try' that not only runs 'try_methods' but also |
|
367 |
'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. |
|
368 |
||
369 |
* Quickcheck: |
|
370 |
- Added "eval" option to evaluate terms for the found counterexample |
|
371 |
(currently only supported by the default (exhaustive) tester). |
|
372 |
- Added post-processing of terms to obtain readable counterexamples |
|
373 |
(currently only supported by the default (exhaustive) tester). |
|
374 |
- New counterexample generator quickcheck[narrowing] enables |
|
375 |
narrowing-based testing. Requires the Glasgow Haskell compiler |
|
376 |
with its installation location defined in the Isabelle settings |
|
377 |
environment as ISABELLE_GHC. |
|
378 |
- Removed quickcheck tester "SML" based on the SML code generator |
|
379 |
(formly in HOL/Library). |
|
380 |
||
381 |
* Function package: discontinued option "tailrec". INCOMPATIBILITY, |
|
382 |
use 'partial_function' instead. |
|
383 |
||
384 |
* Theory Library/Extended_Reals replaces now the positive extended |
|
385 |
reals found in probability theory. This file is extended by |
|
386 |
Multivariate_Analysis/Extended_Real_Limits. |
|
387 |
||
44974 | 388 |
* Theory Library/Old_Recdef: old 'recdef' package has been moved here, |
389 |
from where it must be imported explicitly if it is really required. |
|
390 |
INCOMPATIBILITY. |
|
44968 | 391 |
|
392 |
* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has |
|
393 |
been moved here. INCOMPATIBILITY. |
|
394 |
||
395 |
* Theory Library/Saturated provides type of numbers with saturated |
|
396 |
arithmetic. |
|
397 |
||
398 |
* Theory Library/Product_Lattice defines a pointwise ordering for the |
|
399 |
product type 'a * 'b, and provides instance proofs for various order |
|
400 |
and lattice type classes. |
|
401 |
||
402 |
* Theory Library/Countable now provides the "countable_datatype" proof |
|
403 |
method for proving "countable" class instances for datatypes. |
|
404 |
||
405 |
* Theory Library/Cset_Monad allows do notation for computable sets |
|
406 |
(cset) via the generic monad ad-hoc overloading facility. |
|
407 |
||
408 |
* Library: Theories of common data structures are split into theories |
|
409 |
for implementation, an invariant-ensuring type, and connection to an |
|
410 |
abstract type. INCOMPATIBILITY. |
|
411 |
||
412 |
- RBT is split into RBT and RBT_Mapping. |
|
413 |
- AssocList is split and renamed into AList and AList_Mapping. |
|
414 |
- DList is split into DList_Impl, DList, and DList_Cset. |
|
415 |
- Cset is split into Cset and List_Cset. |
|
416 |
||
417 |
* Theory Library/Nat_Infinity has been renamed to |
|
418 |
Library/Extended_Nat, with name changes of the following types and |
|
419 |
constants: |
|
420 |
||
421 |
type inat ~> type enat |
|
422 |
Fin ~> enat |
|
423 |
Infty ~> infinity (overloaded) |
|
424 |
iSuc ~> eSuc |
|
425 |
the_Fin ~> the_enat |
|
426 |
||
427 |
Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has |
|
428 |
been renamed accordingly. INCOMPATIBILITY. |
|
429 |
||
430 |
* Session Multivariate_Analysis: The euclidean_space type class now |
|
431 |
fixes a constant "Basis :: 'a set" consisting of the standard |
|
432 |
orthonormal basis for the type. Users now have the option of |
|
433 |
quantifying over this set instead of using the "basis" function, e.g. |
|
434 |
"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)". |
|
435 |
||
436 |
* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed |
|
437 |
to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants |
|
438 |
"Cart_nth" and "Cart_lambda" have been respectively renamed to |
|
439 |
"vec_nth" and "vec_lambda"; theorems mentioning those names have |
|
440 |
changed to match. Definition theorems for overloaded constants now use |
|
441 |
the standard "foo_vec_def" naming scheme. A few other theorems have |
|
442 |
been renamed as follows (INCOMPATIBILITY): |
|
443 |
||
444 |
Cart_eq ~> vec_eq_iff |
|
445 |
dist_nth_le_cart ~> dist_vec_nth_le |
|
446 |
tendsto_vector ~> vec_tendstoI |
|
447 |
Cauchy_vector ~> vec_CauchyI |
|
448 |
||
449 |
* Session Multivariate_Analysis: Several duplicate theorems have been |
|
450 |
removed, and other theorems have been renamed or replaced with more |
|
451 |
general versions. INCOMPATIBILITY. |
|
452 |
||
453 |
finite_choice ~> finite_set_choice |
|
454 |
eventually_conjI ~> eventually_conj |
|
455 |
eventually_and ~> eventually_conj_iff |
|
456 |
eventually_false ~> eventually_False |
|
457 |
setsum_norm ~> norm_setsum |
|
458 |
Lim_sequentially ~> LIMSEQ_def |
|
459 |
Lim_ident_at ~> LIM_ident |
|
460 |
Lim_const ~> tendsto_const |
|
461 |
Lim_cmul ~> tendsto_scaleR [OF tendsto_const] |
|
462 |
Lim_neg ~> tendsto_minus |
|
463 |
Lim_add ~> tendsto_add |
|
464 |
Lim_sub ~> tendsto_diff |
|
465 |
Lim_mul ~> tendsto_scaleR |
|
466 |
Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] |
|
467 |
Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] |
|
468 |
Lim_linear ~> bounded_linear.tendsto |
|
469 |
Lim_component ~> tendsto_euclidean_component |
|
470 |
Lim_component_cart ~> tendsto_vec_nth |
|
471 |
Lim_inner ~> tendsto_inner [OF tendsto_const] |
|
472 |
dot_lsum ~> inner_setsum_left |
|
473 |
dot_rsum ~> inner_setsum_right |
|
474 |
continuous_cmul ~> continuous_scaleR [OF continuous_const] |
|
475 |
continuous_neg ~> continuous_minus |
|
476 |
continuous_sub ~> continuous_diff |
|
477 |
continuous_vmul ~> continuous_scaleR [OF _ continuous_const] |
|
478 |
continuous_mul ~> continuous_scaleR |
|
479 |
continuous_inv ~> continuous_inverse |
|
480 |
continuous_at_within_inv ~> continuous_at_within_inverse |
|
481 |
continuous_at_inv ~> continuous_at_inverse |
|
482 |
continuous_at_norm ~> continuous_norm [OF continuous_at_id] |
|
483 |
continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] |
|
484 |
continuous_at_component ~> continuous_component [OF continuous_at_id] |
|
485 |
continuous_on_neg ~> continuous_on_minus |
|
486 |
continuous_on_sub ~> continuous_on_diff |
|
487 |
continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] |
|
488 |
continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] |
|
489 |
continuous_on_mul ~> continuous_on_scaleR |
|
490 |
continuous_on_mul_real ~> continuous_on_mult |
|
491 |
continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
|
492 |
continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
|
493 |
continuous_on_inverse ~> continuous_on_inv |
|
494 |
uniformly_continuous_on_neg ~> uniformly_continuous_on_minus |
|
495 |
uniformly_continuous_on_sub ~> uniformly_continuous_on_diff |
|
496 |
subset_interior ~> interior_mono |
|
497 |
subset_closure ~> closure_mono |
|
498 |
closure_univ ~> closure_UNIV |
|
499 |
real_arch_lt ~> reals_Archimedean2 |
|
500 |
real_arch ~> reals_Archimedean3 |
|
501 |
real_abs_norm ~> abs_norm_cancel |
|
502 |
real_abs_sub_norm ~> norm_triangle_ineq3 |
|
503 |
norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 |
|
504 |
||
505 |
* Session HOL-Probability: |
|
506 |
- Caratheodory's extension lemma is now proved for ring_of_sets. |
|
507 |
- Infinite products of probability measures are now available. |
|
508 |
- Sigma closure is independent, if the generator is independent |
|
509 |
- Use extended reals instead of positive extended |
|
510 |
reals. INCOMPATIBILITY. |
|
511 |
||
45049 | 512 |
* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY. |
513 |
||
514 |
expand_fun_below ~> fun_below_iff |
|
515 |
below_fun_ext ~> fun_belowI |
|
516 |
expand_cfun_eq ~> cfun_eq_iff |
|
517 |
ext_cfun ~> cfun_eqI |
|
518 |
expand_cfun_below ~> cfun_below_iff |
|
519 |
below_cfun_ext ~> cfun_belowI |
|
520 |
monofun_fun_fun ~> fun_belowD |
|
521 |
monofun_fun_arg ~> monofunE |
|
522 |
monofun_lub_fun ~> adm_monofun [THEN admD] |
|
523 |
cont_lub_fun ~> adm_cont [THEN admD] |
|
524 |
cont2cont_Rep_CFun ~> cont2cont_APP |
|
525 |
cont_Rep_CFun_app ~> cont_APP_app |
|
526 |
cont_Rep_CFun_app_app ~> cont_APP_app_app |
|
527 |
cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE] |
|
528 |
cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE] |
|
529 |
contlub_cfun ~> lub_APP [symmetric] |
|
530 |
contlub_LAM ~> lub_LAM [symmetric] |
|
531 |
thelubI ~> lub_eqI |
|
532 |
UU_I ~> bottomI |
|
533 |
lift_distinct1 ~> lift.distinct(1) |
|
534 |
lift_distinct2 ~> lift.distinct(2) |
|
535 |
Def_not_UU ~> lift.distinct(2) |
|
536 |
Def_inject ~> lift.inject |
|
537 |
below_UU_iff ~> below_bottom_iff |
|
538 |
eq_UU_iff ~> eq_bottom_iff |
|
539 |
||
44903 | 540 |
|
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
41667
diff
changeset
|
541 |
*** Document preparation *** |
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
41667
diff
changeset
|
542 |
|
44800 | 543 |
* Antiquotation @{rail} layouts railroad syntax diagrams, see also |
544 |
isar-ref manual, both for description and actual application of the |
|
545 |
same. |
|
546 |
||
547 |
* Antiquotation @{value} evaluates the given term and presents its |
|
548 |
result. |
|
549 |
||
550 |
* Antiquotations: term style "isub" provides ad-hoc conversion of |
|
551 |
variables x1, y23 into subscripted form x\<^isub>1, |
|
552 |
y\<^isub>2\<^isub>3. |
|
41651 | 553 |
|
42484 | 554 |
* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> |
555 |
(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). |
|
556 |
||
44967 | 557 |
* Localized \isabellestyle switch can be used within blocks or groups |
558 |
like this: |
|
559 |
||
560 |
\isabellestyle{it} %preferred default |
|
561 |
{\isabellestylett @{text "typewriter stuff"}} |
|
562 |
||
563 |
* Discontinued special treatment of hard tabulators. Implicit |
|
564 |
tab-width is now defined as 1. Potential INCOMPATIBILITY for visual |
|
565 |
layouts. |
|
44800 | 566 |
|
41651 | 567 |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
568 |
*** ML *** |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
569 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
570 |
* The inner syntax of sort/type/term/prop supports inlined YXML |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
571 |
representations within quoted string tokens. By encoding logical |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
572 |
entities via Term_XML (in ML or Scala) concrete syntax can be |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
573 |
bypassed, which is particularly useful for producing bits of text |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
574 |
under external program control. |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
575 |
|
43565 | 576 |
* Antiquotations for ML and document preparation are managed as theory |
577 |
data, which requires explicit setup. |
|
578 |
||
42897 | 579 |
* Isabelle_Process.is_active allows tools to check if the official |
580 |
process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop |
|
581 |
(better known as Proof General). |
|
582 |
||
42360 | 583 |
* Structure Proof_Context follows standard naming scheme. Old |
584 |
ProofContext is still available for some time as legacy alias. |
|
585 |
||
42015
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
586 |
* Structure Timing provides various operations for timing; supersedes |
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
587 |
former start_timing/end_timing etc. |
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
588 |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
589 |
* Path.print is the official way to show file-system paths to users |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
590 |
(including quotes etc.). |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
591 |
|
42056
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
592 |
* Inner syntax: identifiers in parse trees of generic categories |
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
593 |
"logic", "aprop", "idt" etc. carry position information (disguised as |
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
594 |
type constraints). Occasional INCOMPATIBILITY with non-compliant |
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
595 |
translations that choke on unexpected type constraints. Positions can |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
596 |
be stripped in ML translations via Syntax.strip_positions / |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
597 |
Syntax.strip_positions_ast, or via the syntax constant |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
598 |
"_strip_positions" within parse trees. As last resort, positions can |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
599 |
be disabled via the configuration option Syntax.positions, which is |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
600 |
called "syntax_positions" in Isar attribute syntax. |
42056
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
601 |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
602 |
* Discontinued special status of various ML structures that contribute |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
603 |
to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
604 |
pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
605 |
refer directly to Ast.Constant, Lexicon.is_identifier, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
606 |
Syntax_Trans.mk_binder_tr etc. |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42180
diff
changeset
|
607 |
|
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
608 |
* Typed print translation: discontinued show_sorts argument, which is |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
609 |
already available via context of "advanced" translation. |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
610 |
|
42370 | 611 |
* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic |
612 |
goal states; body tactic needs to address all subgoals uniformly. |
|
613 |
||
42403
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
614 |
* Slightly more special eq_list/eq_set, with shortcut involving |
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
615 |
pointer equality (assumes that eq relation is reflexive). |
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
616 |
|
42793 | 617 |
* Classical tactics use proper Proof.context instead of historic types |
618 |
claset/clasimpset. Old-style declarations like addIs, addEs, addDs |
|
619 |
operate directly on Proof.context. Raw type claset retains its use as |
|
620 |
snapshot of the classical context, which can be recovered via |
|
621 |
(put_claset HOL_cs) etc. Type clasimpset has been discontinued. |
|
622 |
INCOMPATIBILITY, classical tactics and derived proof methods require |
|
623 |
proper Proof.context. |
|
624 |
||
44803 | 625 |
|
626 |
*** System *** |
|
627 |
||
44968 | 628 |
* Discontinued support for Poly/ML 5.2, which was the last version |
629 |
without proper multithreading and TimeLimit implementation. |
|
630 |
||
631 |
* Discontinued old lib/scripts/polyml-platform, which has been |
|
632 |
obsolete since Isabelle2009-2. |
|
633 |
||
44967 | 634 |
* Various optional external tools are referenced more robustly and |
635 |
uniformly by explicit Isabelle settings as follows: |
|
636 |
||
637 |
ISABELLE_CSDP (formerly CSDP_EXE) |
|
638 |
ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) |
|
639 |
ISABELLE_OCAML (formerly EXEC_OCAML) |
|
640 |
ISABELLE_SWIPL (formerly EXEC_SWIPL) |
|
641 |
ISABELLE_YAP (formerly EXEC_YAP) |
|
642 |
||
643 |
Note that automated detection from the file-system or search path has |
|
644 |
been discontinued. INCOMPATIBILITY. |
|
645 |
||
43752 | 646 |
* Scala layer provides JVM method invocation service for static |
44800 | 647 |
methods of type (String)String, see Invoke_Scala.method in ML. For |
648 |
example: |
|
43752 | 649 |
|
650 |
Invoke_Scala.method "java.lang.System.getProperty" "java.home" |
|
651 |
||
44967 | 652 |
Together with YXML.string_of_body/parse_body and XML.Encode/Decode |
653 |
this allows to pass structured values between ML and Scala. |
|
44800 | 654 |
|
44803 | 655 |
* The IsabelleText fonts includes some further glyphs to support the |
656 |
Prover IDE. Potential INCOMPATIBILITY: users who happen to have |
|
657 |
installed a local copy (which is normally *not* required) need to |
|
658 |
delete or update it from ~~/lib/fonts/. |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
659 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
660 |
|
45089 | 661 |
|
41512 | 662 |
New in Isabelle2011 (January 2011) |
663 |
---------------------------------- |
|
37383 | 664 |
|
37536
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
665 |
*** General *** |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
666 |
|
41573 | 667 |
* Experimental Prover IDE based on Isabelle/Scala and jEdit (see |
41612 | 668 |
src/Tools/jEdit). This also serves as IDE for Isabelle/ML, with |
669 |
useful tooltips and hyperlinks produced from its static analysis. The |
|
670 |
bundled component provides an executable Isabelle tool that can be run |
|
671 |
like this: |
|
672 |
||
673 |
Isabelle2011/bin/isabelle jedit |
|
41573 | 674 |
|
40948 | 675 |
* Significantly improved Isabelle/Isar implementation manual. |
676 |
||
41594 | 677 |
* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER |
41595 | 678 |
(and thus refers to something like $HOME/.isabelle/Isabelle2011), |
41594 | 679 |
while the default heap location within that directory lacks that extra |
680 |
suffix. This isolates multiple Isabelle installations from each |
|
681 |
other, avoiding problems with old settings in new versions. |
|
682 |
INCOMPATIBILITY, need to copy/upgrade old user settings manually. |
|
683 |
||
40947 | 684 |
* Source files are always encoded as UTF-8, instead of old-fashioned |
685 |
ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require |
|
40948 | 686 |
the following package declarations: |
40947 | 687 |
|
688 |
\usepackage[utf8]{inputenc} |
|
689 |
\usepackage{textcomp} |
|
690 |
||
41440 | 691 |
* Explicit treatment of UTF-8 sequences as Isabelle symbols, such that |
37536
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
692 |
a Unicode character is treated as a single symbol, not a sequence of |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
693 |
non-ASCII bytes as before. Since Isabelle/ML string literals may |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
694 |
contain symbols without further backslash escapes, Unicode can now be |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
695 |
used here as well. Recall that Symbol.explode in ML provides a |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
696 |
consistent view on symbols, while raw explode (or String.explode) |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
697 |
merely give a byte-oriented representation. |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
698 |
|
41594 | 699 |
* Theory loader: source files are primarily located via the master |
700 |
directory of each theory node (where the .thy file itself resides). |
|
701 |
The global load path is still partially available as legacy feature. |
|
702 |
Minor INCOMPATIBILITY due to subtle change in file lookup: use |
|
703 |
explicit paths, relatively to the theory. |
|
38135
2b9bfa0b44f1
theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents:
38110
diff
changeset
|
704 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
705 |
* Special treatment of ML file names has been discontinued. |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
706 |
Historically, optional extensions .ML or .sml were added on demand -- |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
707 |
at the cost of clarity of file dependencies. Recall that Isabelle/ML |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
708 |
files exclusively use the .ML extension. Minor INCOMPATIBILTY. |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
709 |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
710 |
* Various options that affect pretty printing etc. are now properly |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
711 |
handled within the context via configuration options, instead of |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
712 |
unsynchronized references or print modes. There are both ML Config.T |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
713 |
entities and Isar declaration attributes to access these. |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
714 |
|
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
715 |
ML (Config.T) Isar (attribute) |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
716 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
39126
diff
changeset
|
717 |
eta_contract eta_contract |
39137
ccb53edd59f0
turned show_brackets into proper configuration option;
wenzelm
parents:
39134
diff
changeset
|
718 |
show_brackets show_brackets |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39128
diff
changeset
|
719 |
show_sorts show_sorts |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39128
diff
changeset
|
720 |
show_types show_types |
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
721 |
show_question_marks show_question_marks |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
722 |
show_consts show_consts |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
723 |
show_abbrevs show_abbrevs |
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
724 |
|
41379 | 725 |
Syntax.ast_trace syntax_ast_trace |
726 |
Syntax.ast_stat syntax_ast_stat |
|
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
727 |
Syntax.ambiguity_level syntax_ambiguity_level |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
728 |
|
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
729 |
Goal_Display.goals_limit goals_limit |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
730 |
Goal_Display.show_main_goal show_main_goal |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
731 |
|
41379 | 732 |
Method.rule_trace rule_trace |
733 |
||
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
734 |
Thy_Output.display thy_output_display |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
735 |
Thy_Output.quotes thy_output_quotes |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
736 |
Thy_Output.indent thy_output_indent |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
737 |
Thy_Output.source thy_output_source |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
738 |
Thy_Output.break thy_output_break |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
739 |
|
41440 | 740 |
Note that corresponding "..._default" references in ML may only be |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
741 |
changed globally at the ROOT session setup, but *not* within a theory. |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
742 |
The option "show_abbrevs" supersedes the former print mode |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
743 |
"no_abbrevs" with inverted meaning. |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
744 |
|
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
745 |
* More systematic naming of some configuration options. |
41294 | 746 |
INCOMPATIBILITY. |
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
747 |
|
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
748 |
trace_simp ~> simp_trace |
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
749 |
debug_simp ~> simp_debug |
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
750 |
|
40291 | 751 |
* Support for real valued configuration options, using simplistic |
752 |
floating-point notation that coincides with the inner syntax for |
|
753 |
float_token. |
|
754 |
||
41594 | 755 |
* Support for real valued preferences (with approximative PGIP type): |
756 |
front-ends need to accept "pgint" values in float notation. |
|
757 |
INCOMPATIBILITY. |
|
41573 | 758 |
|
759 |
* The IsabelleText font now includes Cyrillic, Hebrew, Arabic from |
|
760 |
DejaVu Sans. |
|
761 |
||
41594 | 762 |
* Discontinued support for Poly/ML 5.0 and 5.1 versions. |
763 |
||
40948 | 764 |
|
765 |
*** Pure *** |
|
766 |
||
41249
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
767 |
* Command 'type_synonym' (with single argument) replaces somewhat |
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
768 |
outdated 'types', which is still available as legacy feature for some |
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
769 |
time. |
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
770 |
|
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
771 |
* Command 'nonterminal' (with 'and' separated list of arguments) |
26f12f98f50a
Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
wenzelm
parents:
41229
diff
changeset
|
772 |
replaces somewhat outdated 'nonterminals'. INCOMPATIBILITY. |
41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
41228
diff
changeset
|
773 |
|
40965
54b6c9e1c157
command 'notepad' replaces former 'example_proof';
wenzelm
parents:
40959
diff
changeset
|
774 |
* Command 'notepad' replaces former 'example_proof' for |
41020 | 775 |
experimentation in Isar without any result. INCOMPATIBILITY. |
40965
54b6c9e1c157
command 'notepad' replaces former 'example_proof';
wenzelm
parents:
40959
diff
changeset
|
776 |
|
41435 | 777 |
* Locale interpretation commands 'interpret' and 'sublocale' accept |
778 |
lists of equations to map definitions in a locale to appropriate |
|
779 |
entities in the context of the interpretation. The 'interpretation' |
|
780 |
command already provided this functionality. |
|
781 |
||
41594 | 782 |
* Diagnostic command 'print_dependencies' prints the locale instances |
783 |
that would be activated if the specified expression was interpreted in |
|
784 |
the current context. Variant "print_dependencies!" assumes a context |
|
785 |
without interpretations. |
|
38110 | 786 |
|
787 |
* Diagnostic command 'print_interps' prints interpretations in proofs |
|
788 |
in addition to interpretations in theories. |
|
789 |
||
38708
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38656
diff
changeset
|
790 |
* Discontinued obsolete 'global' and 'local' commands to manipulate |
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38656
diff
changeset
|
791 |
the theory name space. Rare INCOMPATIBILITY. The ML functions |
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38656
diff
changeset
|
792 |
Sign.root_path and Sign.local_path may be applied directly where this |
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38656
diff
changeset
|
793 |
feature is still required for historical reasons. |
8915e3ce8655
discontinued obsolete 'global' and 'local' commands;
wenzelm
parents:
38656
diff
changeset
|
794 |
|
40948 | 795 |
* Discontinued obsolete 'constdefs' command. INCOMPATIBILITY, use |
39215 | 796 |
'definition' instead. |
797 |
||
41574 | 798 |
* The "prems" fact, which refers to the accidental collection of |
799 |
foundational premises in the context, is now explicitly marked as |
|
41594 | 800 |
legacy feature and will be discontinued soon. Consider using "assms" |
801 |
of the head statement or reference facts by explicit names. |
|
41574 | 802 |
|
40801 | 803 |
* Document antiquotations @{class} and @{type} print classes and type |
804 |
constructors. |
|
805 |
||
806 |
* Document antiquotation @{file} checks file/directory entries within |
|
807 |
the local file system. |
|
39305
d4fa19eb0822
'class' and 'type' are now antiquoations by default
haftmann
parents:
39277
diff
changeset
|
808 |
|
38110 | 809 |
|
37387
3581483cca6c
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents:
37383
diff
changeset
|
810 |
*** HOL *** |
3581483cca6c
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents:
37383
diff
changeset
|
811 |
|
41594 | 812 |
* Coercive subtyping: functions can be declared as coercions and type |
813 |
inference will add them as necessary upon input of a term. Theory |
|
814 |
Complex_Main declares real :: nat => real and real :: int => real as |
|
815 |
coercions. A coercion function f is declared like this: |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
816 |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
817 |
declare [[coercion f]] |
40866 | 818 |
|
41571 | 819 |
To lift coercions through type constructors (e.g. from nat => real to |
40866 | 820 |
nat list => real list), map functions can be declared, e.g. |
821 |
||
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
822 |
declare [[coercion_map map]] |
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
823 |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
824 |
Currently coercion inference is activated only in theories including |
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
825 |
real numbers, i.e. descendants of Complex_Main. This is controlled by |
41020 | 826 |
the configuration option "coercion_enabled", e.g. it can be enabled in |
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
827 |
other theories like this: |
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
828 |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40927
diff
changeset
|
829 |
declare [[coercion_enabled]] |
40866 | 830 |
|
41571 | 831 |
* Command 'partial_function' provides basic support for recursive |
832 |
function definitions over complete partial orders. Concrete instances |
|
40183 | 833 |
are provided for i) the option type, ii) tail recursion on arbitrary |
41571 | 834 |
types, and iii) the heap monad of Imperative_HOL. See |
835 |
src/HOL/ex/Fundefs.thy and src/HOL/Imperative_HOL/ex/Linked_Lists.thy |
|
836 |
for examples. |
|
40183 | 837 |
|
41571 | 838 |
* Function package: f.psimps rules are no longer implicitly declared |
839 |
as [simp]. INCOMPATIBILITY. |
|
41398 | 840 |
|
841 |
* Datatype package: theorems generated for executable equality (class |
|
41571 | 842 |
"eq") carry proper names and are treated as default code equations. |
843 |
||
41594 | 844 |
* Inductive package: now offers command 'inductive_simps' to |
845 |
automatically derive instantiated and simplified equations for |
|
846 |
inductive predicates, similar to 'inductive_cases'. |
|
847 |
||
41571 | 848 |
* Command 'enriched_type' allows to register properties of the |
849 |
functorial structure of types. |
|
39771 | 850 |
|
39644 | 851 |
* Improved infrastructure for term evaluation using code generator |
852 |
techniques, in particular static evaluation conversions. |
|
853 |
||
41594 | 854 |
* Code generator: Scala (2.8 or higher) has been added to the target |
855 |
languages. |
|
856 |
||
41398 | 857 |
* Code generator: globbing constant expressions "*" and "Theory.*" |
858 |
have been replaced by the more idiomatic "_" and "Theory._". |
|
859 |
INCOMPATIBILITY. |
|
860 |
||
861 |
* Code generator: export_code without explicit file declaration prints |
|
862 |
to standard output. INCOMPATIBILITY. |
|
863 |
||
864 |
* Code generator: do not print function definitions for case |
|
865 |
combinators any longer. |
|
866 |
||
41594 | 867 |
* Code generator: simplification with rules determined with |
41571 | 868 |
src/Tools/Code/code_simp.ML and method "code_simp". |
869 |
||
41594 | 870 |
* Code generator for records: more idiomatic representation of record |
40948 | 871 |
types. Warning: records are not covered by ancient SML code |
872 |
generation any longer. INCOMPATIBILITY. In cases of need, a suitable |
|
873 |
rep_datatype declaration helps to succeed then: |
|
38537 | 874 |
|
875 |
record 'a foo = ... |
|
876 |
... |
|
877 |
rep_datatype foo_ext ... |
|
38535 | 878 |
|
41594 | 879 |
* Records: logical foundation type for records does not carry a |
880 |
'_type' suffix any longer (obsolete due to authentic syntax). |
|
881 |
INCOMPATIBILITY. |
|
882 |
||
41398 | 883 |
* Quickcheck now by default uses exhaustive testing instead of random |
41571 | 884 |
testing. Random testing can be invoked by "quickcheck [random]", |
885 |
exhaustive testing by "quickcheck [exhaustive]". |
|
41398 | 886 |
|
887 |
* Quickcheck instantiates polymorphic types with small finite |
|
888 |
datatypes by default. This enables a simple execution mechanism to |
|
889 |
handle quantifiers and function equality over the finite datatypes. |
|
890 |
||
41571 | 891 |
* Quickcheck random generator has been renamed from "code" to |
892 |
"random". INCOMPATIBILITY. |
|
41398 | 893 |
|
894 |
* Quickcheck now has a configurable time limit which is set to 30 |
|
895 |
seconds by default. This can be changed by adding [timeout = n] to the |
|
896 |
quickcheck command. The time limit for Auto Quickcheck is still set |
|
897 |
independently. |
|
38461 | 898 |
|
899 |
* Quickcheck in locales considers interpretations of that locale for |
|
900 |
counter example search. |
|
901 |
||
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
902 |
* Sledgehammer: |
41571 | 903 |
- Added "smt" and "remote_smt" provers based on the "smt" proof |
904 |
method. See the Sledgehammer manual for details ("isabelle doc |
|
905 |
sledgehammer"). |
|
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
906 |
- Renamed commands: |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
907 |
sledgehammer atp_info ~> sledgehammer running_provers |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
908 |
sledgehammer atp_kill ~> sledgehammer kill_provers |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
909 |
sledgehammer available_atps ~> sledgehammer available_provers |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
910 |
INCOMPATIBILITY. |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
911 |
- Renamed options: |
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
912 |
sledgehammer [atps = ...] ~> sledgehammer [provers = ...] |
40062 | 913 |
sledgehammer [atp = ...] ~> sledgehammer [prover = ...] |
40341
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
914 |
sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77] |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
915 |
(and "ms" and "min" are no longer supported) |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
916 |
INCOMPATIBILITY. |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
917 |
|
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
918 |
* Nitpick: |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
919 |
- Renamed options: |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
920 |
nitpick [timeout = 77 s] ~> nitpick [timeout = 77] |
03156257040f
standardize on seconds for Nitpick and Sledgehammer timeouts
blanchet
parents:
40318
diff
changeset
|
921 |
nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777] |
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39993
diff
changeset
|
922 |
INCOMPATIBILITY. |
40725 | 923 |
- Added support for partial quotient types. |
924 |
- Added local versions of the "Nitpick.register_xxx" functions. |
|
925 |
- Added "whack" option. |
|
926 |
- Allow registration of quotient types as codatatypes. |
|
927 |
- Improved "merge_type_vars" option to merge more types. |
|
928 |
- Removed unsound "fast_descrs" option. |
|
929 |
- Added custom symmetry breaking for datatypes, making it possible to reach |
|
930 |
higher cardinalities. |
|
931 |
- Prevent the expansion of too large definitions. |
|
39957
2f2d90cc31a2
document latest changes to Meson/Metis/Sledgehammer
blanchet
parents:
39910
diff
changeset
|
932 |
|
41571 | 933 |
* Proof methods "metis" and "meson" now have configuration options |
934 |
"meson_trace", "metis_trace", and "metis_verbose" that can be enabled |
|
935 |
to diagnose these tools. E.g. |
|
936 |
||
937 |
using [[metis_trace = true]] |
|
938 |
||
41398 | 939 |
* Auto Solve: Renamed "Auto Solve Direct". The tool is now available |
940 |
manually as command 'solve_direct'. |
|
941 |
||
41601 | 942 |
* The default SMT solver Z3 must be enabled explicitly (due to |
943 |
licensing issues) by setting the environment variable |
|
41603 | 944 |
Z3_NON_COMMERCIAL in etc/settings of the component, for example. For |
945 |
commercial applications, the SMT solver CVC3 is provided as fall-back; |
|
946 |
changing the SMT solver is done via the configuration option |
|
947 |
"smt_solver". |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
948 |
|
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
949 |
* Remote SMT solvers need to be referred to by the "remote_" prefix, |
41571 | 950 |
i.e. "remote_cvc3" and "remote_z3". |
951 |
||
952 |
* Added basic SMT support for datatypes, records, and typedefs using |
|
953 |
the oracle mode (no proofs). Direct support of pairs has been dropped |
|
954 |
in exchange (pass theorems fst_conv snd_conv pair_collapse to the SMT |
|
955 |
support for a similar behavior). Minor INCOMPATIBILITY. |
|
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
956 |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
957 |
* Changed SMT configuration options: |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
958 |
- Renamed: |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
959 |
z3_proofs ~> smt_oracle (with inverted meaning) |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
960 |
z3_trace_assms ~> smt_trace_used_facts |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
961 |
INCOMPATIBILITY. |
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
962 |
- Added: |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40388
diff
changeset
|
963 |
smt_verbose |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
964 |
smt_random_seed |
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40388
diff
changeset
|
965 |
smt_datatypes |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
966 |
smt_infer_triggers |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
967 |
smt_monomorph_limit |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
968 |
cvc3_options |
41432
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
969 |
remote_cvc3_options |
3214c39777ab
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
boehmes
parents:
41430
diff
changeset
|
970 |
remote_z3_options |
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40128
diff
changeset
|
971 |
yices_options |
39957
2f2d90cc31a2
document latest changes to Meson/Metis/Sledgehammer
blanchet
parents:
39910
diff
changeset
|
972 |
|
40948 | 973 |
* Boogie output files (.b2i files) need to be declared in the theory |
974 |
header. |
|
40580
0592d3a39c08
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes
parents:
40424
diff
changeset
|
975 |
|
41594 | 976 |
* Simplification procedure "list_to_set_comprehension" rewrites list |
977 |
comprehensions applied to List.set to set comprehensions. Occasional |
|
978 |
INCOMPATIBILITY, may be deactivated like this: |
|
979 |
||
980 |
declare [[simproc del: list_to_set_comprehension]] |
|
981 |
||
41573 | 982 |
* Removed old version of primrec package. INCOMPATIBILITY. |
41398 | 983 |
|
984 |
* Removed simplifier congruence rule of "prod_case", as has for long |
|
985 |
been the case with "split". INCOMPATIBILITY. |
|
986 |
||
987 |
* String.literal is a type, but not a datatype. INCOMPATIBILITY. |
|
988 |
||
40388
cb9fd7dd641c
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss
parents:
40387
diff
changeset
|
989 |
* Removed [split_format ... and ... and ...] version of |
cb9fd7dd641c
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss
parents:
40387
diff
changeset
|
990 |
[split_format]. Potential INCOMPATIBILITY. |
cb9fd7dd641c
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
krauss
parents:
40387
diff
changeset
|
991 |
|
41571 | 992 |
* Predicate "sorted" now defined inductively, with nice induction |
993 |
rules. INCOMPATIBILITY: former sorted.simps now named sorted_simps. |
|
41398 | 994 |
|
995 |
* Constant "contents" renamed to "the_elem", to free the generic name |
|
996 |
contents for other uses. INCOMPATIBILITY. |
|
997 |
||
998 |
* Renamed class eq and constant eq (for code generation) to class |
|
999 |
equal and constant equal, plus renaming of related facts and various |
|
1000 |
tuning. INCOMPATIBILITY. |
|
1001 |
||
1002 |
* Dropped type classes mult_mono and mult_mono1. INCOMPATIBILITY. |
|
1003 |
||
41571 | 1004 |
* Removed output syntax "'a ~=> 'b" for "'a => 'b option". |
1005 |
INCOMPATIBILITY. |
|
41398 | 1006 |
|
1007 |
* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to |
|
1008 |
avoid confusion with finite sets. INCOMPATIBILITY. |
|
1009 |
||
1010 |
* Abandoned locales equiv, congruent and congruent2 for equivalence |
|
1011 |
relations. INCOMPATIBILITY: use equivI rather than equiv_intro (same |
|
1012 |
for congruent(2)). |
|
1013 |
||
1014 |
* Some previously unqualified names have been qualified: |
|
1015 |
||
1016 |
types |
|
1017 |
bool ~> HOL.bool |
|
1018 |
nat ~> Nat.nat |
|
1019 |
||
1020 |
constants |
|
1021 |
Trueprop ~> HOL.Trueprop |
|
1022 |
True ~> HOL.True |
|
1023 |
False ~> HOL.False |
|
1024 |
op & ~> HOL.conj |
|
1025 |
op | ~> HOL.disj |
|
1026 |
op --> ~> HOL.implies |
|
1027 |
op = ~> HOL.eq |
|
1028 |
Not ~> HOL.Not |
|
1029 |
The ~> HOL.The |
|
1030 |
All ~> HOL.All |
|
1031 |
Ex ~> HOL.Ex |
|
1032 |
Ex1 ~> HOL.Ex1 |
|
1033 |
Let ~> HOL.Let |
|
1034 |
If ~> HOL.If |
|
1035 |
Ball ~> Set.Ball |
|
1036 |
Bex ~> Set.Bex |
|
1037 |
Suc ~> Nat.Suc |
|
1038 |
Pair ~> Product_Type.Pair |
|
1039 |
fst ~> Product_Type.fst |
|
1040 |
snd ~> Product_Type.snd |
|
1041 |
curry ~> Product_Type.curry |
|
1042 |
op : ~> Set.member |
|
1043 |
Collect ~> Set.Collect |
|
1044 |
||
1045 |
INCOMPATIBILITY. |
|
1046 |
||
1047 |
* More canonical naming convention for some fundamental definitions: |
|
1048 |
||
1049 |
bot_bool_eq ~> bot_bool_def |
|
1050 |
top_bool_eq ~> top_bool_def |
|
1051 |
inf_bool_eq ~> inf_bool_def |
|
1052 |
sup_bool_eq ~> sup_bool_def |
|
1053 |
bot_fun_eq ~> bot_fun_def |
|
1054 |
top_fun_eq ~> top_fun_def |
|
1055 |
inf_fun_eq ~> inf_fun_def |
|
1056 |
sup_fun_eq ~> sup_fun_def |
|
1057 |
||
1058 |
INCOMPATIBILITY. |
|
1059 |
||
1060 |
* More stylized fact names: |
|
1061 |
||
1062 |
expand_fun_eq ~> fun_eq_iff |
|
1063 |
expand_set_eq ~> set_eq_iff |
|
1064 |
set_ext ~> set_eqI |
|
1065 |
nat_number ~> eval_nat_numeral |
|
1066 |
||
1067 |
INCOMPATIBILITY. |
|
1068 |
||
41571 | 1069 |
* Refactoring of code-generation specific operations in theory List: |
41398 | 1070 |
|
1071 |
constants |
|
1072 |
null ~> List.null |
|
1073 |
||
1074 |
facts |
|
1075 |
mem_iff ~> member_def |
|
1076 |
null_empty ~> null_def |
|
1077 |
||
1078 |
INCOMPATIBILITY. Note that these were not supposed to be used |
|
1079 |
regularly unless for striking reasons; their main purpose was code |
|
1080 |
generation. |
|
1081 |
||
1082 |
Various operations from the Haskell prelude are used for generating |
|
1083 |
Haskell code. |
|
1084 |
||
41571 | 1085 |
* Term "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". Term |
1086 |
"surj f" is now an abbreviation of "range f = UNIV". The theorems |
|
1087 |
bij_def and surj_def are unchanged. INCOMPATIBILITY. |
|
41398 | 1088 |
|
1089 |
* Abolished some non-alphabetic type names: "prod" and "sum" replace |
|
1090 |
"*" and "+" respectively. INCOMPATIBILITY. |
|
1091 |
||
1092 |
* Name "Plus" of disjoint sum operator "<+>" is now hidden. Write |
|
41571 | 1093 |
"Sum_Type.Plus" instead. |
41398 | 1094 |
|
1095 |
* Constant "split" has been merged with constant "prod_case"; names of |
|
1096 |
ML functions, facts etc. involving split have been retained so far, |
|
1097 |
though. INCOMPATIBILITY. |
|
1098 |
||
1099 |
* Dropped old infix syntax "_ mem _" for List.member; use "_ : set _" |
|
1100 |
instead. INCOMPATIBILITY. |
|
1101 |
||
41571 | 1102 |
* Removed lemma "Option.is_none_none" which duplicates "is_none_def". |
41398 | 1103 |
INCOMPATIBILITY. |
1104 |
||
41594 | 1105 |
* Former theory Library/Enum is now part of the HOL-Main image. |
1106 |
INCOMPATIBILITY: all constants of the Enum theory now have to be |
|
1107 |
referred to by its qualified name. |
|
1108 |
||
1109 |
enum ~> Enum.enum |
|
1110 |
nlists ~> Enum.nlists |
|
1111 |
product ~> Enum.product |
|
1112 |
||
1113 |
* Theory Library/Monad_Syntax provides do-syntax for monad types. |
|
1114 |
Syntax in Library/State_Monad has been changed to avoid ambiguities. |
|
1115 |
INCOMPATIBILITY. |
|
1116 |
||
1117 |
* Theory Library/SetsAndFunctions has been split into |
|
1118 |
Library/Function_Algebras and Library/Set_Algebras; canonical names |
|
1119 |
for instance definitions for functions; various improvements. |
|
1120 |
INCOMPATIBILITY. |
|
1121 |
||
1122 |
* Theory Library/Multiset provides stable quicksort implementation of |
|
1123 |
sort_key. |
|
1124 |
||
1125 |
* Theory Library/Multiset: renamed empty_idemp ~> empty_neutral. |
|
1126 |
INCOMPATIBILITY. |
|
1127 |
||
1128 |
* Session Multivariate_Analysis: introduced a type class for euclidean |
|
1129 |
space. Most theorems are now stated in terms of euclidean spaces |
|
1130 |
instead of finite cartesian products. |
|
1131 |
||
1132 |
types |
|
1133 |
real ^ 'n ~> 'a::real_vector |
|
1134 |
~> 'a::euclidean_space |
|
1135 |
~> 'a::ordered_euclidean_space |
|
1136 |
(depends on your needs) |
|
1137 |
||
1138 |
constants |
|
1139 |
_ $ _ ~> _ $$ _ |
|
1140 |
\<chi> x. _ ~> \<chi>\<chi> x. _ |
|
1141 |
CARD('n) ~> DIM('a) |
|
1142 |
||
1143 |
Also note that the indices are now natural numbers and not from some |
|
1144 |
finite type. Finite cartesian products of euclidean spaces, products |
|
1145 |
of euclidean spaces the real and complex numbers are instantiated to |
|
1146 |
be euclidean_spaces. INCOMPATIBILITY. |
|
1147 |
||
1148 |
* Session Probability: introduced pextreal as positive extended real |
|
1149 |
numbers. Use pextreal as value for measures. Introduce the |
|
1150 |
Radon-Nikodym derivative, product spaces and Fubini's theorem for |
|
1151 |
arbitrary sigma finite measures. Introduces Lebesgue measure based on |
|
1152 |
the integral in Multivariate Analysis. INCOMPATIBILITY. |
|
1153 |
||
1154 |
* Session Imperative_HOL: revamped, corrected dozens of inadequacies. |
|
1155 |
INCOMPATIBILITY. |
|
1156 |
||
1157 |
* Session SPARK (with image HOL-SPARK) provides commands to load and |
|
1158 |
prove verification conditions generated by the SPARK Ada program |
|
1159 |
verifier. See also src/HOL/SPARK and src/HOL/SPARK/Examples. |
|
41567 | 1160 |
|
40621 | 1161 |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1162 |
*** HOL-Algebra *** |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1163 |
|
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1164 |
* Theorems for additive ring operations (locale abelian_monoid and |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1165 |
descendants) are generated by interpretation from their multiplicative |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41433
diff
changeset
|
1166 |
counterparts. Names (in particular theorem names) have the mandatory |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41433
diff
changeset
|
1167 |
qualifier 'add'. Previous theorem names are redeclared for |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41433
diff
changeset
|
1168 |
compatibility. |
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41433
diff
changeset
|
1169 |
|
41571 | 1170 |
* Structure "int_ring" is now an abbreviation (previously a |
41434
710cdb9e0d17
Documentation for 'interpret' and 'sublocale' with mixins.
ballarin
parents:
41433
diff
changeset
|
1171 |
definition). This fits more natural with advanced interpretations. |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1172 |
|
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
41432
diff
changeset
|
1173 |
|
40621 | 1174 |
*** HOLCF *** |
1175 |
||
1176 |
* The domain package now runs in definitional mode by default: The |
|
41571 | 1177 |
former command 'new_domain' is now called 'domain'. To use the domain |
40621 | 1178 |
package in its original axiomatic mode, use 'domain (unsafe)'. |
1179 |
INCOMPATIBILITY. |
|
1180 |
||
41571 | 1181 |
* The new class "domain" is now the default sort. Class "predomain" |
1182 |
is an unpointed version of "domain". Theories can be updated by |
|
1183 |
replacing sort annotations as shown below. INCOMPATIBILITY. |
|
40621 | 1184 |
|
1185 |
'a::type ~> 'a::countable |
|
1186 |
'a::cpo ~> 'a::predomain |
|
1187 |
'a::pcpo ~> 'a::domain |
|
1188 |
||
41571 | 1189 |
* The old type class "rep" has been superseded by class "domain". |
40621 | 1190 |
Accordingly, users of the definitional package must remove any |
41571 | 1191 |
"default_sort rep" declarations. INCOMPATIBILITY. |
40621 | 1192 |
|
41401 | 1193 |
* The domain package (definitional mode) now supports unpointed |
1194 |
predomain argument types, as long as they are marked 'lazy'. (Strict |
|
41571 | 1195 |
arguments must be in class "domain".) For example, the following |
41401 | 1196 |
domain definition now works: |
1197 |
||
1198 |
domain natlist = nil | cons (lazy "nat discr") (lazy "natlist") |
|
1199 |
||
1200 |
* Theory HOLCF/Library/HOL_Cpo provides cpo and predomain class |
|
41571 | 1201 |
instances for types from main HOL: bool, nat, int, char, 'a + 'b, |
1202 |
'a option, and 'a list. Additionally, it configures fixrec and the |
|
1203 |
domain package to work with these types. For example: |
|
41401 | 1204 |
|
1205 |
fixrec isInl :: "('a + 'b) u -> tr" |
|
1206 |
where "isInl$(up$(Inl x)) = TT" | "isInl$(up$(Inr y)) = FF" |
|
1207 |
||
1208 |
domain V = VFun (lazy "V -> V") | VCon (lazy "nat") (lazy "V list") |
|
1209 |
||
41571 | 1210 |
* The "(permissive)" option of fixrec has been replaced with a |
1211 |
per-equation "(unchecked)" option. See |
|
1212 |
src/HOL/HOLCF/Tutorial/Fixrec_ex.thy for examples. INCOMPATIBILITY. |
|
1213 |
||
1214 |
* The "bifinite" class no longer fixes a constant "approx"; the class |
|
1215 |
now just asserts that such a function exists. INCOMPATIBILITY. |
|
1216 |
||
1217 |
* Former type "alg_defl" has been renamed to "defl". HOLCF no longer |
|
41287
029a6fc1bfb8
type 'defl' takes a type parameter again (cf. b525988432e9)
huffman
parents:
41286
diff
changeset
|
1218 |
defines an embedding of type 'a defl into udom by default; instances |
41571 | 1219 |
of "bifinite" and "domain" classes are available in |
1220 |
src/HOL/HOLCF/Library/Defl_Bifinite.thy. |
|
1221 |
||
1222 |
* The syntax "REP('a)" has been replaced with "DEFL('a)". |
|
1223 |
||
1224 |
* The predicate "directed" has been removed. INCOMPATIBILITY. |
|
1225 |
||
1226 |
* The type class "finite_po" has been removed. INCOMPATIBILITY. |
|
1227 |
||
1228 |
* The function "cprod_map" has been renamed to "prod_map". |
|
41401 | 1229 |
INCOMPATIBILITY. |
1230 |
||
1231 |
* The monadic bind operator on each powerdomain has new binder syntax |
|
41571 | 1232 |
similar to sets, e.g. "\<Union>\<sharp>x\<in>xs. t" represents |
1233 |
"upper_bind\<cdot>xs\<cdot>(\<Lambda> x. t)". |
|
41401 | 1234 |
|
1235 |
* The infix syntax for binary union on each powerdomain has changed |
|
41571 | 1236 |
from e.g. "+\<sharp>" to "\<union>\<sharp>", for consistency with set |
1237 |
syntax. INCOMPATIBILITY. |
|
1238 |
||
1239 |
* The constant "UU" has been renamed to "bottom". The syntax "UU" is |
|
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41414
diff
changeset
|
1240 |
still supported as an input translation. |
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41414
diff
changeset
|
1241 |
|
40621 | 1242 |
* Renamed some theorems (the original names are also still available). |
41571 | 1243 |
|
40621 | 1244 |
expand_fun_below ~> fun_below_iff |
1245 |
below_fun_ext ~> fun_belowI |
|
1246 |
expand_cfun_eq ~> cfun_eq_iff |
|
1247 |
ext_cfun ~> cfun_eqI |
|
1248 |
expand_cfun_below ~> cfun_below_iff |
|
1249 |
below_cfun_ext ~> cfun_belowI |
|
1250 |
cont2cont_Rep_CFun ~> cont2cont_APP |
|
1251 |
||
1252 |
* The Abs and Rep functions for various types have changed names. |
|
40948 | 1253 |
Related theorem names have also changed to match. INCOMPATIBILITY. |
41571 | 1254 |
|
40621 | 1255 |
Rep_CFun ~> Rep_cfun |
1256 |
Abs_CFun ~> Abs_cfun |
|
1257 |
Rep_Sprod ~> Rep_sprod |
|
1258 |
Abs_Sprod ~> Abs_sprod |
|
1259 |
Rep_Ssum ~> Rep_ssum |
|
1260 |
Abs_Ssum ~> Abs_ssum |
|
1261 |
||
1262 |
* Lemmas with names of the form *_defined_iff or *_strict_iff have |
|
41571 | 1263 |
been renamed to *_bottom_iff. INCOMPATIBILITY. |
40621 | 1264 |
|
1265 |
* Various changes to bisimulation/coinduction with domain package: |
|
41571 | 1266 |
|
1267 |
- Definitions of "bisim" constants no longer mention definedness. |
|
1268 |
- With mutual recursion, "bisim" predicate is now curried. |
|
40621 | 1269 |
- With mutual recursion, each type gets a separate coind theorem. |
1270 |
- Variable names in bisim_def and coinduct rules have changed. |
|
41571 | 1271 |
|
40621 | 1272 |
INCOMPATIBILITY. |
1273 |
||
41571 | 1274 |
* Case combinators generated by the domain package for type "foo" are |
1275 |
now named "foo_case" instead of "foo_when". INCOMPATIBILITY. |
|
40621 | 1276 |
|
40771 | 1277 |
* Several theorems have been renamed to more accurately reflect the |
41571 | 1278 |
names of constants and types involved. INCOMPATIBILITY. |
1279 |
||
40771 | 1280 |
thelub_const ~> lub_const |
1281 |
lub_const ~> is_lub_const |
|
1282 |
thelubI ~> lub_eqI |
|
1283 |
is_lub_lub ~> is_lubD2 |
|
1284 |
lubI ~> is_lub_lub |
|
1285 |
unique_lub ~> is_lub_unique |
|
1286 |
is_ub_lub ~> is_lub_rangeD1 |
|
1287 |
lub_bin_chain ~> is_lub_bin_chain |
|
41030
ff7d177128ef
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents:
40965
diff
changeset
|
1288 |
lub_fun ~> is_lub_fun |
ff7d177128ef
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
huffman
parents:
40965
diff
changeset
|
1289 |
thelub_fun ~> lub_fun |
41031 | 1290 |
thelub_cfun ~> lub_cfun |
40771 | 1291 |
thelub_Pair ~> lub_Pair |
1292 |
lub_cprod ~> is_lub_prod |
|
1293 |
thelub_cprod ~> lub_prod |
|
1294 |
minimal_cprod ~> minimal_prod |
|
1295 |
inst_cprod_pcpo ~> inst_prod_pcpo |
|
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset
|
1296 |
UU_I ~> bottomI |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset
|
1297 |
compact_UU ~> compact_bottom |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset
|
1298 |
deflation_UU ~> deflation_bottom |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41429
diff
changeset
|
1299 |
finite_deflation_UU ~> finite_deflation_bottom |
40771 | 1300 |
|
41571 | 1301 |
* Many legacy theorem names have been discontinued. INCOMPATIBILITY. |
1302 |
||
40621 | 1303 |
sq_ord_less_eq_trans ~> below_eq_trans |
1304 |
sq_ord_eq_less_trans ~> eq_below_trans |
|
1305 |
refl_less ~> below_refl |
|
1306 |
trans_less ~> below_trans |
|
1307 |
antisym_less ~> below_antisym |
|
1308 |
antisym_less_inverse ~> po_eq_conv [THEN iffD1] |
|
1309 |
box_less ~> box_below |
|
1310 |
rev_trans_less ~> rev_below_trans |
|
1311 |
not_less2not_eq ~> not_below2not_eq |
|
1312 |
less_UU_iff ~> below_UU_iff |
|
1313 |
flat_less_iff ~> flat_below_iff |
|
1314 |
adm_less ~> adm_below |
|
1315 |
adm_not_less ~> adm_not_below |
|
1316 |
adm_compact_not_less ~> adm_compact_not_below |
|
1317 |
less_fun_def ~> below_fun_def |
|
1318 |
expand_fun_less ~> fun_below_iff |
|
1319 |
less_fun_ext ~> fun_belowI |
|
1320 |
less_discr_def ~> below_discr_def |
|
1321 |
discr_less_eq ~> discr_below_eq |
|
1322 |
less_unit_def ~> below_unit_def |
|
1323 |
less_cprod_def ~> below_prod_def |
|
1324 |
prod_lessI ~> prod_belowI |
|
1325 |
Pair_less_iff ~> Pair_below_iff |
|
1326 |
fst_less_iff ~> fst_below_iff |
|
1327 |
snd_less_iff ~> snd_below_iff |
|
1328 |
expand_cfun_less ~> cfun_below_iff |
|
1329 |
less_cfun_ext ~> cfun_belowI |
|
1330 |
injection_less ~> injection_below |
|
1331 |
less_up_def ~> below_up_def |
|
1332 |
not_Iup_less ~> not_Iup_below |
|
1333 |
Iup_less ~> Iup_below |
|
1334 |
up_less ~> up_below |
|
1335 |
Def_inject_less_eq ~> Def_below_Def |
|
1336 |
Def_less_is_eq ~> Def_below_iff |
|
1337 |
spair_less_iff ~> spair_below_iff |
|
1338 |
less_sprod ~> below_sprod |
|
1339 |
spair_less ~> spair_below |
|
1340 |
sfst_less_iff ~> sfst_below_iff |
|
1341 |
ssnd_less_iff ~> ssnd_below_iff |
|
1342 |
fix_least_less ~> fix_least_below |
|
1343 |
dist_less_one ~> dist_below_one |
|
1344 |
less_ONE ~> below_ONE |
|
1345 |
ONE_less_iff ~> ONE_below_iff |
|
1346 |
less_sinlD ~> below_sinlD |
|
1347 |
less_sinrD ~> below_sinrD |
|
1348 |
||
1349 |
||
40948 | 1350 |
*** FOL and ZF *** |
38522 | 1351 |
|
41310 | 1352 |
* All constant names are now qualified internally and use proper |
1353 |
identifiers, e.g. "IFOL.eq" instead of "op =". INCOMPATIBILITY. |
|
1354 |
||
38522 | 1355 |
|
37868
59eed00bfd8e
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents:
37820
diff
changeset
|
1356 |
*** ML *** |
59eed00bfd8e
ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state;
wenzelm
parents:
37820
diff
changeset
|
1357 |
|
41594 | 1358 |
* Antiquotation @{assert} inlines a function bool -> unit that raises |
1359 |
Fail if the argument is false. Due to inlining the source position of |
|
1360 |
failed assertions is included in the error output. |
|
1361 |
||
1362 |
* Discontinued antiquotation @{theory_ref}, which is obsolete since ML |
|
1363 |
text is in practice always evaluated with a stable theory checkpoint. |
|
1364 |
Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead. |
|
1365 |
||
1366 |
* Antiquotation @{theory A} refers to theory A from the ancestry of |
|
1367 |
the current context, not any accidental theory loader state as before. |
|
1368 |
Potential INCOMPATIBILITY, subtle change in semantics. |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41079
diff
changeset
|
1369 |
|
40956 | 1370 |
* Syntax.pretty_priority (default 0) configures the required priority |
1371 |
of pretty-printed output and thus affects insertion of parentheses. |
|
1372 |
||
40959 | 1373 |
* Syntax.default_root (default "any") configures the inner syntax |
1374 |
category (nonterminal symbol) for parsing of terms. |
|
1375 |
||
40722
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40712
diff
changeset
|
1376 |
* Former exception Library.UnequalLengths now coincides with |
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40712
diff
changeset
|
1377 |
ListPair.UnequalLengths. |
441260986b63
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents:
40712
diff
changeset
|
1378 |
|
41594 | 1379 |
* Renamed structure MetaSimplifier to Raw_Simplifier. Note that the |
1380 |
main functionality is provided by structure Simplifier. |
|
1381 |
||
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40624
diff
changeset
|
1382 |
* Renamed raw "explode" function to "raw_explode" to emphasize its |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40624
diff
changeset
|
1383 |
meaning. Note that internally to Isabelle, Symbol.explode is used in |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40624
diff
changeset
|
1384 |
almost all situations. |
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40624
diff
changeset
|
1385 |
|
40318
035b2afbeb2e
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm
parents:
40295
diff
changeset
|
1386 |
* Discontinued obsolete function sys_error and exception SYS_ERROR. |
035b2afbeb2e
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm
parents:
40295
diff
changeset
|
1387 |
See implementation manual for further details on exceptions in |
035b2afbeb2e
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm
parents:
40295
diff
changeset
|
1388 |
Isabelle/ML. |
035b2afbeb2e
discontinued obsolete function sys_error and exception SYS_ERROR;
wenzelm
parents:
40295
diff
changeset
|
1389 |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset
|
1390 |
* Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset
|
1391 |
meaning. |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset
|
1392 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39513
diff
changeset
|
1393 |
* Renamed structure PureThy to Pure_Thy and moved most of its |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39513
diff
changeset
|
1394 |
operations to structure Global_Theory, to emphasize that this is |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39513
diff
changeset
|
1395 |
rarely-used global-only stuff. |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39513
diff
changeset
|
1396 |
|
39513
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39308
diff
changeset
|
1397 |
* Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln |
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39308
diff
changeset
|
1398 |
instead (or tracing for high-volume output). |
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39308
diff
changeset
|
1399 |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1400 |
* Configuration option show_question_marks only affects regular pretty |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1401 |
printing of types and terms, not raw Term.string_of_vname. |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1402 |
|
39164
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39154
diff
changeset
|
1403 |
* ML_Context.thm and ML_Context.thms are no longer pervasive. Rare |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39154
diff
changeset
|
1404 |
INCOMPATIBILITY, superseded by static antiquotations @{thm} and |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39154
diff
changeset
|
1405 |
@{thms} for most purposes. |
e7e12555e763
ML_Context.thm and ML_Context.thms no longer pervasive;
wenzelm
parents:
39154
diff
changeset
|
1406 |
|
41594 | 1407 |
* ML structure Unsynchronized is never opened, not even in Isar |
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1408 |
interaction mode as before. Old Unsynchronized.set etc. have been |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1409 |
discontinued -- use plain := instead. This should be *rare* anyway, |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1410 |
since modern tools always work via official context data, notably |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1411 |
configuration options. |
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1412 |
|
39239
|