author | wenzelm |
Thu, 10 Mar 2016 22:21:01 +0100 | |
changeset 62591 | 98122e719d19 |
parent 62588 | cd266473b81b |
child 62597 | b3f2b8c906a6 |
permissions | -rw-r--r-- |
57491 | 1 |
Isabelle NEWS -- history of user-relevant changes |
2 |
================================================= |
|
2553 | 3 |
|
62114
a7cf464933f7
generate HTML version of NEWS, with proper symbol rendering;
wenzelm
parents:
62111
diff
changeset
|
4 |
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) |
60006 | 5 |
|
60331 | 6 |
|
62216 | 7 |
New in this Isabelle version |
8 |
---------------------------- |
|
9 |
||
62440 | 10 |
*** General *** |
11 |
||
12 |
* New symbol \<circle>, e.g. for temporal operator. |
|
13 |
||
62453 | 14 |
* Old 'header' command is no longer supported (legacy since |
15 |
Isabelle2015). |
|
16 |
||
62440 | 17 |
|
62312
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
18 |
*** Isar *** |
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
19 |
|
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
20 |
* Command '\<proof>' is an alias for 'sorry', with different |
5e5a881ebc12
command '\<proof>' is an alias for 'sorry', with different typesetting;
wenzelm
parents:
62284
diff
changeset
|
21 |
typesetting. E.g. to produce proof holes in examples and documentation. |
62216 | 22 |
|
23 |
||
62327 | 24 |
*** HOL *** |
25 |
||
62522 | 26 |
* New abbreviations for negated existence (but not bounded existence): |
27 |
||
28 |
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x) |
|
29 |
\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x) |
|
30 |
||
62521 | 31 |
* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@" |
32 |
has been removed for output. It is retained for input only, until it is |
|
33 |
eliminated altogether. |
|
34 |
||
62327 | 35 |
* (Co)datatype package: |
62332 | 36 |
- the predicator :: ('a => bool) => 'a F => bool is now a first-class |
37 |
citizen in bounded natural functors |
|
62327 | 38 |
- "primrec" now allows nested calls through the predicator in addition |
39 |
to the map function. |
|
62332 | 40 |
- "bnf" automatically discharges reflexive proof obligations |
41 |
"bnf" outputs a slightly modified proof obligation expressing rel in |
|
42 |
terms of map and set |
|
43 |
(not giving a specification for rel makes this one reflexive) |
|
44 |
"bnf" outputs a new proof obligation expressing pred in terms of set |
|
45 |
(not giving a specification for pred makes this one reflexive) |
|
46 |
INCOMPATIBILITY: manual "bnf" declarations may need adjustment |
|
62335 | 47 |
- Renamed lemmas: |
48 |
rel_prod_apply ~> rel_prod_inject |
|
49 |
pred_prod_apply ~> pred_prod_inject |
|
50 |
INCOMPATIBILITY. |
|
62536
656e9653c645
made 'size' plugin compatible with locales again (and added regression test)
blanchet
parents:
62525
diff
changeset
|
51 |
- The "size" plugin has been made compatible again with locales. |
62327 | 52 |
|
62407 | 53 |
* Renamed split_if -> if_split and split_if_asm -> if_split_asm to |
54 |
resemble the f.split naming convention, INCOMPATIBILITY. |
|
62396 | 55 |
|
62430
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
56 |
* Multiset membership is now expressed using set_mset rather than count. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
57 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
58 |
- Expressions "count M a > 0" and similar simplify to membership |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
59 |
by default. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
60 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
61 |
- Converting between "count M a = 0" and non-membership happens using |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
62 |
equations count_eq_zero_iff and not_in_iff. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
63 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
64 |
- Rules count_inI and in_countE obtain facts of the form |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
65 |
"count M a = n" from membership. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
66 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
67 |
- Rules count_in_diffI and in_diff_countE obtain facts of the form |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
68 |
"count M a = n + count N a" from membership on difference sets. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
69 |
|
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
70 |
INCOMPATIBILITY. |
9527ff088c15
more succint formulation of membership for multisets, similar to lists;
haftmann
parents:
62415
diff
changeset
|
71 |
|
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
72 |
* Compound constants INFIMUM and SUPREMUM are mere abbreviations now. |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
73 |
INCOMPATIBILITY. |
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62335
diff
changeset
|
74 |
|
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62407
diff
changeset
|
75 |
* More complex analysis including Cauchy's inequality, Liouville theorem, |
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62407
diff
changeset
|
76 |
open mapping theorem, maximum modulus principle, Schwarz Lemma. |
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
62407
diff
changeset
|
77 |
|
62358 | 78 |
* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional |
79 |
comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)". |
|
80 |
||
62345 | 81 |
* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY. |
82 |
||
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
83 |
* The type class ordered_comm_monoid_add is now called |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
84 |
ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
85 |
introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add. |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
86 |
INCOMPATIBILITY. |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
87 |
|
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
88 |
* Introduced the type classes canonically_ordered_comm_monoid_add and dioid. |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
89 |
|
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
90 |
* Added topological_monoid |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62358
diff
changeset
|
91 |
|
62352
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
92 |
* Library/Polynomial.thy contains also derivation of polynomials |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
93 |
but not gcd/lcm on polynomials over fields. This has been moved |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
94 |
to a separate theory Library/Polynomial_GCD_euclidean.thy, to |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
95 |
pave way for a possible future different type class instantiation |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
96 |
for polynomials over factorial rings. INCOMPATIBILITY. |
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62348
diff
changeset
|
97 |
|
62348 | 98 |
* Dropped various legacy fact bindings, whose replacements are often |
99 |
of a more general type also: |
|
100 |
lcm_left_commute_nat ~> lcm.left_commute |
|
101 |
lcm_left_commute_int ~> lcm.left_commute |
|
102 |
gcd_left_commute_nat ~> gcd.left_commute |
|
103 |
gcd_left_commute_int ~> gcd.left_commute |
|
104 |
gcd_greatest_iff_nat ~> gcd_greatest_iff |
|
105 |
gcd_greatest_iff_int ~> gcd_greatest_iff |
|
106 |
coprime_dvd_mult_nat ~> coprime_dvd_mult |
|
107 |
coprime_dvd_mult_int ~> coprime_dvd_mult |
|
108 |
zpower_numeral_even ~> power_numeral_even |
|
109 |
gcd_mult_cancel_nat ~> gcd_mult_cancel |
|
110 |
gcd_mult_cancel_int ~> gcd_mult_cancel |
|
111 |
div_gcd_coprime_nat ~> div_gcd_coprime |
|
112 |
div_gcd_coprime_int ~> div_gcd_coprime |
|
113 |
zpower_numeral_odd ~> power_numeral_odd |
|
114 |
zero_less_int_conv ~> of_nat_0_less_iff |
|
115 |
gcd_greatest_nat ~> gcd_greatest |
|
116 |
gcd_greatest_int ~> gcd_greatest |
|
117 |
coprime_mult_nat ~> coprime_mult |
|
118 |
coprime_mult_int ~> coprime_mult |
|
119 |
lcm_commute_nat ~> lcm.commute |
|
120 |
lcm_commute_int ~> lcm.commute |
|
121 |
int_less_0_conv ~> of_nat_less_0_iff |
|
122 |
gcd_commute_nat ~> gcd.commute |
|
123 |
gcd_commute_int ~> gcd.commute |
|
124 |
Gcd_insert_nat ~> Gcd_insert |
|
125 |
Gcd_insert_int ~> Gcd_insert |
|
126 |
of_int_int_eq ~> of_int_of_nat_eq |
|
127 |
lcm_least_nat ~> lcm_least |
|
128 |
lcm_least_int ~> lcm_least |
|
129 |
lcm_assoc_nat ~> lcm.assoc |
|
130 |
lcm_assoc_int ~> lcm.assoc |
|
131 |
int_le_0_conv ~> of_nat_le_0_iff |
|
132 |
int_eq_0_conv ~> of_nat_eq_0_iff |
|
133 |
Gcd_empty_nat ~> Gcd_empty |
|
134 |
Gcd_empty_int ~> Gcd_empty |
|
135 |
gcd_assoc_nat ~> gcd.assoc |
|
136 |
gcd_assoc_int ~> gcd.assoc |
|
137 |
zero_zle_int ~> of_nat_0_le_iff |
|
138 |
lcm_dvd2_nat ~> dvd_lcm2 |
|
139 |
lcm_dvd2_int ~> dvd_lcm2 |
|
140 |
lcm_dvd1_nat ~> dvd_lcm1 |
|
141 |
lcm_dvd1_int ~> dvd_lcm1 |
|
142 |
gcd_zero_nat ~> gcd_eq_0_iff |
|
143 |
gcd_zero_int ~> gcd_eq_0_iff |
|
144 |
gcd_dvd2_nat ~> gcd_dvd2 |
|
145 |
gcd_dvd2_int ~> gcd_dvd2 |
|
146 |
gcd_dvd1_nat ~> gcd_dvd1 |
|
147 |
gcd_dvd1_int ~> gcd_dvd1 |
|
148 |
int_numeral ~> of_nat_numeral |
|
149 |
lcm_ac_nat ~> ac_simps |
|
150 |
lcm_ac_int ~> ac_simps |
|
151 |
gcd_ac_nat ~> ac_simps |
|
152 |
gcd_ac_int ~> ac_simps |
|
153 |
abs_int_eq ~> abs_of_nat |
|
154 |
zless_int ~> of_nat_less_iff |
|
155 |
zdiff_int ~> of_nat_diff |
|
156 |
zadd_int ~> of_nat_add |
|
157 |
int_mult ~> of_nat_mult |
|
158 |
int_Suc ~> of_nat_Suc |
|
159 |
inj_int ~> inj_of_nat |
|
160 |
int_1 ~> of_nat_1 |
|
161 |
int_0 ~> of_nat_0 |
|
62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
162 |
Lcm_empty_nat ~> Lcm_empty |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
163 |
Lcm_empty_int ~> Lcm_empty |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
164 |
Lcm_insert_nat ~> Lcm_insert |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
165 |
Lcm_insert_int ~> Lcm_insert |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
166 |
comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
167 |
comp_fun_idem_gcd_int ~> comp_fun_idem_gcd |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
168 |
comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
169 |
comp_fun_idem_lcm_int ~> comp_fun_idem_lcm |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
170 |
Lcm_eq_0 ~> Lcm_eq_0_I |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
171 |
Lcm0_iff ~> Lcm_0_iff |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
172 |
Lcm_dvd_int ~> Lcm_least |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
173 |
divides_mult_nat ~> divides_mult |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
174 |
divides_mult_int ~> divides_mult |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
175 |
lcm_0_nat ~> lcm_0_right |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
176 |
lcm_0_int ~> lcm_0_right |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
177 |
lcm_0_left_nat ~> lcm_0_left |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
178 |
lcm_0_left_int ~> lcm_0_left |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
179 |
dvd_gcd_D1_nat ~> dvd_gcdD1 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
180 |
dvd_gcd_D1_int ~> dvd_gcdD1 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
181 |
dvd_gcd_D2_nat ~> dvd_gcdD2 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
182 |
dvd_gcd_D2_int ~> dvd_gcdD2 |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
183 |
coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff |
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
184 |
coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff |
62348 | 185 |
realpow_minus_mult ~> power_minus_mult |
186 |
realpow_Suc_le_self ~> power_Suc_le_self |
|
62353
7f927120b5a2
dropped various legacy fact bindings and tuned proofs
haftmann
parents:
62352
diff
changeset
|
187 |
dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest |
62347 | 188 |
INCOMPATIBILITY. |
189 |
||
62479 | 190 |
* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis. |
191 |
||
62327 | 192 |
|
62498 | 193 |
*** ML *** |
194 |
||
195 |
* Option ML_exception_debugger controls detailed exception trace via the |
|
196 |
Poly/ML debugger. Relevant ML modules need to be compiled beforehand |
|
197 |
with ML_file_debug, or with ML_file and option ML_debugger enabled. Note |
|
198 |
debugger information requires consirable time and space: main |
|
199 |
Isabelle/HOL with full debugger support may need ML_system_64. |
|
200 |
||
62514 | 201 |
* Local_Theory.restore has been renamed to Local_Theory.reset to |
202 |
emphasize its disruptive impact on the cumulative context, notably the |
|
203 |
scope of 'private' or 'qualified' names. Note that Local_Theory.reset is |
|
204 |
only appropriate when targets are managed, e.g. starting from a global |
|
205 |
theory and returning to it. Regular definitional packages should use |
|
206 |
balanced blocks of Local_Theory.open_target versus |
|
207 |
Local_Theory.close_target instead. Rare INCOMPATIBILITY. |
|
208 |
||
62519 | 209 |
* Structure TimeLimit (originally from the SML/NJ library) has been |
210 |
replaced by structure Timeout, with slightly different signature. |
|
211 |
INCOMPATIBILITY. |
|
212 |
||
62551 | 213 |
* Discontinued cd and pwd operations, which are not well-defined in a |
214 |
multi-threaded environment. Note that files are usually located |
|
215 |
relatively to the master directory of a theory (see also |
|
216 |
File.full_path). Potential INCOMPATIBILITY. |
|
217 |
||
62498 | 218 |
|
62354 | 219 |
*** System *** |
220 |
||
62591 | 221 |
* The Isabelle system environment always ensures that the main |
222 |
executables are found within the shell search $PATH: "isabelle" and |
|
223 |
"isabelle_scala_script". |
|
224 |
||
225 |
* The Isabelle ML process is now managed directly by Isabelle/Scala, and |
|
226 |
shell scripts merely provide optional command-line access. In |
|
227 |
particular: |
|
228 |
||
229 |
. Scala module ML_Process to connect to the raw ML process, |
|
230 |
with interaction via stdin/stdout/stderr or in batch mode; |
|
231 |
. command-line tool "isabelle console" as interactive wrapper; |
|
232 |
. command-line tool "isabelle process" as batch mode wrapper. |
|
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
233 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
234 |
* The executable "isabelle_process" has been discontinued. Tools and |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
235 |
prover front-ends should use ML_Process or Isabelle_Process in |
62591 | 236 |
Isabelle/Scala. INCOMPATIBILITY. |
62588
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
237 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
238 |
* New command-line tool "isabelle process" supports ML evaluation of |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
239 |
literal expressions (option -e) or files (option -f) in the context of a |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
240 |
given heap image. Errors lead to premature exit of the ML process with |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
241 |
return code 1. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
242 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
243 |
* Command-line tool "isabelle console" provides option -r to help to |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
244 |
bootstrapping Isabelle/Pure interactively. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
245 |
|
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
246 |
* Command-line tool "isabelle yxml" has been discontinued. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
247 |
INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
248 |
Isabelle/ML or Isabelle/Scala. |
cd266473b81b
isabelle_process is superseded by "isabelle process" tool;
wenzelm
parents:
62579
diff
changeset
|
249 |
|
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
250 |
* File.bash_string, File.bash_path etc. represent Isabelle/ML and |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
251 |
Isabelle/Scala strings authentically within GNU bash. This is useful to |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
252 |
produce robust shell scripts under program control, without worrying |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
253 |
about spaces or special characters. Note that user output works via |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
254 |
Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
255 |
less versatile) operations File.shell_quote, File.shell_path etc. have |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
256 |
been discontinued. |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62525
diff
changeset
|
257 |
|
62591 | 258 |
* SML/NJ and old versions of Poly/ML are no longer supported. |
259 |
||
62354 | 260 |
|
261 |
||
62031 | 262 |
New in Isabelle2016 (February 2016) |
62016 | 263 |
----------------------------------- |
60138 | 264 |
|
61337 | 265 |
*** General *** |
266 |
||
62168
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
267 |
* Eisbach is now based on Pure instead of HOL. Objects-logics may import |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
268 |
either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
269 |
~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
270 |
the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
271 |
examples that do require HOL. |
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62163
diff
changeset
|
272 |
|
62157 | 273 |
* Better resource usage on all platforms (Linux, Windows, Mac OS X) for |
274 |
both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage. |
|
275 |
||
62017 | 276 |
* Former "xsymbols" syntax with Isabelle symbols is used by default, |
277 |
without any special print mode. Important ASCII replacement syntax |
|
278 |
remains available under print mode "ASCII", but less important syntax |
|
279 |
has been removed (see below). |
|
280 |
||
62109 | 281 |
* Support for more arrow symbols, with rendering in LaTeX and Isabelle |
282 |
fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>. |
|
62017 | 283 |
|
62108
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
284 |
* Special notation \<struct> for the first implicit 'structure' in the |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
285 |
context has been discontinued. Rare INCOMPATIBILITY, use explicit |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
286 |
structure name instead, notably in indexed notation with block-subscript |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
287 |
(e.g. \<odot>\<^bsub>A\<^esub>). |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
288 |
|
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
289 |
* The glyph for \<diamond> in the IsabelleText font now corresponds better to its |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
290 |
counterpart \<box> as quantifier-like symbol. A small diamond is available as |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
291 |
\<diamondop>; the old symbol \<struct> loses this rendering and any special |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
292 |
meaning. |
0046bacc5f5b
\<struct> loses its rendering and is superseded by \<diamondop>;
wenzelm
parents:
62107
diff
changeset
|
293 |
|
62017 | 294 |
* Syntax for formal comments "-- text" now also supports the symbolic |
295 |
form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps |
|
296 |
to update old sources. |
|
297 |
||
61337 | 298 |
* Toplevel theorem statements have been simplified as follows: |
299 |
||
300 |
theorems ~> lemmas |
|
301 |
schematic_lemma ~> schematic_goal |
|
302 |
schematic_theorem ~> schematic_goal |
|
303 |
schematic_corollary ~> schematic_goal |
|
304 |
||
305 |
Command-line tool "isabelle update_theorems" updates theory sources |
|
306 |
accordingly. |
|
307 |
||
61338 | 308 |
* Toplevel theorem statement 'proposition' is another alias for |
309 |
'theorem'. |
|
310 |
||
62169 | 311 |
* The old 'defs' command has been removed (legacy since Isabelle2014). |
312 |
INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or |
|
313 |
deferred definitions require a surrounding 'overloading' block. |
|
314 |
||
61337 | 315 |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
316 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
317 |
|
60986 | 318 |
* IDE support for the source-level debugger of Poly/ML, to work with |
62253 | 319 |
Isabelle/ML and official Standard ML. Option "ML_debugger" and commands |
320 |
'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug', |
|
321 |
'SML_file_no_debug' control compilation of sources with or without |
|
322 |
debugging information. The Debugger panel allows to set breakpoints (via |
|
323 |
context menu), step through stopped threads, evaluate local ML |
|
324 |
expressions etc. At least one Debugger view needs to be active to have |
|
325 |
any effect on the running ML program. |
|
60984 | 326 |
|
61803 | 327 |
* The State panel manages explicit proof state output, with dynamic |
328 |
auto-update according to cursor movement. Alternatively, the jEdit |
|
329 |
action "isabelle.update-state" (shortcut S+ENTER) triggers manual |
|
330 |
update. |
|
61729 | 331 |
|
332 |
* The Output panel no longer shows proof state output by default, to |
|
333 |
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or |
|
334 |
enable option "editor_output_state". |
|
61215 | 335 |
|
61803 | 336 |
* The text overview column (status of errors, warnings etc.) is updated |
337 |
asynchronously, leading to much better editor reactivity. Moreover, the |
|
338 |
full document node content is taken into account. The width of the |
|
339 |
column is scaled according to the main text area font, for improved |
|
340 |
visibility. |
|
341 |
||
342 |
* The main text area no longer changes its color hue in outdated |
|
343 |
situations. The text overview column takes over the role to indicate |
|
344 |
unfinished edits in the PIDE pipeline. This avoids flashing text display |
|
345 |
due to ad-hoc updates by auxiliary GUI components, such as the State |
|
346 |
panel. |
|
347 |
||
62254
81cbea2babd9
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset
|
348 |
* Slightly improved scheduling for urgent print tasks (e.g. command |
81cbea2babd9
tuned NEWS: long-running tasks can still prevent urgent tasks from being started, due to start_execution pri = 0;
wenzelm
parents:
62253
diff
changeset
|
349 |
state output, interactive queries) wrt. long-running background tasks. |
62017 | 350 |
|
351 |
* Completion of symbols via prefix of \<name> or \<^name> or \name is |
|
352 |
always possible, independently of the language context. It is never |
|
353 |
implicit: a popup will show up unconditionally. |
|
354 |
||
355 |
* Additional abbreviations for syntactic completion may be specified in |
|
356 |
$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with |
|
357 |
support for simple templates using ASCII 007 (bell) as placeholder. |
|
358 |
||
62234
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset
|
359 |
* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for |
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset
|
360 |
completion like "+o", "*o", ".o" etc. -- due to conflicts with other |
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset
|
361 |
ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define |
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset
|
362 |
suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs. |
7cc9d7b822ae
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
wenzelm
parents:
62231
diff
changeset
|
363 |
|
61483 | 364 |
* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls |
365 |
emphasized text style; the effect is visible in document output, not in |
|
366 |
the editor. |
|
367 |
||
368 |
* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE, |
|
369 |
instead of former C+e LEFT. |
|
370 |
||
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
371 |
* The command-line tool "isabelle jedit" and the isabelle.Main |
62027 | 372 |
application wrapper treat the default $USER_HOME/Scratch.thy more |
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
373 |
uniformly, and allow the dummy file argument ":" to open an empty buffer |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
374 |
instead. |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61501
diff
changeset
|
375 |
|
62017 | 376 |
* New command-line tool "isabelle jedit_client" allows to connect to an |
377 |
already running Isabelle/jEdit process. This achieves the effect of |
|
378 |
single-instance applications seen on common GUI desktops. |
|
379 |
||
61529
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
380 |
* The default look-and-feel for Linux is the traditional "Metal", which |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
381 |
works better with GUI scaling for very high-resolution displays (e.g. |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
382 |
4K). Moreover, it is generally more robust than "Nimbus". |
82fc5a6231a2
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
wenzelm
parents:
61520
diff
changeset
|
383 |
|
62163 | 384 |
* Update to jedit-5.3.0, with improved GUI scaling and support of |
385 |
high-resolution displays (e.g. 4K). |
|
386 |
||
62034 | 387 |
* The main Isabelle executable is managed as single-instance Desktop |
388 |
application uniformly on all platforms: Linux, Windows, Mac OS X. |
|
389 |
||
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
60595
diff
changeset
|
390 |
|
61405 | 391 |
*** Document preparation *** |
392 |
||
62017 | 393 |
* Commands 'paragraph' and 'subparagraph' provide additional section |
394 |
headings. Thus there are 6 levels of standard headings, as in HTML. |
|
395 |
||
396 |
* Command 'text_raw' has been clarified: input text is processed as in |
|
397 |
'text' (with antiquotations and control symbols). The key difference is |
|
398 |
the lack of the surrounding isabelle markup environment in output. |
|
399 |
||
400 |
* Text is structured in paragraphs and nested lists, using notation that |
|
401 |
is similar to Markdown. The control symbols for list items are as |
|
402 |
follows: |
|
403 |
||
404 |
\<^item> itemize |
|
405 |
\<^enum> enumerate |
|
406 |
\<^descr> description |
|
407 |
||
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
408 |
* There is a new short form for antiquotations with a single argument |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
409 |
that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and |
61595 | 410 |
\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. |
411 |
\<^name> without following cartouche is equivalent to @{name}. The |
|
61501 | 412 |
standard Isabelle fonts provide glyphs to render important control |
413 |
symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
414 |
|
61595 | 415 |
* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with |
416 |
corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using |
|
417 |
standard LaTeX macros of the same names. |
|
418 |
||
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
419 |
* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
420 |
Consequently, \<open>...\<close> without any decoration prints literal quasi-formal |
61492 | 421 |
text. Command-line tool "isabelle update_cartouches -t" helps to update |
422 |
old sources, by approximative patching of the content of string and |
|
423 |
cartouche tokens seen in theory sources. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
424 |
|
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
425 |
* The @{text} antiquotation now ignores the antiquotation option |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
426 |
"source". The given text content is output unconditionally, without any |
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
427 |
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the |
61494 | 428 |
argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial |
429 |
or terminal spaces are ignored. |
|
61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61488
diff
changeset
|
430 |
|
62017 | 431 |
* Antiquotations @{emph} and @{bold} output LaTeX source recursively, |
432 |
adding appropriate text style markup. These may be used in the short |
|
433 |
form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>. |
|
434 |
||
435 |
* Document antiquotation @{footnote} outputs LaTeX source recursively, |
|
436 |
marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>. |
|
437 |
||
438 |
* Antiquotation @{verbatim [display]} supports option "indent". |
|
439 |
||
440 |
* Antiquotation @{theory_text} prints uninterpreted theory source text |
|
62231
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset
|
441 |
(Isar outer syntax with command keywords etc.). This may be used in the |
25f4a9cd8b68
tuned markup, e.g. relevant for Rendering.tooltip;
wenzelm
parents:
62209
diff
changeset
|
442 |
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent". |
62017 | 443 |
|
444 |
* Antiquotation @{doc ENTRY} provides a reference to the given |
|
445 |
documentation, with a hyperlink in the Prover IDE. |
|
446 |
||
447 |
* Antiquotations @{command}, @{method}, @{attribute} print checked |
|
448 |
entities of the Isar language. |
|
449 |
||
61471 | 450 |
* HTML presentation uses the standard IsabelleText font and Unicode |
451 |
rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former |
|
61488 | 452 |
print mode "HTML" loses its special meaning. |
61471 | 453 |
|
61405 | 454 |
|
60406 | 455 |
*** Isar *** |
456 |
||
62205 | 457 |
* Local goals ('have', 'show', 'hence', 'thus') allow structured rule |
458 |
statements like fixes/assumes/shows in theorem specifications, but the |
|
459 |
notation is postfix with keywords 'if' (or 'when') and 'for'. For |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
460 |
example: |
60414 | 461 |
|
462 |
have result: "C x y" |
|
463 |
if "A x" and "B y" |
|
464 |
for x :: 'a and y :: 'a |
|
465 |
<proof> |
|
466 |
||
60449 | 467 |
The local assumptions are bound to the name "that". The result is |
468 |
exported from context of the statement as usual. The above roughly |
|
60414 | 469 |
corresponds to a raw proof block like this: |
470 |
||
471 |
{ |
|
472 |
fix x :: 'a and y :: 'a |
|
60449 | 473 |
assume that: "A x" "B y" |
60414 | 474 |
have "C x y" <proof> |
475 |
} |
|
476 |
note result = this |
|
60406 | 477 |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
478 |
The keyword 'when' may be used instead of 'if', to indicate 'presume' |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
479 |
instead of 'assume' above. |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60554
diff
changeset
|
480 |
|
61733 | 481 |
* Assumptions ('assume', 'presume') allow structured rule statements |
482 |
using 'if' and 'for', similar to 'have' etc. above. For example: |
|
61658 | 483 |
|
484 |
assume result: "C x y" |
|
485 |
if "A x" and "B y" |
|
486 |
for x :: 'a and y :: 'a |
|
487 |
||
488 |
This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general |
|
489 |
result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y". |
|
490 |
||
491 |
Vacuous quantification in assumptions is omitted, i.e. a for-context |
|
492 |
only effects propositions according to actual use of variables. For |
|
493 |
example: |
|
494 |
||
495 |
assume "A x" and "B y" for x and y |
|
496 |
||
497 |
is equivalent to: |
|
498 |
||
499 |
assume "\<And>x. A x" and "\<And>y. B y" |
|
500 |
||
60595 | 501 |
* The meaning of 'show' with Pure rule statements has changed: premises |
502 |
are treated in the sense of 'assume', instead of 'presume'. This means, |
|
62205 | 503 |
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as |
504 |
follows: |
|
60595 | 505 |
|
506 |
show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
507 |
||
508 |
or: |
|
509 |
||
510 |
show "C x" if "A x" "B x" for x |
|
511 |
||
512 |
Rare INCOMPATIBILITY, the old behaviour may be recovered as follows: |
|
513 |
||
514 |
show "C x" when "A x" "B x" for x |
|
515 |
||
60459 | 516 |
* New command 'consider' states rules for generalized elimination and |
517 |
case splitting. This is like a toplevel statement "theorem obtains" used |
|
518 |
within a proof body; or like a multi-branch 'obtain' without activation |
|
519 |
of the local context elements yet. |
|
520 |
||
60455 | 521 |
* Proof method "cases" allows to specify the rule as first entry of |
522 |
chained facts. This is particularly useful with 'consider': |
|
523 |
||
524 |
consider (a) A | (b) B | (c) C <proof> |
|
525 |
then have something |
|
526 |
proof cases |
|
527 |
case a |
|
528 |
then show ?thesis <proof> |
|
529 |
next |
|
530 |
case b |
|
531 |
then show ?thesis <proof> |
|
532 |
next |
|
533 |
case c |
|
534 |
then show ?thesis <proof> |
|
535 |
qed |
|
536 |
||
60565 | 537 |
* Command 'case' allows fact name and attribute specification like this: |
538 |
||
539 |
case a: (c xs) |
|
540 |
case a [attributes]: (c xs) |
|
541 |
||
542 |
Facts that are introduced by invoking the case context are uniformly |
|
543 |
qualified by "a"; the same name is used for the cumulative fact. The old |
|
544 |
form "case (c xs) [attributes]" is no longer supported. Rare |
|
545 |
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, |
|
546 |
and always put attributes in front. |
|
547 |
||
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
548 |
* The standard proof method of commands 'proof' and '..' is now called |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
549 |
"standard" to make semantically clear what it is; the old name "default" |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
550 |
is still available as legacy for some time. Documentation now explains |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
551 |
'..' more accurately as "by standard" instead of "by rule". |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60617
diff
changeset
|
552 |
|
62017 | 553 |
* Nesting of Isar goal structure has been clarified: the context after |
554 |
the initial backwards refinement is retained for the whole proof, within |
|
555 |
all its context sections (as indicated via 'next'). This is e.g. |
|
556 |
relevant for 'using', 'including', 'supply': |
|
557 |
||
558 |
have "A \<and> A" if a: A for A |
|
559 |
supply [simp] = a |
|
560 |
proof |
|
561 |
show A by simp |
|
562 |
next |
|
563 |
show A by simp |
|
564 |
qed |
|
565 |
||
566 |
* Command 'obtain' binds term abbreviations (via 'is' patterns) in the |
|
567 |
proof body as well, abstracted over relevant parameters. |
|
568 |
||
569 |
* Improved type-inference for theorem statement 'obtains': separate |
|
570 |
parameter scope for of each clause. |
|
571 |
||
572 |
* Term abbreviations via 'is' patterns also work for schematic |
|
573 |
statements: result is abstracted over unknowns. |
|
574 |
||
60631 | 575 |
* Command 'subgoal' allows to impose some structure on backward |
576 |
refinements, to avoid proof scripts degenerating into long of 'apply' |
|
577 |
sequences. Further explanations and examples are given in the isar-ref |
|
578 |
manual. |
|
579 |
||
62017 | 580 |
* Command 'supply' supports fact definitions during goal refinement |
581 |
('apply' scripts). |
|
582 |
||
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
583 |
* Proof method "goal_cases" turns the current subgoals into cases within |
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
584 |
the context; the conclusion is bound to variable ?case in each case. For |
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
585 |
example: |
60617 | 586 |
|
587 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
60622 | 588 |
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" |
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
589 |
proof goal_cases |
60622 | 590 |
case (1 x) |
591 |
then show ?case using \<open>A x\<close> \<open>B x\<close> sorry |
|
592 |
next |
|
593 |
case (2 y z) |
|
594 |
then show ?case using \<open>U y\<close> \<open>V z\<close> sorry |
|
595 |
qed |
|
596 |
||
597 |
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" |
|
598 |
and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z" |
|
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61158
diff
changeset
|
599 |
proof goal_cases |
60617 | 600 |
case prems: 1 |
601 |
then show ?case using prems sorry |
|
602 |
next |
|
603 |
case prems: 2 |
|
604 |
then show ?case using prems sorry |
|
605 |
qed |
|
60578 | 606 |
|
60581 | 607 |
* The undocumented feature of implicit cases goal1, goal2, goal3, etc. |
60617 | 608 |
is marked as legacy, and will be removed eventually. The proof method |
609 |
"goals" achieves a similar effect within regular Isar; often it can be |
|
610 |
done more adequately by other means (e.g. 'consider'). |
|
60581 | 611 |
|
62017 | 612 |
* The vacuous fact "TERM x" may be established "by fact" or as `TERM x` |
613 |
as well, not just "by this" or "." as before. |
|
60551 | 614 |
|
60554 | 615 |
* Method "sleep" succeeds after a real-time delay (in seconds). This is |
616 |
occasionally useful for demonstration and testing purposes. |
|
617 |
||
60406 | 618 |
|
60331 | 619 |
*** Pure *** |
620 |
||
61606
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
621 |
* Qualifiers in locale expressions default to mandatory ('!') regardless |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
622 |
of the command. Previously, for 'locale' and 'sublocale' the default was |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
623 |
optional ('?'). The old synatx '!' has been discontinued. |
6d5213bd9709
uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
wenzelm
parents:
61604
diff
changeset
|
624 |
INCOMPATIBILITY, remove '!' and add '?' as required. |
61565
352c73a689da
Qualifiers in locale expressions default to mandatory regardless of the command.
ballarin
parents:
61551
diff
changeset
|
625 |
|
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
626 |
* Keyword 'rewrites' identifies rewrite morphisms in interpretation |
62017 | 627 |
commands. Previously, the keyword was 'where'. INCOMPATIBILITY. |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61565
diff
changeset
|
628 |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
629 |
* More gentle suppression of syntax along locale morphisms while |
62017 | 630 |
printing terms. Previously 'abbreviation' and 'notation' declarations |
631 |
would be suppressed for morphisms except term identity. Now |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
632 |
'abbreviation' is also kept for morphims that only change the involved |
62017 | 633 |
parameters, and only 'notation' is suppressed. This can be of great help |
634 |
when working with complex locale hierarchies, because proof states are |
|
635 |
displayed much more succinctly. It also means that only notation needs |
|
636 |
to be redeclared if desired, as illustrated by this example: |
|
61701
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
637 |
|
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
638 |
locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65) |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
639 |
begin |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
640 |
definition derived (infixl "\<odot>" 65) where ... |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
641 |
end |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
642 |
|
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
643 |
locale morphism = |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
644 |
left: struct composition + right: struct composition' |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
645 |
for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65) |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
646 |
begin |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
647 |
notation right.derived ("\<odot>''") |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
648 |
end |
e89cfc004f18
Refine the supression of abbreviations for morphisms that are not identities.
ballarin
parents:
61694
diff
changeset
|
649 |
|
61895 | 650 |
* Command 'global_interpretation' issues interpretations into global |
651 |
theories, with optional rewrite definitions following keyword 'defines'. |
|
652 |
||
653 |
* Command 'sublocale' accepts optional rewrite definitions after keyword |
|
61675 | 654 |
'defines'. |
655 |
||
61895 | 656 |
* Command 'permanent_interpretation' has been discontinued. Use |
657 |
'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY. |
|
61670
301e0b4ecd45
coalesce permanent_interpretation.ML with interpretation.ML
haftmann
parents:
61660
diff
changeset
|
658 |
|
61252 | 659 |
* Command 'print_definitions' prints dependencies of definitional |
660 |
specifications. This functionality used to be part of 'print_theory'. |
|
661 |
||
60331 | 662 |
* Configuration option rule_insts_schematic has been discontinued |
62017 | 663 |
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY. |
60331 | 664 |
|
62205 | 665 |
* Abbreviations in type classes now carry proper sort constraint. Rare |
666 |
INCOMPATIBILITY in situations where the previous misbehaviour has been |
|
667 |
exploited. |
|
60347 | 668 |
|
669 |
* Refinement of user-space type system in type classes: pseudo-local |
|
62205 | 670 |
operations behave more similar to abbreviations. Potential |
60347 | 671 |
INCOMPATIBILITY in exotic situations. |
672 |
||
673 |
||
60171 | 674 |
*** HOL *** |
675 |
||
62017 | 676 |
* The 'typedef' command has been upgraded from a partially checked |
677 |
"axiomatization", to a full definitional specification that takes the |
|
678 |
global collection of overloaded constant / type definitions into |
|
679 |
account. Type definitions with open dependencies on overloaded |
|
680 |
definitions need to be specified as "typedef (overloaded)". This |
|
681 |
provides extra robustness in theory construction. Rare INCOMPATIBILITY. |
|
682 |
||
683 |
* Qualification of various formal entities in the libraries is done more |
|
684 |
uniformly via "context begin qualified definition ... end" instead of |
|
685 |
old-style "hide_const (open) ...". Consequently, both the defined |
|
686 |
constant and its defining fact become qualified, e.g. Option.is_none and |
|
687 |
Option.is_none_def. Occasional INCOMPATIBILITY in applications. |
|
688 |
||
689 |
* Some old and rarely used ASCII replacement syntax has been removed. |
|
690 |
INCOMPATIBILITY, standard syntax with symbols should be used instead. |
|
691 |
The subsequent commands help to reproduce the old forms, e.g. to |
|
692 |
simplify porting old theories: |
|
693 |
||
694 |
notation iff (infixr "<->" 25) |
|
695 |
||
696 |
notation Times (infixr "<*>" 80) |
|
697 |
||
698 |
type_notation Map.map (infixr "~=>" 0) |
|
699 |
notation Map.map_comp (infixl "o'_m" 55) |
|
700 |
||
701 |
type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21) |
|
702 |
||
703 |
notation FuncSet.funcset (infixr "->" 60) |
|
704 |
notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60) |
|
705 |
||
706 |
notation Omega_Words_Fun.conc (infixr "conc" 65) |
|
707 |
||
708 |
notation Preorder.equiv ("op ~~") |
|
709 |
and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50) |
|
710 |
||
711 |
notation (in topological_space) tendsto (infixr "--->" 55) |
|
712 |
notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60) |
|
713 |
notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
|
714 |
||
715 |
notation NSA.approx (infixl "@=" 50) |
|
716 |
notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60) |
|
717 |
notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
|
718 |
||
719 |
* The alternative notation "\<Colon>" for type and sort constraints has been |
|
720 |
removed: in LaTeX document output it looks the same as "::". |
|
721 |
INCOMPATIBILITY, use plain "::" instead. |
|
722 |
||
723 |
* Commands 'inductive' and 'inductive_set' work better when names for |
|
724 |
intro rules are omitted: the "cases" and "induct" rules no longer |
|
725 |
declare empty case_names, but no case_names at all. This allows to use |
|
726 |
numbered cases in proofs, without requiring method "goal_cases". |
|
727 |
||
728 |
* Inductive definitions ('inductive', 'coinductive', etc.) expose |
|
729 |
low-level facts of the internal construction only if the option |
|
62093 | 730 |
"inductive_internals" is enabled. This refers to the internal predicate |
62017 | 731 |
definition and its monotonicity result. Rare INCOMPATIBILITY. |
732 |
||
733 |
* Recursive function definitions ('fun', 'function', 'partial_function') |
|
734 |
expose low-level facts of the internal construction only if the option |
|
62205 | 735 |
"function_internals" is enabled. Its internal inductive definition is |
736 |
also subject to "inductive_internals". Rare INCOMPATIBILITY. |
|
62093 | 737 |
|
738 |
* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts |
|
739 |
of the internal construction only if the option "bnf_internals" is |
|
740 |
enabled. This supersedes the former option "bnf_note_all". Rare |
|
741 |
INCOMPATIBILITY. |
|
62017 | 742 |
|
743 |
* Combinator to represent case distinction on products is named |
|
744 |
"case_prod", uniformly, discontinuing any input aliasses. Very popular |
|
745 |
theorem aliasses have been retained. |
|
746 |
||
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
747 |
Consolidated facts: |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
748 |
PairE ~> prod.exhaust |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
749 |
Pair_eq ~> prod.inject |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
750 |
pair_collapse ~> prod.collapse |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
751 |
Pair_fst_snd_eq ~> prod_eq_iff |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
752 |
split_twice ~> prod.case_distrib |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
753 |
split_weak_cong ~> prod.case_cong_weak |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
754 |
split_split ~> prod.split |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
755 |
split_split_asm ~> prod.split_asm |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
756 |
splitI ~> case_prodI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
757 |
splitD ~> case_prodD |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
758 |
splitI2 ~> case_prodI2 |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
759 |
splitI2' ~> case_prodI2' |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
760 |
splitE ~> case_prodE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
761 |
splitE' ~> case_prodE' |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
762 |
split_pair ~> case_prod_Pair |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
763 |
split_eta ~> case_prod_eta |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
764 |
split_comp ~> case_prod_comp |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
765 |
mem_splitI ~> mem_case_prodI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
766 |
mem_splitI2 ~> mem_case_prodI2 |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
767 |
mem_splitE ~> mem_case_prodE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
768 |
The_split ~> The_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
769 |
cond_split_eta ~> cond_case_prod_eta |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
770 |
Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
771 |
Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
772 |
in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
773 |
Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
774 |
Collect_split_Grp_inD ~> Collect_case_prod_Grp_in |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
775 |
Domain_Collect_split ~> Domain_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
776 |
Image_Collect_split ~> Image_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
777 |
Range_Collect_split ~> Range_Collect_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
778 |
Eps_split ~> Eps_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
779 |
Eps_split_eq ~> Eps_case_prod_eq |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
780 |
split_rsp ~> case_prod_rsp |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
781 |
curry_split ~> curry_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
782 |
split_curry ~> case_prod_curry |
62017 | 783 |
|
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
784 |
Changes in structure HOLogic: |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
785 |
split_const ~> case_prod_const |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
786 |
mk_split ~> mk_case_prod |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
787 |
mk_psplits ~> mk_ptupleabs |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61405
diff
changeset
|
788 |
strip_psplits ~> strip_ptupleabs |
62017 | 789 |
|
790 |
INCOMPATIBILITY. |
|
791 |
||
792 |
* The coercions to type 'real' have been reorganised. The function |
|
793 |
'real' is no longer overloaded, but has type 'nat => real' and |
|
794 |
abbreviates of_nat for that type. Also 'real_of_int :: int => real' |
|
795 |
abbreviates of_int for that type. Other overloaded instances of 'real' |
|
796 |
have been replaced by 'real_of_ereal' and 'real_of_float'. |
|
797 |
||
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
798 |
Consolidated facts (among others): |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
799 |
real_of_nat_le_iff -> of_nat_le_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
800 |
real_of_nat_numeral of_nat_numeral |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
801 |
real_of_int_zero of_int_0 |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
802 |
real_of_nat_zero of_nat_0 |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
803 |
real_of_one of_int_1 |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
804 |
real_of_int_add of_int_add |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
805 |
real_of_nat_add of_nat_add |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
806 |
real_of_int_diff of_int_diff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
807 |
real_of_nat_diff of_nat_diff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
808 |
floor_subtract floor_diff_of_int |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
809 |
real_of_int_inject of_int_eq_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
810 |
real_of_int_gt_zero_cancel_iff of_int_0_less_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
811 |
real_of_int_ge_zero_cancel_iff of_int_0_le_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
812 |
real_of_nat_ge_zero of_nat_0_le_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
813 |
real_of_int_ceiling_ge le_of_int_ceiling |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
814 |
ceiling_less_eq ceiling_less_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
815 |
ceiling_le_eq ceiling_le_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
816 |
less_floor_eq less_floor_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
817 |
floor_less_eq floor_less_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
818 |
floor_divide_eq_div floor_divide_of_int_eq |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
819 |
real_of_int_zero_cancel of_nat_eq_0_iff |
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61685
diff
changeset
|
820 |
ceiling_real_of_int ceiling_of_int |
62017 | 821 |
|
822 |
INCOMPATIBILITY. |
|
61143 | 823 |
|
60841 | 824 |
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has |
825 |
been removed. INCOMPATIBILITY. |
|
826 |
||
60712
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset
|
827 |
* Quickcheck setup for finite sets. |
3ba16d28449d
Quickcheck setup for finite sets
Lars Hupel <lars.hupel@mytum.de>
parents:
60707
diff
changeset
|
828 |
|
60171 | 829 |
* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY. |
60138 | 830 |
|
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
831 |
* Sledgehammer: |
61318 | 832 |
- The MaSh relevance filter has been sped up. |
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
833 |
- Proof reconstruction has been improved, to minimize the incidence of |
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
834 |
cases where Sledgehammer gives a proof that does not work. |
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
835 |
- Auto Sledgehammer now minimizes and preplays the results. |
61030 | 836 |
- Handle Vampire 4.0 proof output without raising exception. |
61043 | 837 |
- Eliminated "MASH" environment variable. Use the "MaSh" option in |
838 |
Isabelle/jEdit instead. INCOMPATIBILITY. |
|
61317 | 839 |
- Eliminated obsolete "blocking" option and related subcommands. |
60306
6b7c64ab8bd2
made Auto Sledgehammer behave more like the real thing
blanchet
parents:
60301
diff
changeset
|
840 |
|
60310 | 841 |
* Nitpick: |
61325
1cfc476198c9
avoid too aggressive optimization of 'finite' predicate
blanchet
parents:
61324
diff
changeset
|
842 |
- Fixed soundness bug in translation of "finite" predicate. |
61324
d4ec7594f558
avoid unsound simplification of (C (s x)) when s is a selector but not C's
blanchet
parents:
61318
diff
changeset
|
843 |
- Fixed soundness bug in "destroy_constrs" optimization. |
62080 | 844 |
- Fixed soundness bug in translation of "rat" type. |
60310 | 845 |
- Removed "check_potential" and "check_genuine" options. |
61317 | 846 |
- Eliminated obsolete "blocking" option. |
60310 | 847 |
|
62027 | 848 |
* (Co)datatype package: |
61345 | 849 |
- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF |
850 |
structure on the raw type to an abstract type defined using typedef. |
|
851 |
- Always generate "case_transfer" theorem. |
|
62235 | 852 |
- For mutual types, generate slightly stronger "rel_induct", |
853 |
"rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY. |
|
61551 | 854 |
- Allow discriminators and selectors with the same name as the type |
855 |
being defined. |
|
856 |
- Avoid various internal name clashes (e.g., 'datatype f = f'). |
|
60920 | 857 |
|
62098 | 858 |
* Transfer: new methods for interactive debugging of 'transfer' and |
859 |
'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end', |
|
860 |
'transfer_prover_start' and 'transfer_prover_end'. |
|
61370 | 861 |
|
62118 | 862 |
* New diagnostic command print_record for displaying record definitions. |
863 |
||
60868
dd18c33c001e
direct bootstrap of integer division from natural division
haftmann
parents:
60841
diff
changeset
|
864 |
* Division on integers is bootstrapped directly from division on |
62017 | 865 |
naturals and uses generic numeral algorithm for computations. Slight |
866 |
INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former |
|
867 |
simprocs binary_int_div and binary_int_mod |
|
868 |
||
869 |
* Tightened specification of class semiring_no_zero_divisors. Minor |
|
60516
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
870 |
INCOMPATIBILITY. |
0826b7025d07
generalized some theorems about integral domains and moved to HOL theories
haftmann
parents:
60515
diff
changeset
|
871 |
|
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
872 |
* Class algebraic_semidom introduces common algebraic notions of |
62017 | 873 |
integral (semi)domains, particularly units. Although logically subsumed |
874 |
by fields, is is not a super class of these in order not to burden |
|
875 |
fields with notions that are trivial there. |
|
876 |
||
877 |
* Class normalization_semidom specifies canonical representants for |
|
878 |
equivalence classes of associated elements in an integral (semi)domain. |
|
879 |
This formalizes associated elements as well. |
|
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
880 |
|
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60642
diff
changeset
|
881 |
* Abstract specification of gcd/lcm operations in classes semiring_gcd, |
62017 | 882 |
semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute |
883 |
and gcd_int.commute are subsumed by gcd.commute, as well as |
|
884 |
gcd_nat.assoc and gcd_int.assoc by gcd.assoc. |
|
885 |
||
886 |
* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are |
|
887 |
logically unified to Rings.divide in syntactic type class Rings.divide, |
|
888 |
with infix syntax (_ div _). Infix syntax (_ / _) for field division is |
|
889 |
added later as abbreviation in class Fields.inverse. INCOMPATIBILITY, |
|
890 |
instantiations must refer to Rings.divide rather than the former |
|
891 |
separate constants, hence infix syntax (_ / _) is usually not available |
|
892 |
during instantiation. |
|
893 |
||
894 |
* New cancellation simprocs for boolean algebras to cancel complementary |
|
895 |
terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to |
|
896 |
"top". INCOMPATIBILITY. |
|
61629
90f54d9e63f2
cancel complementary terms as arguments to sup/inf in boolean algebras
Andreas Lochbihler
parents:
61623
diff
changeset
|
897 |
|
62101 | 898 |
* Class uniform_space introduces uniform spaces btw topological spaces |
899 |
and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be |
|
62205 | 900 |
introduced in the form of an uniformity. Some constants are more general |
901 |
now, it may be necessary to add type class constraints. |
|
62101 | 902 |
|
903 |
open_real_def \<leadsto> open_dist |
|
904 |
open_complex_def \<leadsto> open_dist |
|
905 |
||
62026 | 906 |
* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY. |
907 |
||
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
908 |
* Library/Multiset: |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
909 |
- Renamed multiset inclusion operators: |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
910 |
< ~> <# |
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset
|
911 |
> ~> ># |
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
912 |
<= ~> <=# |
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset
|
913 |
>= ~> >=# |
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
914 |
\<le> ~> \<le># |
62208
ad43b3ab06e4
added 'supset' variants for new '<#' etc. symbols on multisets
blanchet
parents:
62205
diff
changeset
|
915 |
\<ge> ~> \<ge># |
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
916 |
INCOMPATIBILITY. |
62209 | 917 |
- Added multiset inclusion operator syntax: |
918 |
\<subset># |
|
919 |
\<subseteq># |
|
920 |
\<supset># |
|
921 |
\<supseteq># |
|
60397
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
922 |
- "'a multiset" is no longer an instance of the "order", |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
923 |
"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff", |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
924 |
"semilattice_inf", and "semilattice_sup" type classes. The theorems |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
925 |
previously provided by these type classes (directly or indirectly) |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
926 |
are now available through the "subset_mset" interpretation |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
927 |
(e.g. add_mono ~> subset_mset.add_mono). |
f8a513fedb31
Renaming multiset operators < ~> <#,...
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
60390
diff
changeset
|
928 |
INCOMPATIBILITY. |
60497 | 929 |
- Renamed conversions: |
60515 | 930 |
multiset_of ~> mset |
931 |
multiset_of_set ~> mset_set |
|
60497 | 932 |
set_of ~> set_mset |
933 |
INCOMPATIBILITY |
|
60398 | 934 |
- Renamed lemmas: |
935 |
mset_le_def ~> subseteq_mset_def |
|
936 |
mset_less_def ~> subset_mset_def |
|
60400 | 937 |
less_eq_multiset.rep_eq ~> subseteq_mset_def |
938 |
INCOMPATIBILITY |
|
939 |
- Removed lemmas generated by lift_definition: |
|
62235 | 940 |
less_eq_multiset.abs_eq, less_eq_multiset.rsp, |
941 |
less_eq_multiset.transfer, less_eq_multiset_def |
|
60400 | 942 |
INCOMPATIBILITY |
60006 | 943 |
|
62017 | 944 |
* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a. |
945 |
||
946 |
* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the |
|
947 |
Bourbaki-Witt fixpoint theorem for increasing functions in |
|
948 |
chain-complete partial orders. |
|
949 |
||
950 |
* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command. |
|
951 |
Minor INCOMPATIBILITY, use 'function' instead. |
|
952 |
||
62064 | 953 |
* Library/Periodic_Fun: a locale that provides convenient lemmas for |
954 |
periodic functions. |
|
62060
b75764fc4c35
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
eberlm
parents:
62034
diff
changeset
|
955 |
|
62098 | 956 |
* Library/Formal_Power_Series: proper definition of division (with |
957 |
remainder) for formal power series; instances for Euclidean Ring and |
|
958 |
GCD. |
|
62086
1c0246456ab9
Added formal power series updates to NEWS/CONTRIBUTORS
Manuel Eberl <eberlm@in.tum.de>
parents:
62084
diff
changeset
|
959 |
|
62084 | 960 |
* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed. |
961 |
||
962 |
* HOL-Statespace: command 'statespace' uses mandatory qualifier for |
|
963 |
import of parent, as for general 'locale' expressions. INCOMPATIBILITY, |
|
964 |
remove '!' and add '?' as required. |
|
965 |
||
62237 | 966 |
* HOL-Decision_Procs: The "approximation" method works with "powr" |
967 |
(exponentiation on real numbers) again. |
|
968 |
||
62084 | 969 |
* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour |
970 |
integrals (= complex path integrals), Cauchy's integral theorem, winding |
|
971 |
numbers and Cauchy's integral formula, Liouville theorem, Fundamental |
|
972 |
Theorem of Algebra. Ported from HOL Light. |
|
973 |
||
974 |
* HOL-Multivariate_Analysis: topological concepts such as connected |
|
62017 | 975 |
components, homotopic paths and the inside or outside of a set. |
61121
efe8b18306b7
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
wenzelm
parents:
61119
diff
changeset
|
976 |
|
62084 | 977 |
* HOL-Multivariate_Analysis: radius of convergence of power series and |
62064 | 978 |
various summability tests; Harmonic numbers and the Euler–Mascheroni |
979 |
constant; the Generalised Binomial Theorem; the complex and real |
|
980 |
Gamma/log-Gamma/Digamma/ Polygamma functions and their most important |
|
981 |
properties. |
|
62060
b75764fc4c35
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
eberlm
parents:
62034
diff
changeset
|
982 |
|
62084 | 983 |
* HOL-Probability: The central limit theorem based on Levy's uniqueness |
984 |
and continuity theorems, weak convergence, and characterisitc functions. |
|
985 |
||
986 |
* HOL-Data_Structures: new and growing session of standard data |
|
987 |
structures. |
|
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
61174
diff
changeset
|
988 |
|
60479 | 989 |
|
60793 | 990 |
*** ML *** |
991 |
||
62017 | 992 |
* The following combinators for low-level profiling of the ML runtime |
993 |
system are available: |
|
994 |
||
995 |
profile_time (*CPU time*) |
|
996 |
profile_time_thread (*CPU time on this thread*) |
|
997 |
profile_allocations (*overall heap allocations*) |
|
998 |
||
999 |
* Antiquotation @{undefined} or \<^undefined> inlines (raise Match). |
|
1000 |
||
62075 | 1001 |
* Antiquotation @{method NAME} inlines the (checked) name of the given |
1002 |
Isar proof method. |
|
1003 |
||
61922 | 1004 |
* Pretty printing of Poly/ML compiler output in Isabelle has been |
1005 |
improved: proper treatment of break offsets and blocks with consistent |
|
1006 |
breaks. |
|
1007 |
||
61268 | 1008 |
* The auxiliary module Pure/display.ML has been eliminated. Its |
1009 |
elementary thm print operations are now in Pure/more_thm.ML and thus |
|
1010 |
called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY. |
|
1011 |
||
61144 | 1012 |
* Simproc programming interfaces have been simplified: |
1013 |
Simplifier.make_simproc and Simplifier.define_simproc supersede various |
|
1014 |
forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that |
|
1015 |
term patterns for the left-hand sides are specified with implicitly |
|
1016 |
fixed variables, like top-level theorem statements. INCOMPATIBILITY. |
|
1017 |
||
60802 | 1018 |
* Instantiation rules have been re-organized as follows: |
1019 |
||
1020 |
Thm.instantiate (*low-level instantiation with named arguments*) |
|
1021 |
Thm.instantiate' (*version with positional arguments*) |
|
1022 |
||
1023 |
Drule.infer_instantiate (*instantiation with type inference*) |
|
1024 |
Drule.infer_instantiate' (*version with positional arguments*) |
|
1025 |
||
1026 |
The LHS only requires variable specifications, instead of full terms. |
|
1027 |
Old cterm_instantiate is superseded by infer_instantiate. |
|
1028 |
INCOMPATIBILITY, need to re-adjust some ML names and types accordingly. |
|
1029 |
||
60793 | 1030 |
* Old tactic shorthands atac, rtac, etac, dtac, ftac have been |
1031 |
discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc. |
|
1032 |
instead (with proper context). |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
1033 |
|
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
1034 |
* Thm.instantiate (and derivatives) no longer require the LHS of the |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
1035 |
instantiation to be certified: plain variables are given directly. |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
1036 |
|
60707
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1037 |
* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1038 |
quasi-bound variables (like the Simplifier), instead of accidentally |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1039 |
named local fixes. This has the potential to improve stability of proof |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1040 |
tools, but can also cause INCOMPATIBILITY for tools that don't observe |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1041 |
the proof context discipline. |
e96b7be56d44
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
wenzelm
parents:
60688
diff
changeset
|
1042 |
|
62017 | 1043 |
* Isar proof methods are based on a slightly more general type |
1044 |
context_tactic, which allows to change the proof context dynamically |
|
1045 |
(e.g. to update cases) and indicate explicit Seq.Error results. Former |
|
1046 |
METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are |
|
1047 |
provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY. |
|
61885
acdfc76a6c33
more explicit ML profiling, with official Isabelle output;
wenzelm
parents:
61848
diff
changeset
|
1048 |
|
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60631
diff
changeset
|
1049 |
|
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
1050 |
*** System *** |
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
1051 |
|
62525 | 1052 |
* Command-line tool "isabelle console" enables print mode "ASCII". |
61958 | 1053 |
|
62017 | 1054 |
* Command-line tool "isabelle update_then" expands old Isar command |
1055 |
conflations: |
|
1056 |
||
1057 |
hence ~> then have |
|
1058 |
thus ~> then show |
|
1059 |
||
1060 |
This syntax is more orthogonal and improves readability and |
|
1061 |
maintainability of proofs. |
|
1062 |
||
61602 | 1063 |
* Global session timeout is multiplied by timeout_scale factor. This |
1064 |
allows to adjust large-scale tests (e.g. AFP) to overall hardware |
|
1065 |
performance. |
|
1066 |
||
61174 | 1067 |
* Property values in etc/symbols may contain spaces, if written with the |
62205 | 1068 |
replacement character "␣" (Unicode point 0x2324). For example: |
61174 | 1069 |
|
61602 | 1070 |
\<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono |
61174 | 1071 |
|
60995
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
1072 |
* Java runtime environment for x86_64-windows allows to use larger heap |
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
1073 |
space. |
5176de8f90db
updated to jdk-8u60, with support for x86_64-windows;
wenzelm
parents:
60986
diff
changeset
|
1074 |
|
61135
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1075 |
* Java runtime options are determined separately for 32bit vs. 64bit |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1076 |
platforms as follows. |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1077 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1078 |
- Isabelle desktop application: platform-specific files that are |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1079 |
associated with the main app bundle |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1080 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1081 |
- isabelle jedit: settings |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1082 |
JEDIT_JAVA_SYSTEM_OPTIONS |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1083 |
JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64 |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1084 |
|
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1085 |
- isabelle build: settings |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1086 |
ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64 |
8f7d802b7a71
clarified Java runtime options (NB: ISABELLE_JAVA_PLATFORM is determined later via component);
wenzelm
parents:
61134
diff
changeset
|
1087 |
|
61294 | 1088 |
* Bash shell function "jvmpath" has been renamed to "platform_path": it |
1089 |
is relevant both for Poly/ML and JVM processes. |
|
1090 |
||
62017 | 1091 |
* Poly/ML default platform architecture may be changed from 32bit to |
62205 | 1092 |
64bit via system option ML_system_64. A system restart (and rebuild) is |
1093 |
required after change. |
|
62017 | 1094 |
|
1095 |
* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which |
|
1096 |
both allow larger heap space than former x86-cygwin. |
|
1097 |
||
62157 | 1098 |
* Heap images are 10-15% smaller due to less wasteful persistent theory |
1099 |
content (using ML type theory_id instead of theory); |
|
1100 |
||
60983
ff4a67c65084
updated to polyml-5.5.3-20150820, with native x86-windows support;
wenzelm
parents:
60922
diff
changeset
|
1101 |
|
60479 | 1102 |
|
60009 | 1103 |
New in Isabelle2015 (May 2015) |
1104 |
------------------------------ |
|
57695 | 1105 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
1106 |
*** General *** |
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
1107 |
|
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset
|
1108 |
* Local theory specification commands may have a 'private' or |
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
1109 |
'qualified' modifier to restrict name space accesses to the local scope, |
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59936
diff
changeset
|
1110 |
as provided by some "context begin ... end" block. For example: |
59926 | 1111 |
|
1112 |
context |
|
1113 |
begin |
|
1114 |
||
1115 |
private definition ... |
|
1116 |
private lemma ... |
|
1117 |
||
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
1118 |
qualified definition ... |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
1119 |
qualified lemma ... |
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59967
diff
changeset
|
1120 |
|
59926 | 1121 |
lemma ... |
1122 |
theorem ... |
|
1123 |
||
1124 |
end |
|
1125 |
||
59901 | 1126 |
* Command 'experiment' opens an anonymous locale context with private |
1127 |
naming policy. |
|
1128 |
||
59951 | 1129 |
* Command 'notepad' requires proper nesting of begin/end and its proof |
1130 |
structure in the body: 'oops' is no longer supported here. Minor |
|
1131 |
INCOMPATIBILITY, use 'sorry' instead. |
|
1132 |
||
1133 |
* Command 'named_theorems' declares a dynamic fact within the context, |
|
1134 |
together with an attribute to maintain the content incrementally. This |
|
1135 |
supersedes functor Named_Thms in Isabelle/ML, but with a subtle change |
|
1136 |
of semantics due to external visual order vs. internal reverse order. |
|
1137 |
||
1138 |
* 'find_theorems': search patterns which are abstractions are |
|
1139 |
schematically expanded before search. Search results match the naive |
|
1140 |
expectation more closely, particularly wrt. abbreviations. |
|
1141 |
INCOMPATIBILITY. |
|
59648 | 1142 |
|
59569 | 1143 |
* Commands 'method_setup' and 'attribute_setup' now work within a local |
1144 |
theory context. |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
1145 |
|
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
1146 |
* Outer syntax commands are managed authentically within the theory |
59569 | 1147 |
context, without implicit global state. Potential for accidental |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
1148 |
INCOMPATIBILITY, make sure that required theories are really imported. |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58872
diff
changeset
|
1149 |
|
60115 | 1150 |
* Historical command-line terminator ";" is no longer accepted (and |
1151 |
already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle |
|
1152 |
update_semicolons" to remove obsolete semicolons from old theory |
|
1153 |
sources. |
|
1154 |
||
59951 | 1155 |
* Structural composition of proof methods (meth1; meth2) in Isar |
1156 |
corresponds to (tac1 THEN_ALL_NEW tac2) in ML. |
|
59105 | 1157 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
1158 |
* The Eisbach proof method language allows to define new proof methods |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
1159 |
by combining existing ones with their usual syntax. The "match" proof |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
1160 |
method provides basic fact/term matching in addition to |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
1161 |
premise/conclusion matching through Subgoal.focus, and binds fact names |
60288
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
1162 |
from matches as well as term patterns within matches. The Isabelle |
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
1163 |
documentation provides an entry "eisbach" for the Eisbach User Manual. |
d7f636331176
added Eisbach manual, using version 8845c4cb28b6 of its Bitbucket repository;
wenzelm
parents:
60273
diff
changeset
|
1164 |
Sources and various examples are in ~~/src/HOL/Eisbach/. |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60115
diff
changeset
|
1165 |
|
57941
57200bdc2aa7
localized command 'method_setup' and 'attribute_setup';
wenzelm
parents:
57882
diff
changeset
|
1166 |
|
58524 | 1167 |
*** Prover IDE -- Isabelle/Scala/jEdit *** |
1168 |
||
59569 | 1169 |
* Improved folding mode "isabelle" based on Isar syntax. Alternatively, |
1170 |
the "sidekick" mode may be used for document structure. |
|
1171 |
||
1172 |
* Extended bracket matching based on Isar language structure. System |
|
1173 |
option jedit_structure_limit determines maximum number of lines to scan |
|
1174 |
in the buffer. |
|
58758 | 1175 |
|
58540 | 1176 |
* Support for BibTeX files: context menu, context-sensitive token |
1177 |
marker, SideKick parser. |
|
58524 | 1178 |
|
58551 | 1179 |
* Document antiquotation @{cite} provides formal markup, which is |
60265 | 1180 |
interpreted semi-formally based on .bib files that happen to be open in |
1181 |
the editor (hyperlinks, completion etc.). |
|
58551 | 1182 |
|
58785 | 1183 |
* Less waste of vertical space via negative line spacing (see Global |
1184 |
Options / Text Area). |
|
1185 |
||
60089
8bd5999133d4
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
wenzelm
parents:
60085
diff
changeset
|
1186 |
* Improved graphview panel with optional output of PNG or PDF, for |
60273
83de10e27007
use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
wenzelm
parents:
60265
diff
changeset
|
1187 |
display of 'thy_deps', 'class_deps' etc. |
60009 | 1188 |
|
60115 | 1189 |
* The commands 'thy_deps' and 'class_deps' allow optional bounds to |
1190 |
restrict the visualized hierarchy. |
|
60093 | 1191 |
|
60072 | 1192 |
* Improved scheduling for asynchronous print commands (e.g. provers |
1193 |
managed by the Sledgehammer panel) wrt. ongoing document processing. |
|
1194 |
||
58524 | 1195 |
|
59951 | 1196 |
*** Document preparation *** |
1197 |
||
1198 |
* Document markup commands 'chapter', 'section', 'subsection', |
|
1199 |
'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any |
|
1200 |
context, even before the initial 'theory' command. Obsolete proof |
|
1201 |
commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been |
|
1202 |
discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw' |
|
1203 |
instead. The old 'header' command is still retained for some time, but |
|
1204 |
should be replaced by 'chapter', 'section' etc. (using "isabelle |
|
1205 |
update_header"). Minor INCOMPATIBILITY. |
|
1206 |
||
60009 | 1207 |
* Official support for "tt" style variants, via \isatt{...} or |
1208 |
\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or |
|
1209 |
verbatim environment of LaTeX is no longer used. This allows @{ML} etc. |
|
1210 |
as argument to other macros (such as footnotes). |
|
1211 |
||
1212 |
* Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
|
1213 |
style. |
|
1214 |
||
1215 |
* Discontinued obsolete option "document_graph": session_graph.pdf is |
|
1216 |
produced unconditionally for HTML browser_info and PDF-LaTeX document. |
|
1217 |
||
59951 | 1218 |
* Diagnostic commands and document markup commands within a proof do not |
1219 |
affect the command tag for output. Thus commands like 'thm' are subject |
|
1220 |
to proof document structure, and no longer "stick out" accidentally. |
|
1221 |
Commands 'text' and 'txt' merely differ in the LaTeX style, not their |
|
1222 |
tags. Potential INCOMPATIBILITY in exotic situations. |
|
1223 |
||
1224 |
* System option "pretty_margin" is superseded by "thy_output_margin", |
|
1225 |
which is also accessible via document antiquotation option "margin". |
|
1226 |
Only the margin for document output may be changed, but not the global |
|
1227 |
pretty printing: that is 76 for plain console output, and adapted |
|
1228 |
dynamically in GUI front-ends. Implementations of document |
|
1229 |
antiquotations need to observe the margin explicitly according to |
|
1230 |
Thy_Output.string_of_margin. Minor INCOMPATIBILITY. |
|
1231 |
||
60299
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
1232 |
* Specification of 'document_files' in the session ROOT file is |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
1233 |
mandatory for document preparation. The legacy mode with implicit |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
1234 |
copying of the document/ directory is no longer supported. Minor |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
1235 |
INCOMPATIBILITY. |
5ae2a2e74c93
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;
wenzelm
parents:
60288
diff
changeset
|
1236 |
|
59951 | 1237 |
|
58202 | 1238 |
*** Pure *** |
1239 |
||
59835
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1240 |
* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1241 |
etc.) allow an optional context of local variables ('for' declaration): |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1242 |
these variables become schematic in the instantiated theorem; this |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1243 |
behaviour is analogous to 'for' in attributes "where" and "of". |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1244 |
Configuration option rule_insts_schematic (default false) controls use |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1245 |
of schematic variables outside the context. Minor INCOMPATIBILITY, |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1246 |
declare rule_insts_schematic = true temporarily and update to use local |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1247 |
variable declarations or dummy patterns instead. |
97872c658a44
rule_insts_schematic is considered legacy and false by default;
wenzelm
parents:
59815
diff
changeset
|
1248 |
|
60009 | 1249 |
* Explicit instantiation via attributes "where", "of", and proof methods |
1250 |
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns |
|
1251 |
("_") that stand for anonymous local variables. |
|
1252 |
||
59951 | 1253 |
* Generated schematic variables in standard format of exported facts are |
1254 |
incremented to avoid material in the proof context. Rare |
|
1255 |
INCOMPATIBILITY, explicit instantiation sometimes needs to refer to |
|
1256 |
different index. |
|
1257 |
||
60010 | 1258 |
* Lexical separation of signed and unsigned numerals: categories "num" |
1259 |
and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence |
|
1260 |
of numeral signs, particularly in expressions involving infix syntax |
|
1261 |
like "(- 1) ^ n". |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58373
diff
changeset
|
1262 |
|
58421 | 1263 |
* Old inner token category "xnum" has been discontinued. Potential |
1264 |
INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" |
|
1265 |
token category instead. |
|
1266 |
||
58202 | 1267 |
|
57737 | 1268 |
*** HOL *** |
1269 |
||
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1270 |
* New (co)datatype package: |
58373 | 1271 |
- The 'datatype_new' command has been renamed 'datatype'. The old |
1272 |
command of that name is now called 'old_datatype' and is provided |
|
1273 |
by "~~/src/HOL/Library/Old_Datatype.thy". See |
|
1274 |
'isabelle doc datatypes' for information on porting. |
|
1275 |
INCOMPATIBILITY. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1276 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1277 |
disc_corec ~> corec_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1278 |
disc_corec_iff ~> corec_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1279 |
disc_exclude ~> distinct_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1280 |
disc_exhaust ~> exhaust_disc |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1281 |
disc_map_iff ~> map_disc_iff |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1282 |
sel_corec ~> corec_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1283 |
sel_exhaust ~> exhaust_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1284 |
sel_map ~> map_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1285 |
sel_set ~> set_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1286 |
sel_split ~> split_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1287 |
sel_split_asm ~> split_sel_asm |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1288 |
strong_coinduct ~> coinduct_strong |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1289 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1290 |
INCOMPATIBILITY. |
58192 | 1291 |
- The "no_code" option to "free_constructors", "datatype_new", and |
1292 |
"codatatype" has been renamed "plugins del: code". |
|
1293 |
INCOMPATIBILITY. |
|
58044 | 1294 |
- The rules "set_empty" have been removed. They are easy |
1295 |
consequences of other set rules "by auto". |
|
1296 |
INCOMPATIBILITY. |
|
1297 |
- The rule "set_cases" is now registered with the "[cases set]" |
|
57990 | 1298 |
attribute. This can influence the behavior of the "cases" proof |
1299 |
method when more than one case rule is applicable (e.g., an |
|
1300 |
assumption is of the form "w : set ws" and the method "cases w" |
|
1301 |
is invoked). The solution is to specify the case rule explicitly |
|
1302 |
(e.g. "cases w rule: widget.exhaust"). |
|
1303 |
INCOMPATIBILITY. |
|
59675 | 1304 |
- Renamed theories: |
1305 |
BNF_Comp ~> BNF_Composition |
|
1306 |
BNF_FP_Base ~> BNF_Fixpoint_Base |
|
1307 |
BNF_GFP ~> BNF_Greatest_Fixpoint |
|
1308 |
BNF_LFP ~> BNF_Least_Fixpoint |
|
1309 |
BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions |
|
1310 |
Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions |
|
1311 |
INCOMPATIBILITY. |
|
60114 | 1312 |
- Lifting and Transfer setup for basic HOL types sum and prod (also |
1313 |
option) is now performed by the BNF package. Theories Lifting_Sum, |
|
1314 |
Lifting_Product and Lifting_Option from Main became obsolete and |
|
1315 |
were removed. Changed definitions of the relators rel_prod and |
|
1316 |
rel_sum (using inductive). |
|
60111 | 1317 |
INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead |
60114 | 1318 |
of rel_prod_def and rel_sum_def. |
1319 |
Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names |
|
1320 |
changed (e.g. map_prod_transfer ~> prod.map_transfer). |
|
60261 | 1321 |
- Parametricity theorems for map functions, relators, set functions, |
1322 |
constructors, case combinators, discriminators, selectors and |
|
1323 |
(co)recursors are automatically proved and registered as transfer |
|
1324 |
rules. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1325 |
|
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1326 |
* Old datatype package: |
58310 | 1327 |
- The old 'datatype' command has been renamed 'old_datatype', and |
58373 | 1328 |
'rep_datatype' has been renamed 'old_rep_datatype'. They are |
1329 |
provided by "~~/src/HOL/Library/Old_Datatype.thy". See |
|
58310 | 1330 |
'isabelle doc datatypes' for information on porting. |
58373 | 1331 |
INCOMPATIBILITY. |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1332 |
- Renamed theorems: |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1333 |
weak_case_cong ~> case_cong_weak |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1334 |
INCOMPATIBILITY. |
58373 | 1335 |
- Renamed theory: |
1336 |
~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy |
|
1337 |
INCOMPATIBILITY. |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57946
diff
changeset
|
1338 |
|
59039 | 1339 |
* Nitpick: |
60010 | 1340 |
- Fixed soundness bug related to the strict and non-strict subset |
59039 | 1341 |
operations. |
1342 |
||
57737 | 1343 |
* Sledgehammer: |
59511 | 1344 |
- CVC4 is now included with Isabelle instead of CVC3 and run by |
1345 |
default. |
|
59965 | 1346 |
- Z3 is now always enabled by default, now that it is fully open |
1347 |
source. The "z3_non_commercial" option is discontinued. |
|
57737 | 1348 |
- Minimization is now always enabled by default. |
60010 | 1349 |
Removed sub-command: |
57737 | 1350 |
min |
59967 | 1351 |
- Proof reconstruction, both one-liners and Isar, has been |
59039 | 1352 |
dramatically improved. |
1353 |
- Improved support for CVC4 and veriT. |
|
57737 | 1354 |
|
58062 | 1355 |
* Old and new SMT modules: |
58067 | 1356 |
- The old 'smt' method has been renamed 'old_smt' and moved to |
59569 | 1357 |
'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility, |
1358 |
until applications have been ported to use the new 'smt' method. For |
|
1359 |
the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must |
|
1360 |
be installed, and the environment variable "OLD_Z3_SOLVER" must |
|
1361 |
point to it. |
|
58062 | 1362 |
INCOMPATIBILITY. |
58067 | 1363 |
- The 'smt2' method has been renamed 'smt'. |
58060 | 1364 |
INCOMPATIBILITY. |
59569 | 1365 |
- New option 'smt_reconstruction_step_timeout' to limit the |
1366 |
reconstruction time of Z3 proof steps in the new 'smt' method. |
|
59216 | 1367 |
- New option 'smt_statistics' to display statistics of the new 'smt' |
1368 |
method, especially runtime statistics of Z3 proof reconstruction. |
|
58060 | 1369 |
|
60261 | 1370 |
* Lifting: command 'lift_definition' allows to execute lifted constants |
1371 |
that have as a return type a datatype containing a subtype. This |
|
1372 |
overcomes long-time limitations in the area of code generation and |
|
1373 |
lifting, and avoids tedious workarounds. |
|
60258 | 1374 |
|
60009 | 1375 |
* Command and antiquotation "value" provide different evaluation slots |
1376 |
(again), where the previous strategy (NBE after ML) serves as default. |
|
1377 |
Minor INCOMPATIBILITY. |
|
1378 |
||
1379 |
* Add NO_MATCH-simproc, allows to check for syntactic non-equality. |
|
1380 |
||
1381 |
* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid |
|
1382 |
non-termination in case of distributing a division. With this change |
|
1383 |
field_simps is in some cases slightly less powerful, if it fails try to |
|
1384 |
add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY. |
|
1385 |
||
1386 |
* Separate class no_zero_divisors has been given up in favour of fully |
|
1387 |
algebraic semiring_no_zero_divisors. INCOMPATIBILITY. |
|
1388 |
||
1389 |
* Class linordered_semidom really requires no zero divisors. |
|
1390 |
INCOMPATIBILITY. |
|
1391 |
||
1392 |
* Classes division_ring, field and linordered_field always demand |
|
1393 |
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero, |
|
1394 |
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY. |
|
1395 |
||
1396 |
* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit |
|
1397 |
additive inverse operation. INCOMPATIBILITY. |
|
1398 |
||
60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60010
diff
changeset
|
1399 |
* Complex powers and square roots. The functions "ln" and "powr" are now |
60025 | 1400 |
overloaded for types real and complex, and 0 powr y = 0 by definition. |
1401 |
INCOMPATIBILITY: type constraints may be necessary. |
|
60020
065ecea354d0
Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.
paulson <lp15@cam.ac.uk>
parents:
60010
diff
changeset
|
1402 |
|
60009 |