author | wenzelm |
Sat, 14 Apr 2012 12:51:38 +0200 | |
changeset 47463 | 9be52539082d |
parent 47462 | 8f85051693d1 |
child 47464 | b1cd02f2d534 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
47462 | 4 |
New in Isabelle2012 (May 2012) |
5 |
------------------------------ |
|
45109 | 6 |
|
45593 | 7 |
*** General *** |
8 |
||
45614 | 9 |
* Prover IDE (PIDE) improvements: |
10 |
||
11 |
- markup for bound variables |
|
12 |
- markup for types of term variables (e.g. displayed as tooltips) |
|
46956
9ff441f295c2
Isabelle/jEdit supports user-defined Isar commands within the running session;
wenzelm
parents:
46948
diff
changeset
|
13 |
- support for user-defined Isar commands within the running session |
47158 | 14 |
- improved support for Unicode outside original 16bit range |
15 |
e.g. glyph for \<A> (thanks to jEdit 4.5.1) |
|
45614 | 16 |
|
46485 | 17 |
* Updated and extended reference manuals ("isar-ref" and |
18 |
"implementation"); reduced remaining material in old "ref" manual. |
|
19 |
||
45593 | 20 |
* Rule attributes in local theory declarations (e.g. locale or class) |
21 |
are now statically evaluated: the resulting theorem is stored instead |
|
22 |
of the original expression. INCOMPATIBILITY in rare situations, where |
|
23 |
the historic accident of dynamic re-evaluation in interpretations |
|
24 |
etc. was exploited. |
|
25 |
||
45600
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
26 |
* Commands 'lemmas' and 'theorems' allow local variables using 'for' |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
27 |
declaration, and results are standardized before being stored. Thus |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
28 |
old-style "standard" after instantiation or composition of facts |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
29 |
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
30 |
indices of schematic variables. |
1bbbac9a0cb0
'lemmas' / 'theorems' commands allow 'for' fixes and standardize the result before storing;
wenzelm
parents:
45593
diff
changeset
|
31 |
|
46483 | 32 |
* Renamed some inner syntax categories: |
33 |
||
34 |
num ~> num_token |
|
35 |
xnum ~> xnum_token |
|
36 |
xstr ~> str_token |
|
37 |
||
38 |
Minor INCOMPATIBILITY. Note that in practice "num_const" or |
|
39 |
"num_position" etc. are mainly used instead (which also include |
|
40 |
position information via constraints). |
|
45703
c7a13ce60161
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
wenzelm
parents:
45625
diff
changeset
|
41 |
|
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46497
diff
changeset
|
42 |
* Simplified configuration options for syntax ambiguity: see |
46512
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
43 |
"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref |
4f9f61f9b535
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46506
diff
changeset
|
44 |
manual. Minor INCOMPATIBILITY. |
46506
c7faa011bfa7
simplified configuration options for syntax ambiguity;
wenzelm
parents:
46497
diff
changeset
|
45 |
|
46959
cdc791910460
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents:
46956
diff
changeset
|
46 |
* Forward declaration of outer syntax keywords within the theory |
cdc791910460
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents:
46956
diff
changeset
|
47 |
header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
cdc791910460
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents:
46956
diff
changeset
|
48 |
commands to be used in the same theory where defined. |
cdc791910460
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents:
46956
diff
changeset
|
49 |
|
47113
b5a5662528fb
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents:
47108
diff
changeset
|
50 |
* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar |
47185
300fa46fd081
clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME;
wenzelm
parents:
47172
diff
changeset
|
51 |
(not just JRE). |
47113
b5a5662528fb
ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents:
47108
diff
changeset
|
52 |
|
45593 | 53 |
|
45134 | 54 |
*** Pure *** |
55 |
||
47427
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47413
diff
changeset
|
56 |
* Rule composition via attribute "OF" (or ML functions OF/MRS) is more |
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47413
diff
changeset
|
57 |
tolerant against multiple unifiers, as long as the final result is |
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47413
diff
changeset
|
58 |
unique. (As before, rules are composed in canonical right-to-left |
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47413
diff
changeset
|
59 |
order to accommodate newly introduced premises.) |
0daa97ed1585
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
wenzelm
parents:
47413
diff
changeset
|
60 |
|
46976
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
61 |
* Command 'definition' no longer exports the foundational "raw_def" |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
62 |
into the user context. Minor INCOMPATIBILITY, may use the regular |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
63 |
"def" result with attribute "abs_def" to imitate the old version. |
80123a220219
'definition' no longer exports the foundational "raw_def";
wenzelm
parents:
46966
diff
changeset
|
64 |
|
46903
3d44892ac0d6
improved attribute "abs_def" to handle object-equality as well;
wenzelm
parents:
46888
diff
changeset
|
65 |
* Attribute "abs_def" turns an equation of the form "f x y == t" into |
3d44892ac0d6
improved attribute "abs_def" to handle object-equality as well;
wenzelm
parents:
46888
diff
changeset
|
66 |
"f == %x y. t", which ensures that "simp" or "unfold" steps always |
3d44892ac0d6
improved attribute "abs_def" to handle object-equality as well;
wenzelm
parents:
46888
diff
changeset
|
67 |
expand it. This also works for object-logic equality. (Formerly |
3d44892ac0d6
improved attribute "abs_def" to handle object-equality as well;
wenzelm
parents:
46888
diff
changeset
|
68 |
undocumented feature.) |
3d44892ac0d6
improved attribute "abs_def" to handle object-equality as well;
wenzelm
parents:
46888
diff
changeset
|
69 |
|
46493 | 70 |
* Discontinued old "prems" fact, which used to refer to the accidental |
71 |
collection of foundational premises in the context (marked as legacy |
|
72 |
since Isabelle2011). |
|
73 |
||
45134 | 74 |
* Obsolete command 'types' has been discontinued. Use 'type_synonym' |
75 |
instead. INCOMPATIBILITY. |
|
76 |
||
45191 | 77 |
* Ancient code generator for SML and its commands 'code_module', |
45383 | 78 |
'code_library', 'consts_code', 'types_code' have been discontinued. |
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
79 |
Use commands of the generic code generator instead. INCOMPATIBILITY. |
45383 | 80 |
|
81 |
* Redundant attribute 'code_inline' has been discontinued. Use |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
82 |
'code_unfold' instead. INCOMPATIBILITY. |
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
83 |
|
46160 | 84 |
* Dropped attribute 'code_unfold_post' in favor of the its dual |
85 |
'code_abbrev', which yields a common pattern in definitions like |
|
46028
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
86 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
87 |
definition [code_abbrev]: "f = t" |
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
88 |
|
9f113cdf3d66
attribute code_abbrev superseedes code_unfold_post
haftmann
parents:
46014
diff
changeset
|
89 |
INCOMPATIBILITY. |
45383 | 90 |
|
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
91 |
* Sort constraints are now propagated in simultaneous statements, just |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
92 |
like type constraints. INCOMPATIBILITY in rare situations, where |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
93 |
distinct sorts used to be assigned accidentally. For example: |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
94 |
|
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
95 |
lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
96 |
|
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
97 |
lemma "P (x::'a)" and "Q (y::'a::bar)" |
47462 | 98 |
-- "now uniform 'a::bar instead of default sort for first occurrence (!)" |
45427
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
99 |
|
fca432074fb2
sort assignment before simultaneous term_check, not isolated parse_term;
wenzelm
parents:
45398
diff
changeset
|
100 |
|
45122 | 101 |
*** HOL *** |
102 |
||
47270 | 103 |
* New tutorial Programming and Proving in Isabelle/HOL |
104 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
105 |
* The representation of numerals has changed. We now have a datatype |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
106 |
"num" representing strictly positive binary numerals, along with |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
107 |
functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
108 |
represent positive and negated numeric literals, respectively. (See |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
109 |
definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
110 |
may require adaptations: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
111 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
112 |
- Theorems with number_ring or number_semiring constraints: These |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
113 |
classes are gone; use comm_ring_1 or comm_semiring_1 instead. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
114 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
115 |
- Theories defining numeric types: Remove number, number_semiring, |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
116 |
and number_ring instances. Defer all theorems about numerals until |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
117 |
after classes one and semigroup_add have been instantiated. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
118 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
119 |
- Numeral-only simp rules: Replace each rule having a "number_of v" |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
120 |
pattern with two copies, one for numeral and one for neg_numeral. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
121 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
122 |
- Theorems about subclasses of semiring_1 or ring_1: These classes |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
123 |
automatically support numerals now, so more simp rules and |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
124 |
simprocs may now apply within the proof. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
125 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
126 |
- Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
127 |
Redefine using other integer operations. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
47086
diff
changeset
|
128 |
|
46160 | 129 |
* Type 'a set is now a proper type constructor (just as before |
130 |
Isabelle2008). Definitions mem_def and Collect_def have disappeared. |
|
131 |
Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
|
132 |
sets separate, it is often sufficient to rephrase sets S accidentally |
|
133 |
used as predicates by "%x. x : S" and predicates P accidentally used |
|
134 |
as sets by "{x. P x}". Corresponding proofs in a first step should be |
|
135 |
pruned from any tinkering with former theorems mem_def and |
|
46834
a5fa1dc55945
less rigorous but more realistic migration recommendation; note on code generation of sets
haftmann
parents:
46752
diff
changeset
|
136 |
Collect_def as far as possible. |
a5fa1dc55945
less rigorous but more realistic migration recommendation; note on code generation of sets
haftmann
parents:
46752
diff
changeset
|
137 |
For developments which deliberately mixed predicates and |
46160 | 138 |
sets, a planning step is necessary to determine what should become a |
139 |
predicate and what a set. It can be helpful to carry out that step in |
|
140 |
Isabelle2011-1 before jumping right into the current release. |
|
141 |
||
46834
a5fa1dc55945
less rigorous but more realistic migration recommendation; note on code generation of sets
haftmann
parents:
46752
diff
changeset
|
142 |
* Code generation by default implements sets as container type rather |
a5fa1dc55945
less rigorous but more realistic migration recommendation; note on code generation of sets
haftmann
parents:
46752
diff
changeset
|
143 |
than predicates. INCOMPATIBILITY. |
a5fa1dc55945
less rigorous but more realistic migration recommendation; note on code generation of sets
haftmann
parents:
46752
diff
changeset
|
144 |
|
47265 | 145 |
* New proof import from HOL Light: Faster, simpler, and more scalable. |
146 |
Requires a proof bundle, which is available as an external component. |
|
147 |
Removed old (and mostly dead) Importer for HOL4 and HOL Light. |
|
148 |
INCOMPATIBILITY. |
|
47264
6488c5efec49
renamed import session back to Import, conforming to directory name; NEWS
krauss
parents:
47217
diff
changeset
|
149 |
|
46373 | 150 |
* New type synonym 'a rel = ('a * 'a) set |
151 |
||
47142 | 152 |
* Theory Divides: Discontinued redundant theorems about div and mod. |
153 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
154 |
||
155 |
DIVISION_BY_ZERO ~> div_by_0, mod_by_0 |
|
156 |
zdiv_self ~> div_self |
|
157 |
zmod_self ~> mod_self |
|
158 |
zdiv_zero ~> div_0 |
|
159 |
zmod_zero ~> mod_0 |
|
47165 | 160 |
zdiv_zmod_equality ~> div_mod_equality2 |
161 |
zdiv_zmod_equality2 ~> div_mod_equality |
|
47142 | 162 |
zmod_zdiv_trivial ~> mod_div_trivial |
47159 | 163 |
zdiv_zminus_zminus ~> div_minus_minus |
164 |
zmod_zminus_zminus ~> mod_minus_minus |
|
165 |
zdiv_zminus2 ~> div_minus_right |
|
166 |
zmod_zminus2 ~> mod_minus_right |
|
47160 | 167 |
zdiv_minus1_right ~> div_minus1_right |
168 |
zmod_minus1_right ~> mod_minus1_right |
|
47162 | 169 |
zdvd_mult_div_cancel ~> dvd_mult_div_cancel |
47163 | 170 |
zmod_zmult1_eq ~> mod_mult_right_eq |
47164 | 171 |
zpower_zmod ~> power_mod |
47167 | 172 |
zdvd_zmod ~> dvd_mod |
173 |
zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd |
|
47159 | 174 |
mod_mult_distrib ~> mult_mod_left |
175 |
mod_mult_distrib2 ~> mult_mod_right |
|
47142 | 176 |
|
47217
501b9bbd0d6e
removed redundant nat-specific copies of theorems
huffman
parents:
47202
diff
changeset
|
177 |
* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use |
501b9bbd0d6e
removed redundant nat-specific copies of theorems
huffman
parents:
47202
diff
changeset
|
178 |
generic mult_2 and mult_2_right instead. INCOMPATIBILITY. |
501b9bbd0d6e
removed redundant nat-specific copies of theorems
huffman
parents:
47202
diff
changeset
|
179 |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
180 |
* More default pred/set conversions on a couple of relation operations |
47202 | 181 |
and predicates. Added powers of predicate relations. |
182 |
Consolidation of some relation theorems: |
|
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
183 |
|
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
184 |
converse_def ~> converse_unfold |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
185 |
rel_comp_def ~> rel_comp_unfold |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
186 |
symp_def ~> (dropped, use symp_def and sym_def instead) |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
187 |
transp_def ~> transp_trans |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
188 |
Domain_def ~> Domain_unfold |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
189 |
Range_def ~> Domain_converse [symmetric] |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
190 |
|
46981 | 191 |
Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. |
192 |
||
47086 | 193 |
See theory "Relation" for examples for making use of pred/set conversions |
194 |
by means of attributes "to_set" and "to_pred". |
|
195 |
||
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
196 |
INCOMPATIBILITY. |
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
197 |
|
46160 | 198 |
* Consolidated various theorem names relating to Finite_Set.fold |
199 |
combinator: |
|
200 |
||
46145
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
201 |
inf_INFI_fold_inf ~> inf_INF_fold_inf |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
202 |
sup_SUPR_fold_sup ~> sup_SUP_fold_sup |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
203 |
INFI_fold_inf ~> INF_fold_inf |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
204 |
SUPR_fold_sup ~> SUP_fold_sup |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
205 |
union_set ~> union_set_fold |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
206 |
minus_set ~> minus_set_fold |
46752
e9e7209eb375
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
haftmann
parents:
46732
diff
changeset
|
207 |
|
46145
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
208 |
INCOMPATIBILITY. |
0ec0af1c651d
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
haftmann
parents:
46141
diff
changeset
|
209 |
|
46132
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
210 |
* Consolidated theorem names concerning fold combinators: |
46160 | 211 |
|
46132
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
212 |
INFI_set_fold ~> INF_set_fold |
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
213 |
SUPR_set_fold ~> SUP_set_fold |
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
214 |
INF_code ~> INF_set_foldr |
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
215 |
SUP_code ~> SUP_set_foldr |
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
216 |
foldr.simps ~> foldr.simps (in point-free formulation) |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
217 |
foldr_fold_rev ~> foldr_conv_fold |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
218 |
foldl_fold ~> foldl_conv_fold |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
219 |
foldr_foldr ~> foldr_conv_foldl |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
220 |
foldl_foldr ~> foldl_conv_foldr |
46160 | 221 |
|
46132
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
222 |
INCOMPATIBILITY. |
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
223 |
|
46160 | 224 |
* Dropped rarely useful theorems concerning fold combinators: |
225 |
foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant, |
|
226 |
rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, |
|
227 |
concat_conv_foldl, foldl_weak_invariant, foldl_invariant, |
|
228 |
foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, |
|
47397
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
229 |
listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
230 |
foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
231 |
INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
232 |
and "List.foldl plus 0", prefer "List.listsum". Otherwise it can |
d654c73e4b12
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
haftmann
parents:
47349
diff
changeset
|
233 |
be useful to boil down "List.foldr" and "List.foldl" to "List.fold" |
47399 | 234 |
by unfolding "foldr_conv_fold" and "foldl_conv_fold". |
235 |
||
236 |
* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, |
|
237 |
inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, |
|
238 |
Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr, |
|
239 |
INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding |
|
240 |
lemmas over fold rather than foldr, or make use of lemmas |
|
241 |
fold_conv_foldr and fold_rev. |
|
46132
5a29dbf4c155
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes
haftmann
parents:
46126
diff
changeset
|
242 |
|
46528 | 243 |
* Congruence rules Option.map_cong and Option.bind_cong for recursion |
244 |
through option types. |
|
245 |
||
46125
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
246 |
* Concrete syntax for case expressions includes constraints for source |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
247 |
positions, and thus produces Prover IDE markup for its bindings. |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
248 |
INCOMPATIBILITY for old-style syntax translations that augment the |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
249 |
pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
250 |
one_case. |
00cd193a48dc
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
wenzelm
parents:
46028
diff
changeset
|
251 |
|
46126
bab00660539d
discontinued Syntax.positions -- atomic parse trees are always annotated;
wenzelm
parents:
46125
diff
changeset
|
252 |
* Discontinued configuration option "syntax_positions": atomic terms |
bab00660539d
discontinued Syntax.positions -- atomic parse trees are always annotated;
wenzelm
parents:
46125
diff
changeset
|
253 |
in parse trees are always annotated by position constraints. |
bab00660539d
discontinued Syntax.positions -- atomic parse trees are always annotated;
wenzelm
parents:
46125
diff
changeset
|
254 |
|
45991 | 255 |
* Finite_Set.fold now qualified. INCOMPATIBILITY. |
256 |
||
46160 | 257 |
* Renamed some facts on canonical fold on lists, in order to avoid |
258 |
problems with interpretation involving corresponding facts on foldl |
|
259 |
with the same base names: |
|
45988 | 260 |
|
261 |
fold_set_remdups ~> fold_set_fold_remdups |
|
262 |
fold_set ~> fold_set_fold |
|
263 |
fold1_set ~> fold1_set_fold |
|
264 |
||
265 |
INCOMPATIBILITY. |
|
266 |
||
46363 | 267 |
* Renamed facts about the power operation on relations, i.e., relpow |
268 |
to match the constant's name: |
|
47463 | 269 |
|
46458 | 270 |
rel_pow_1 ~> relpow_1 |
46363 | 271 |
rel_pow_0_I ~> relpow_0_I |
272 |
rel_pow_Suc_I ~> relpow_Suc_I |
|
273 |
rel_pow_Suc_I2 ~> relpow_Suc_I2 |
|
274 |
rel_pow_0_E ~> relpow_0_E |
|
275 |
rel_pow_Suc_E ~> relpow_Suc_E |
|
276 |
rel_pow_E ~> relpow_E |
|
46458 | 277 |
rel_pow_Suc_D2 ~> relpow_Suc_D2 |
47463 | 278 |
rel_pow_Suc_E2 ~> relpow_Suc_E2 |
46363 | 279 |
rel_pow_Suc_D2' ~> relpow_Suc_D2' |
280 |
rel_pow_E2 ~> relpow_E2 |
|
281 |
rel_pow_add ~> relpow_add |
|
282 |
rel_pow_commute ~> relpow |
|
283 |
rel_pow_empty ~> relpow_empty: |
|
284 |
rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow |
|
285 |
rel_pow_imp_rtrancl ~> relpow_imp_rtrancl |
|
286 |
rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow |
|
287 |
rtrancl_imp_rel_pow ~> rtrancl_imp_relpow |
|
288 |
rel_pow_fun_conv ~> relpow_fun_conv |
|
289 |
rel_pow_finite_bounded1 ~> relpow_finite_bounded1 |
|
290 |
rel_pow_finite_bounded ~> relpow_finite_bounded |
|
291 |
rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow |
|
292 |
trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow |
|
293 |
single_valued_rel_pow ~> single_valued_relpow |
|
47463 | 294 |
|
46363 | 295 |
INCOMPATIBILITY. |
296 |
||
47448 | 297 |
* Theory Relation: Consolidated constant name for relation composition |
298 |
and corresponding theorem names: |
|
299 |
- Renamed constant rel_comp to relcomp |
|
300 |
- Dropped abbreviation pred_comp. Use relcompp instead. |
|
301 |
- Renamed theorems: |
|
302 |
Relation: |
|
303 |
rel_compI ~> relcompI |
|
304 |
rel_compEpair ~> relcompEpair |
|
305 |
rel_compE ~> relcompE |
|
306 |
pred_comp_rel_comp_eq ~> relcompp_relcomp_eq |
|
307 |
rel_comp_empty1 ~> relcomp_empty1 |
|
308 |
rel_comp_mono ~> relcomp_mono |
|
309 |
rel_comp_subset_Sigma ~> relcomp_subset_Sigma |
|
310 |
rel_comp_distrib ~> relcomp_distrib |
|
311 |
rel_comp_distrib2 ~> relcomp_distrib2 |
|
312 |
rel_comp_UNION_distrib ~> relcomp_UNION_distrib |
|
313 |
rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2 |
|
314 |
single_valued_rel_comp ~> single_valued_relcomp |
|
315 |
rel_comp_unfold ~> relcomp_unfold |
|
316 |
converse_rel_comp ~> converse_relcomp |
|
317 |
pred_compI ~> relcomppI |
|
318 |
pred_compE ~> relcomppE |
|
319 |
pred_comp_bot1 ~> relcompp_bot1 |
|
320 |
pred_comp_bot2 ~> relcompp_bot2 |
|
321 |
transp_pred_comp_less_eq ~> transp_relcompp_less_eq |
|
322 |
pred_comp_mono ~> relcompp_mono |
|
323 |
pred_comp_distrib ~> relcompp_distrib |
|
324 |
pred_comp_distrib2 ~> relcompp_distrib2 |
|
325 |
converse_pred_comp ~> converse_relcompp |
|
326 |
Transitive_Closure: |
|
327 |
finite_rel_comp ~> finite_relcomp |
|
328 |
List: |
|
329 |
set_rel_comp ~> set_relcomp |
|
330 |
||
331 |
INCOMPATIBILITY. |
|
332 |
||
46239 | 333 |
* New theory HOL/Library/DAList provides an abstract type for association |
334 |
lists with distinct keys. |
|
45874 | 335 |
|
45839
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45810
diff
changeset
|
336 |
* 'datatype' specifications allow explicit sort constraints. |
43a5b86bc102
'datatype' specifications allow explicit sort constraints;
wenzelm
parents:
45810
diff
changeset
|
337 |
|
46160 | 338 |
* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, |
339 |
use theory HOL/Library/Nat_Bijection instead. |
|
340 |
||
47452 | 341 |
* Theory HOL/Library/RBT_Impl: Backing implementation of red-black trees is |
47463 | 342 |
now inside the type class' local context. Names of affected operations and lemmas |
47452 | 343 |
have been prefixed by rbt_. INCOMPATIBILITY for theories working directly with |
344 |
raw red-black trees, adapt the names as follows: |
|
345 |
||
346 |
Operations: |
|
347 |
bulkload -> rbt_bulkload |
|
348 |
del_from_left -> rbt_del_from_left |
|
349 |
del_from_right -> rbt_del_from_right |
|
350 |
del -> rbt_del |
|
351 |
delete -> rbt_delete |
|
352 |
ins -> rbt_ins |
|
353 |
insert -> rbt_insert |
|
354 |
insertw -> rbt_insert_with |
|
355 |
insert_with_key -> rbt_insert_with_key |
|
356 |
map_entry -> rbt_map_entry |
|
357 |
lookup -> rbt_lookup |
|
358 |
sorted -> rbt_sorted |
|
359 |
tree_greater -> rbt_greater |
|
360 |
tree_less -> rbt_less |
|
361 |
tree_less_symbol -> rbt_less_symbol |
|
362 |
union -> rbt_union |
|
363 |
union_with -> rbt_union_with |
|
364 |
union_with_key -> rbt_union_with_key |
|
365 |
||
366 |
Lemmas: |
|
367 |
balance_left_sorted -> balance_left_rbt_sorted |
|
368 |
balance_left_tree_greater -> balance_left_rbt_greater |
|
369 |
balance_left_tree_less -> balance_left_rbt_less |
|
370 |
balance_right_sorted -> balance_right_rbt_sorted |
|
371 |
balance_right_tree_greater -> balance_right_rbt_greater |
|
372 |
balance_right_tree_less -> balance_right_rbt_less |
|
373 |
balance_sorted -> balance_rbt_sorted |
|
374 |
balance_tree_greater -> balance_rbt_greater |
|
375 |
balance_tree_less -> balance_rbt_less |
|
376 |
bulkload_is_rbt -> rbt_bulkload_is_rbt |
|
377 |
combine_sorted -> combine_rbt_sorted |
|
378 |
combine_tree_greater -> combine_rbt_greater |
|
379 |
combine_tree_less -> combine_rbt_less |
|
380 |
delete_in_tree -> rbt_delete_in_tree |
|
381 |
delete_is_rbt -> rbt_delete_is_rbt |
|
382 |
del_from_left_tree_greater -> rbt_del_from_left_rbt_greater |
|
383 |
del_from_left_tree_less -> rbt_del_from_left_rbt_less |
|
384 |
del_from_right_tree_greater -> rbt_del_from_right_rbt_greater |
|
385 |
del_from_right_tree_less -> rbt_del_from_right_rbt_less |
|
386 |
del_in_tree -> rbt_del_in_tree |
|
387 |
del_inv1_inv2 -> rbt_del_inv1_inv2 |
|
388 |
del_sorted -> rbt_del_rbt_sorted |
|
389 |
del_tree_greater -> rbt_del_rbt_greater |
|
390 |
del_tree_less -> rbt_del_rbt_less |
|
391 |
dom_lookup_Branch -> dom_rbt_lookup_Branch |
|
392 |
entries_lookup -> entries_rbt_lookup |
|
393 |
finite_dom_lookup -> finite_dom_rbt_lookup |
|
394 |
insert_sorted -> rbt_insert_rbt_sorted |
|
395 |
insertw_is_rbt -> rbt_insertw_is_rbt |
|
396 |
insertwk_is_rbt -> rbt_insertwk_is_rbt |
|
397 |
insertwk_sorted -> rbt_insertwk_rbt_sorted |
|
398 |
insertw_sorted -> rbt_insertw_rbt_sorted |
|
399 |
ins_sorted -> ins_rbt_sorted |
|
400 |
ins_tree_greater -> ins_rbt_greater |
|
401 |
ins_tree_less -> ins_rbt_less |
|
402 |
is_rbt_sorted -> is_rbt_rbt_sorted |
|
403 |
lookup_balance -> rbt_lookup_balance |
|
404 |
lookup_bulkload -> rbt_lookup_rbt_bulkload |
|
405 |
lookup_delete -> rbt_lookup_rbt_delete |
|
406 |
lookup_Empty -> rbt_lookup_Empty |
|
407 |
lookup_from_in_tree -> rbt_lookup_from_in_tree |
|
408 |
lookup_in_tree -> rbt_lookup_in_tree |
|
409 |
lookup_ins -> rbt_lookup_ins |
|
410 |
lookup_insert -> rbt_lookup_rbt_insert |
|
411 |
lookup_insertw -> rbt_lookup_rbt_insertw |
|
412 |
lookup_insertwk -> rbt_lookup_rbt_insertwk |
|
413 |
lookup_keys -> rbt_lookup_keys |
|
414 |
lookup_map -> rbt_lookup_map |
|
415 |
lookup_map_entry -> rbt_lookup_rbt_map_entry |
|
416 |
lookup_tree_greater -> rbt_lookup_rbt_greater |
|
417 |
lookup_tree_less -> rbt_lookup_rbt_less |
|
418 |
lookup_union -> rbt_lookup_rbt_union |
|
419 |
map_entry_color_of -> rbt_map_entry_color_of |
|
420 |
map_entry_inv1 -> rbt_map_entry_inv1 |
|
421 |
map_entry_inv2 -> rbt_map_entry_inv2 |
|
422 |
map_entry_is_rbt -> rbt_map_entry_is_rbt |
|
423 |
map_entry_sorted -> rbt_map_entry_rbt_sorted |
|
424 |
map_entry_tree_greater -> rbt_map_entry_rbt_greater |
|
425 |
map_entry_tree_less -> rbt_map_entry_rbt_less |
|
426 |
map_tree_greater -> map_rbt_greater |
|
427 |
map_tree_less -> map_rbt_less |
|
428 |
map_sorted -> map_rbt_sorted |
|
429 |
paint_sorted -> paint_rbt_sorted |
|
430 |
paint_lookup -> paint_rbt_lookup |
|
431 |
paint_tree_greater -> paint_rbt_greater |
|
432 |
paint_tree_less -> paint_rbt_less |
|
433 |
sorted_entries -> rbt_sorted_entries |
|
434 |
tree_greater_eq_trans -> rbt_greater_eq_trans |
|
435 |
tree_greater_nit -> rbt_greater_nit |
|
436 |
tree_greater_prop -> rbt_greater_prop |
|
437 |
tree_greater_simps -> rbt_greater_simps |
|
438 |
tree_greater_trans -> rbt_greater_trans |
|
439 |
tree_less_eq_trans -> rbt_less_eq_trans |
|
440 |
tree_less_nit -> rbt_less_nit |
|
441 |
tree_less_prop -> rbt_less_prop |
|
442 |
tree_less_simps -> rbt_less_simps |
|
443 |
tree_less_trans -> rbt_less_trans |
|
444 |
tree_ord_props -> rbt_ord_props |
|
445 |
union_Branch -> rbt_union_Branch |
|
446 |
union_is_rbt -> rbt_union_is_rbt |
|
447 |
unionw_is_rbt -> rbt_unionw_is_rbt |
|
448 |
unionwk_is_rbt -> rbt_unionwk_is_rbt |
|
449 |
unionwk_sorted -> rbt_unionwk_rbt_sorted |
|
450 |
||
46160 | 451 |
* Session HOL-Word: Discontinued many redundant theorems specific to |
452 |
type 'a word. INCOMPATIBILITY, use the corresponding generic theorems |
|
453 |
instead. |
|
45546
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
454 |
|
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
455 |
word_sub_alt ~> word_sub_wi |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
456 |
word_add_alt ~> word_add_def |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
457 |
word_mult_alt ~> word_mult_def |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
458 |
word_minus_alt ~> word_minus_def |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
459 |
word_0_alt ~> word_0_wi |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
460 |
word_1_alt ~> word_1_wi |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
461 |
word_add_0 ~> add_0_left |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
462 |
word_add_0_right ~> add_0_right |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
463 |
word_mult_1 ~> mult_1_left |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
464 |
word_mult_1_right ~> mult_1_right |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
465 |
word_add_commute ~> add_commute |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
466 |
word_add_assoc ~> add_assoc |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
467 |
word_add_left_commute ~> add_left_commute |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
468 |
word_mult_commute ~> mult_commute |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
469 |
word_mult_assoc ~> mult_assoc |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
470 |
word_mult_left_commute ~> mult_left_commute |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
471 |
word_left_distrib ~> left_distrib |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
472 |
word_right_distrib ~> right_distrib |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
473 |
word_left_minus ~> left_minus |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
474 |
word_diff_0_right ~> diff_0_right |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
475 |
word_diff_self ~> diff_self |
45957 | 476 |
word_sub_def ~> diff_minus |
45804 | 477 |
word_diff_minus ~> diff_minus |
45546
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
478 |
word_add_ac ~> add_ac |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
479 |
word_mult_ac ~> mult_ac |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
480 |
word_plus_ac0 ~> add_0_left add_0_right add_ac |
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
481 |
word_times_ac1 ~> mult_1_left mult_1_right mult_ac |
45547 | 482 |
word_order_trans ~> order_trans |
483 |
word_order_refl ~> order_refl |
|
484 |
word_order_antisym ~> order_antisym |
|
485 |
word_order_linear ~> linorder_linear |
|
45810 | 486 |
lenw1_zero_neq_one ~> zero_neq_one |
487 |
word_number_of_eq ~> number_of_eq |
|
46013 | 488 |
word_of_int_add_hom ~> wi_hom_add |
489 |
word_of_int_sub_hom ~> wi_hom_sub |
|
490 |
word_of_int_mult_hom ~> wi_hom_mult |
|
491 |
word_of_int_minus_hom ~> wi_hom_neg |
|
492 |
word_of_int_succ_hom ~> wi_hom_succ |
|
493 |
word_of_int_pred_hom ~> wi_hom_pred |
|
494 |
word_of_int_0_hom ~> word_0_wi |
|
495 |
word_of_int_1_hom ~> word_1_wi |
|
45546
6dd3e88de4c2
HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents:
45516
diff
changeset
|
496 |
|
46014 | 497 |
* Clarified attribute "mono_set": pure declaration without modifying |
45384
dffa657f0aa2
clarified attribute "mono_set": pure declaration, proper export in ML;
wenzelm
parents:
45383
diff
changeset
|
498 |
the result of the fact expression. |
dffa657f0aa2
clarified attribute "mono_set": pure declaration, proper export in ML;
wenzelm
parents:
45383
diff
changeset
|
499 |
|
45383 | 500 |
* "Transitive_Closure.ntrancl": bounded transitive closure on |
501 |
relations. |
|
502 |
||
46014 | 503 |
* Constant "Set.not_member" now qualified. INCOMPATIBILITY. |
45383 | 504 |
|
505 |
* "sublists" moved to theory More_List. INCOMPATIBILITY. |
|
45143 | 506 |
|
45122 | 507 |
* Theory Int: Discontinued many legacy theorems specific to type int. |
45383 | 508 |
INCOMPATIBILITY, use the corresponding generic theorems instead. |
45122 | 509 |
|
510 |
zminus_zminus ~> minus_minus |
|
511 |
zminus_0 ~> minus_zero |
|
512 |
zminus_zadd_distrib ~> minus_add_distrib |
|
513 |
zadd_commute ~> add_commute |
|
514 |
zadd_assoc ~> add_assoc |
|
515 |
zadd_left_commute ~> add_left_commute |
|
45196
78478d938cb8
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
wenzelm
parents:
45191
diff
changeset
|
516 |
zadd_ac ~> add_ac |
45122 | 517 |
zmult_ac ~> mult_ac |
518 |
zadd_0 ~> add_0_left |
|
519 |
zadd_0_right ~> add_0_right |
|
520 |
zadd_zminus_inverse2 ~> left_minus |
|
521 |
zmult_zminus ~> mult_minus_left |
|
522 |
zmult_commute ~> mult_commute |
|
523 |
zmult_assoc ~> mult_assoc |
|
524 |
zadd_zmult_distrib ~> left_distrib |
|
525 |
zadd_zmult_distrib2 ~> right_distrib |
|
526 |
zdiff_zmult_distrib ~> left_diff_distrib |
|
527 |
zdiff_zmult_distrib2 ~> right_diff_distrib |
|
528 |
zmult_1 ~> mult_1_left |
|
529 |
zmult_1_right ~> mult_1_right |
|
530 |
zle_refl ~> order_refl |
|
531 |
zle_trans ~> order_trans |
|
532 |
zle_antisym ~> order_antisym |
|
533 |
zle_linear ~> linorder_linear |
|
534 |
zless_linear ~> linorder_less_linear |
|
535 |
zadd_left_mono ~> add_left_mono |
|
536 |
zadd_strict_right_mono ~> add_strict_right_mono |
|
537 |
zadd_zless_mono ~> add_less_le_mono |
|
538 |
int_0_less_1 ~> zero_less_one |
|
539 |
int_0_neq_1 ~> zero_neq_one |
|
540 |
zless_le ~> less_le |
|
541 |
zpower_zadd_distrib ~> power_add |
|
542 |
zero_less_zpower_abs_iff ~> zero_less_power_abs_iff |
|
543 |
zero_le_zpower_abs ~> zero_le_power_abs |
|
544 |
||
45791 | 545 |
* Theory Deriv: Renamed |
546 |
||
547 |
DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing |
|
548 |
||
45383 | 549 |
* New "case_product" attribute to generate a case rule doing multiple |
550 |
case distinctions at the same time. E.g. |
|
551 |
||
552 |
list.exhaust [case_product nat.exhaust] |
|
553 |
||
554 |
produces a rule which can be used to perform case distinction on both |
|
555 |
a list and a nat. |
|
556 |
||
46170 | 557 |
* Improved code generation of multisets. |
558 |
||
46591 | 559 |
* New diagnostic command find_unused_assms to find potentially superfluous |
560 |
assumptions in theorems using Quickcheck. |
|
561 |
||
45759 | 562 |
* Quickcheck: |
563 |
- Quickcheck returns variable assignments as counterexamples, which |
|
564 |
allows to reveal the underspecification of functions under test. |
|
565 |
For example, refuting "hd xs = x", it presents the variable |
|
566 |
assignment xs = [] and x = a1 as a counterexample, assuming that |
|
567 |
any property is false whenever "hd []" occurs in it. |
|
568 |
These counterexample are marked as potentially spurious, as |
|
569 |
Quickcheck also returns "xs = []" as a counterexample to the |
|
570 |
obvious theorem "hd xs = hd xs". |
|
571 |
After finding a potentially spurious counterexample, Quickcheck |
|
572 |
continues searching for genuine ones. |
|
573 |
By default, Quickcheck shows potentially spurious and genuine |
|
574 |
counterexamples. The option "genuine_only" sets quickcheck to |
|
575 |
only show genuine counterexamples. |
|
45941 | 576 |
|
577 |
- The command 'quickcheck_generator' creates random and exhaustive |
|
578 |
value generators for a given type and operations. |
|
579 |
It generates values by using the operations as if they were |
|
47463 | 580 |
constructors of that type. |
46170 | 581 |
|
582 |
- Support for multisets. |
|
583 |
||
46591 | 584 |
- Added "use_subtype" options. |
47349
803729c9fd4d
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
bulwahn
parents:
47270
diff
changeset
|
585 |
- Added "quickcheck_locale" configuration to specify how to process |
803729c9fd4d
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
bulwahn
parents:
47270
diff
changeset
|
586 |
conjectures in a locale context. |
803729c9fd4d
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
bulwahn
parents:
47270
diff
changeset
|
587 |
|
45398
7dbb7b044a11
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
blanchet
parents:
45384
diff
changeset
|
588 |
* Nitpick: |
45516 | 589 |
- Fixed infinite loop caused by the 'peephole_optim' option and |
590 |
affecting 'rat' and 'real'. |
|
591 |
||
592 |
* Sledgehammer: |
|
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46373
diff
changeset
|
593 |
- Added "lam_trans", "uncurry_aliases", and "minimize" options. |
45706 | 594 |
- Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). |
46301 | 595 |
- Renamed "sound" option to "strict". |
45516 | 596 |
|
597 |
* Metis: |
|
598 |
- Added possibility to specify lambda translations scheme as a |
|
46366 | 599 |
parenthesized argument (e.g., "by (metis (lifting) ...)"). |
45398
7dbb7b044a11
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
blanchet
parents:
45384
diff
changeset
|
600 |
|
47197 | 601 |
* SMT: |
602 |
- renamed "smt_fixed" option to "smt_read_only_certificates". |
|
47463 | 603 |
|
46641 | 604 |
* Command 'try0': |
605 |
- Renamed from 'try_methods'. INCOMPATIBILITY. |
|
606 |
||
46888 | 607 |
* New "eventually_elim" method as a generalized variant of the |
608 |
eventually_elim* rules. Supports structured proofs. |
|
609 |
||
47413 | 610 |
* HOL/TPTP: support to parse and import TPTP problems (all languages) |
611 |
into Isabelle/HOL. |
|
612 |
||
45398
7dbb7b044a11
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
blanchet
parents:
45384
diff
changeset
|
613 |
|
45160 | 614 |
*** FOL *** |
615 |
||
45383 | 616 |
* New "case_product" attribute (see HOL). |
45160 | 617 |
|
45109 | 618 |
|
47463 | 619 |
*** ZF *** |
620 |
||
621 |
* Greater support for structured proofs involving induction or case |
|
622 |
analysis. |
|
623 |
||
624 |
* Much greater use of mathematical symbols. |
|
625 |
||
626 |
* Removal of many ML theorem bindings. INCOMPATIBILITY. |
|
627 |
||
628 |
||
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
629 |
*** ML *** |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
630 |
|
46948 | 631 |
* Antiquotation @{keyword "name"} produces a parser for outer syntax |
632 |
from a minor keyword introduced via theory header declaration. |
|
633 |
||
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
634 |
* Antiquotation @{command_spec "name"} produces the |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
635 |
Outer_Syntax.command_spec from a major keyword introduced via theory |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
636 |
header declaration; it can be passed to Outer_Syntax.command etc. |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46959
diff
changeset
|
637 |
|
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
46903
diff
changeset
|
638 |
* Local_Theory.define no longer hard-wires default theorem name |
46992
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
639 |
"foo_def", but retains the binding as given. If that is Binding.empty |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
640 |
/ Attrib.empty_binding, the result is not registered as user-level |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
641 |
fact. The Local_Theory.define_internal variant allows to specify a |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
642 |
non-empty name (used for the foundation in the background theory), |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
643 |
while omitting the fact binding in the user-context. Potential |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
644 |
INCOMPATIBILITY for derived definitional packages: need to specify |
eeea81b86b70
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
wenzelm
parents:
46983
diff
changeset
|
645 |
naming policy for primitive definitions more explicitly. |
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
46903
diff
changeset
|
646 |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
647 |
* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
648 |
conformance with similar operations in structure Term and Logic. |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
46493
diff
changeset
|
649 |
|
45592 | 650 |
* Antiquotation @{attributes [...]} embeds attribute source |
651 |
representation into the ML text, which is particularly useful with |
|
652 |
declarations like Local_Theory.note. |
|
653 |
||
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
654 |
* Structure Proof_Context follows standard naming scheme. Old |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
655 |
ProofContext has been discontinued. INCOMPATIBILITY. |
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
656 |
|
45293
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
657 |
* Refined Local_Theory.declaration {syntax, pervasive}, with subtle |
45298
aa35859c8741
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
wenzelm
parents:
45293
diff
changeset
|
658 |
change of semantics: update is applied to auxiliary local theory |
45293
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
659 |
context as well. |
57def0b39696
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
wenzelm
parents:
45233
diff
changeset
|
660 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
661 |
* Modernized some old-style infix operations: |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
662 |
|
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
663 |
addeqcongs ~> Simplifier.add_eqcong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
664 |
deleqcongs ~> Simplifier.del_eqcong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
665 |
addcongs ~> Simplifier.add_cong |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
666 |
delcongs ~> Simplifier.del_cong |
45625
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
667 |
setmksimps ~> Simplifier.set_mksimps |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
668 |
setmkcong ~> Simplifier.set_mkcong |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
669 |
setmksym ~> Simplifier.set_mksym |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
670 |
setmkeqTrue ~> Simplifier.set_mkeqTrue |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
671 |
settermless ~> Simplifier.set_termless |
750c5a47400b
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45620
diff
changeset
|
672 |
setsubgoaler ~> Simplifier.set_subgoaler |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
673 |
addsplits ~> Splitter.add_split |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
674 |
delsplits ~> Splitter.del_split |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45614
diff
changeset
|
675 |
|
45128
5af3a3203a76
discontinued obsolete alias structure ProofContext;
wenzelm
parents:
45122
diff
changeset
|
676 |
|
47461
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
677 |
*** System *** |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
678 |
|
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
679 |
* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
680 |
notation, which is useful for the jEdit file browser, for example. |
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
681 |
|
5a7903ba2dac
more robust treatment of ISABELLE_HOME on windows: eliminate spaces and funny unicode characters in directory name via DOS~1 notation;
wenzelm
parents:
47453
diff
changeset
|
682 |
|
45109 | 683 |
|
44801 | 684 |
New in Isabelle2011-1 (October 2011) |
685 |
------------------------------------ |
|
41651 | 686 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
687 |
*** General *** |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
688 |
|
44760 | 689 |
* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as |
44968 | 690 |
"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line. |
44760 | 691 |
|
44777 | 692 |
- Management of multiple theory files directly from the editor |
44760 | 693 |
buffer store -- bypassing the file-system (no requirement to save |
694 |
files for checking). |
|
695 |
||
44777 | 696 |
- Markup of formal entities within the text buffer, with semantic |
44760 | 697 |
highlighting, tooltips and hyperlinks to jump to defining source |
698 |
positions. |
|
699 |
||
44777 | 700 |
- Improved text rendering, with sub/superscripts in the source |
701 |
buffer (including support for copy/paste wrt. output panel, HTML |
|
702 |
theory output and other non-Isabelle text boxes). |
|
703 |
||
704 |
- Refined scheduling of proof checking and printing of results, |
|
44760 | 705 |
based on interactive editor view. (Note: jEdit folding and |
706 |
narrowing allows to restrict buffer perspectives explicitly.) |
|
707 |
||
44777 | 708 |
- Reduced CPU performance requirements, usable on machines with few |
44760 | 709 |
cores. |
710 |
||
44777 | 711 |
- Reduced memory requirements due to pruning of unused document |
44760 | 712 |
versions (garbage collection). |
713 |
||
714 |
See also ~~/src/Tools/jEdit/README.html for further information, |
|
715 |
including some remaining limitations. |
|
716 |
||
44800 | 717 |
* Theory loader: source files are exclusively located via the master |
718 |
directory of each theory node (where the .thy file itself resides). |
|
719 |
The global load path (such as src/HOL/Library) has been discontinued. |
|
720 |
Note that the path element ~~ may be used to reference theories in the |
|
721 |
Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". |
|
722 |
INCOMPATIBILITY. |
|
723 |
||
41955
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
724 |
* Theory loader: source files are identified by content via SHA1 |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
725 |
digests. Discontinued former path/modtime identification and optional |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
726 |
ISABELLE_FILE_IDENT plugin scripts. |
703ea96b13c6
files are identified via SHA1 digests -- discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41952
diff
changeset
|
727 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
728 |
* Parallelization of nested Isar proofs is subject to |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
729 |
Goal.parallel_proofs_threshold (default 100). See also isabelle |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
730 |
usedir option -Q. |
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
731 |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
732 |
* Name space: former unsynchronized references are now proper |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
733 |
configuration options, with more conventional names: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
734 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
735 |
long_names ~> names_long |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
736 |
short_names ~> names_short |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
737 |
unique_names ~> names_unique |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
738 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
739 |
Minor INCOMPATIBILITY, need to declare options in context like this: |
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
740 |
|
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42658
diff
changeset
|
741 |
declare [[names_unique = false]] |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42290
diff
changeset
|
742 |
|
42502 | 743 |
* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note |
744 |
that the result needs to be unique, which means fact specifications |
|
745 |
may have to be refined after enriching a proof context. |
|
746 |
||
44800 | 747 |
* Attribute "case_names" has been refined: the assumptions in each case |
748 |
can be named now by following the case name with [name1 name2 ...]. |
|
749 |
||
44968 | 750 |
* Isabelle/Isar reference manual has been updated and extended: |
751 |
- "Synopsis" provides a catalog of main Isar language concepts. |
|
752 |
- Formal references in syntax diagrams, via @{rail} antiquotation. |
|
753 |
- Updated material from classic "ref" manual, notably about |
|
754 |
"Classical Reasoner". |
|
42633 | 755 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
756 |
|
41727
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
757 |
*** HOL *** |
ab3f6d76fb23
available_provers ~> supported_provers (for clarity)
blanchet
parents:
41703
diff
changeset
|
758 |
|
44968 | 759 |
* Class bot and top require underlying partial order rather than |
44800 | 760 |
preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. |
43815
4f6e2965d821
adjusted to tightened specification of classes bot and top
haftmann
parents:
43752
diff
changeset
|
761 |
|
43940 | 762 |
* Class complete_lattice: generalized a couple of lemmas from sets; |
44800 | 763 |
generalized theorems INF_cong and SUP_cong. New type classes for |
764 |
complete boolean algebras and complete linear orders. Lemmas |
|
765 |
Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in |
|
766 |
class complete_linorder. |
|
767 |
||
768 |
Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
|
769 |
Sup_fun_def, Inf_apply, Sup_apply. |
|
770 |
||
45088 | 771 |
Removed redundant lemmas (the right hand side gives hints how to |
772 |
replace them for (metis ...), or (simp only: ...) proofs): |
|
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
773 |
|
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
774 |
Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
775 |
Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right] |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
776 |
Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
777 |
Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
778 |
Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
779 |
Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
780 |
Inter_def ~> INF_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
781 |
Union_def ~> SUP_def, image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
782 |
INT_eq ~> INF_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
783 |
UN_eq ~> SUP_def, and image_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
784 |
INF_subset ~> INF_superset_mono [OF _ order_refl] |
44800 | 785 |
|
786 |
More consistent and comprehensive names: |
|
787 |
||
45041
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
788 |
INTER_eq_Inter_image ~> INF_def |
0523a6be8ade
NEWS: mention replacement lemmas for the removed ones in Complete_Lattices
hoelzl
parents:
45016
diff
changeset
|
789 |
UNION_eq_Union_image ~> SUP_def |
43872 | 790 |
INFI_def ~> INF_def |
791 |
SUPR_def ~> SUP_def |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
792 |
INF_leI ~> INF_lower |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
793 |
INF_leI2 ~> INF_lower2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
794 |
le_INFI ~> INF_greatest |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
795 |
le_SUPI ~> SUP_upper |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
796 |
le_SUPI2 ~> SUP_upper2 |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
797 |
SUP_leI ~> SUP_least |
43873 | 798 |
INFI_bool_eq ~> INF_bool_eq |
799 |
SUPR_bool_eq ~> SUP_bool_eq |
|
800 |
INFI_apply ~> INF_apply |
|
801 |
SUPR_apply ~> SUP_apply |
|
44103
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
802 |
INTER_def ~> INTER_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
803 |
UNION_def ~> UNION_eq |
cedaca00789f
more uniform naming scheme for Inf/INF and Sup/SUP lemmas
haftmann
parents:
44086
diff
changeset
|
804 |
|
43865
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
805 |
INCOMPATIBILITY. |
db18f4d0cc7d
further generalization from sets to complete lattices
haftmann
parents:
43816
diff
changeset
|
806 |
|
44973
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
807 |
* Renamed theory Complete_Lattice to Complete_Lattices. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
808 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
809 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
810 |
* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
811 |
INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
812 |
Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
813 |
Sup_insert are now declared as [simp]. INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
814 |
|
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
815 |
* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
816 |
compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
817 |
sup_inf_absob, sup_left_idem are now declared as [simp]. Minor |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
818 |
INCOMPATIBILITY. |
dfe923d5308d
separated NEWS for Isabelle2011 from Isabelle2011-1 (cf. e1139e612b55);
wenzelm
parents:
44968
diff
changeset
|
819 |
|
44845 | 820 |
* Added syntactic classes "inf" and "sup" for the respective |
821 |
constants. INCOMPATIBILITY: Changes in the argument order of the |
|
822 |
(mostly internal) locale predicates for some derived classes. |
|
823 |
||
44800 | 824 |
* Theorem collections ball_simps and bex_simps do not contain theorems |
825 |
referring to UNION any longer; these have been moved to collection |
|
826 |
UN_ball_bex_simps. INCOMPATIBILITY. |
|
827 |
||
828 |
* Theory Archimedean_Field: floor now is defined as parameter of a |
|
829 |
separate type class floor_ceiling. |
|
830 |
||
831 |
* Theory Finite_Set: more coherent development of fold_set locales: |
|
42874 | 832 |
|
833 |
locale fun_left_comm ~> locale comp_fun_commute |
|
834 |
locale fun_left_comm_idem ~> locale comp_fun_idem |
|
44800 | 835 |
|
836 |
Both use point-free characterization; interpretation proofs may need |
|
837 |
adjustment. INCOMPATIBILITY. |
|
42874 | 838 |
|
44800 | 839 |
* Theory Limits: Type "'a net" has been renamed to "'a filter", in |
44081
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
840 |
accordance with standard mathematical terminology. INCOMPATIBILITY. |
730f7cced3a6
rename type 'a net to 'a filter, following standard mathematical terminology
huffman
parents:
44027
diff
changeset
|
841 |
|
44800 | 842 |
* Theory Complex_Main: The locale interpretations for the |
843 |
bounded_linear and bounded_bilinear locales have been removed, in |
|
844 |
order to reduce the number of duplicate lemmas. Users must use the |
|
845 |
original names for distributivity theorems, potential INCOMPATIBILITY. |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
846 |
|
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
847 |
divide.add ~> add_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
848 |
divide.diff ~> diff_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
849 |
divide.setsum ~> setsum_divide_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
850 |
mult.add_right ~> right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
851 |
mult.diff_right ~> right_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
852 |
mult_right.setsum ~> setsum_right_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
853 |
mult_left.diff ~> left_diff_distrib |
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44274
diff
changeset
|
854 |
|
44800 | 855 |
* Theory Complex_Main: Several redundant theorems have been removed or |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
856 |
replaced by more general versions. INCOMPATIBILITY. |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
857 |
|
45051
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
858 |
real_diff_def ~> minus_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
859 |
real_divide_def ~> divide_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
860 |
real_less_def ~> less_le |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
861 |
real_abs_def ~> abs_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
862 |
real_sgn_def ~> sgn_real_def |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
863 |
real_mult_commute ~> mult_commute |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
864 |
real_mult_assoc ~> mult_assoc |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
865 |
real_mult_1 ~> mult_1_left |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
866 |
real_add_mult_distrib ~> left_distrib |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
867 |
real_zero_not_eq_one ~> zero_neq_one |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
868 |
real_mult_inverse_left ~> left_inverse |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
869 |
INVERSE_ZERO ~> inverse_zero |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
870 |
real_le_refl ~> order_refl |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
871 |
real_le_antisym ~> order_antisym |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
872 |
real_le_trans ~> order_trans |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
873 |
real_le_linear ~> linear |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
874 |
real_le_eq_diff ~> le_iff_diff_le_0 |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
875 |
real_add_left_mono ~> add_left_mono |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
876 |
real_mult_order ~> mult_pos_pos |
c478d1876371
discontinued legacy theorem names from RealDef.thy
huffman
parents:
45049
diff
changeset
|
877 |
real_mult_less_mono2 ~> mult_strict_left_mono |
44822
2690b6de5021
remove duplicate lemma real_of_int_real_of_nat in favor of real_of_int_of_nat_eq
huffman
parents:
44777
diff
changeset
|
878 |
real_of_int_real_of_nat ~> real_of_int_of_nat_eq |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
879 |
real_0_le_divide_iff ~> zero_le_divide_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
880 |
realpow_two_disj ~> power2_eq_iff |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
881 |
real_squared_diff_one_factored ~> square_diff_one_factored |
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
882 |
realpow_two_diff ~> square_diff_square_factored |
44669
8e6cdb9c00a7
remove redundant lemma reals_complete2 in favor of complete_real
huffman
parents:
44666
diff
changeset
|
883 |
reals_complete2 ~> complete_real |
44749
5b1e1432c320
remove redundant lemma real_sum_squared_expand in favor of power2_sum
huffman
parents:
44748
diff
changeset
|
884 |
real_sum_squared_expand ~> power2_sum |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
885 |
exp_ln_eq ~> ln_unique |
44711 | 886 |
expi_add ~> exp_add |
887 |
expi_zero ~> exp_zero |
|
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
888 |
lemma_DERIV_subst ~> DERIV_cong |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
889 |
LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
890 |
LIMSEQ_const ~> tendsto_const |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
891 |
LIMSEQ_norm ~> tendsto_norm |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
892 |
LIMSEQ_add ~> tendsto_add |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
893 |
LIMSEQ_minus ~> tendsto_minus |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
894 |
LIMSEQ_minus_cancel ~> tendsto_minus_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
895 |
LIMSEQ_diff ~> tendsto_diff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
896 |
bounded_linear.LIMSEQ ~> bounded_linear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
897 |
bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
898 |
LIMSEQ_mult ~> tendsto_mult |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
899 |
LIMSEQ_inverse ~> tendsto_inverse |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
900 |
LIMSEQ_divide ~> tendsto_divide |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
901 |
LIMSEQ_pow ~> tendsto_power |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
902 |
LIMSEQ_setsum ~> tendsto_setsum |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
903 |
LIMSEQ_setprod ~> tendsto_setprod |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
904 |
LIMSEQ_norm_zero ~> tendsto_norm_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
905 |
LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
906 |
LIMSEQ_imp_rabs ~> tendsto_rabs |
44710 | 907 |
LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] |
908 |
LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] |
|
909 |
LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] |
|
44748
7f6838b3474a
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
huffman
parents:
44711
diff
changeset
|
910 |
LIMSEQ_Complex ~> tendsto_Complex |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
911 |
LIM_ident ~> tendsto_ident_at |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
912 |
LIM_const ~> tendsto_const |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
913 |
LIM_add ~> tendsto_add |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
914 |
LIM_add_zero ~> tendsto_add_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
915 |
LIM_minus ~> tendsto_minus |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
916 |
LIM_diff ~> tendsto_diff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
917 |
LIM_norm ~> tendsto_norm |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
918 |
LIM_norm_zero ~> tendsto_norm_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
919 |
LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
920 |
LIM_norm_zero_iff ~> tendsto_norm_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
921 |
LIM_rabs ~> tendsto_rabs |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
922 |
LIM_rabs_zero ~> tendsto_rabs_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
923 |
LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
924 |
LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
925 |
LIM_compose ~> tendsto_compose |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
926 |
LIM_mult ~> tendsto_mult |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
927 |
LIM_scaleR ~> tendsto_scaleR |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
928 |
LIM_of_real ~> tendsto_of_real |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
929 |
LIM_power ~> tendsto_power |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
930 |
LIM_inverse ~> tendsto_inverse |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
931 |
LIM_sgn ~> tendsto_sgn |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
932 |
isCont_LIM_compose ~> isCont_tendsto_compose |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
933 |
bounded_linear.LIM ~> bounded_linear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
934 |
bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
935 |
bounded_bilinear.LIM ~> bounded_bilinear.tendsto |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
936 |
bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
937 |
bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
938 |
bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero |
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44538
diff
changeset
|
939 |
LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] |
44522
2f7e9d890efe
rename subset_{interior,closure} to {interior,closure}_mono;
huffman
parents:
44322
diff
changeset
|
940 |
|
44967 | 941 |
* Theory Complex_Main: The definition of infinite series was |
942 |
generalized. Now it is defined on the type class {topological_space, |
|
943 |
comm_monoid_add}. Hence it is useable also for extended real numbers. |
|
42484 | 944 |
|
44908 | 945 |
* Theory Complex_Main: The complex exponential function "expi" is now |
946 |
a type-constrained abbreviation for "exp :: complex => complex"; thus |
|
947 |
several polymorphic lemmas about "exp" are now applicable to "expi". |
|
948 |
||
44968 | 949 |
* Code generation: |
950 |
||
951 |
- Theory Library/Code_Char_ord provides native ordering of |
|
952 |
characters in the target language. |
|
953 |
||
954 |
- Commands code_module and code_library are legacy, use export_code |
|
955 |
instead. |
|
956 |
||
957 |
- Method "evaluation" is legacy, use method "eval" instead. |
|
958 |
||
959 |
- Legacy evaluator "SML" is deactivated by default. May be |
|
960 |
reactivated by the following theory command: |
|
961 |
||
962 |
setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} |
|
963 |
||
964 |
* Declare ext [intro] by default. Rare INCOMPATIBILITY. |
|
965 |
||
45088 | 966 |
* New proof method "induction" that gives induction hypotheses the |
967 |
name "IH", thus distinguishing them from further hypotheses that come |
|
968 |
from rule induction. The latter are still called "hyps". Method |
|
969 |
"induction" is a thin wrapper around "induct" and follows the same |
|
970 |
syntax. |
|
971 |
||
44968 | 972 |
* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is |
973 |
still available as a legacy feature for some time. |
|
974 |
||
975 |
* Nitpick: |
|
976 |
- Added "need" and "total_consts" options. |
|
977 |
- Reintroduced "show_skolems" option by popular demand. |
|
978 |
- Renamed attribute: nitpick_def ~> nitpick_unfold. |
|
979 |
INCOMPATIBILITY. |
|
980 |
||
981 |
* Sledgehammer: |
|
982 |
- Use quasi-sound (and efficient) translations by default. |
|
983 |
- Added support for the following provers: E-ToFoF, LEO-II, |
|
984 |
Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. |
|
985 |
- Automatically preplay and minimize proofs before showing them if |
|
986 |
this can be done within reasonable time. |
|
987 |
- sledgehammer available_provers ~> sledgehammer supported_provers. |
|
988 |
INCOMPATIBILITY. |
|
989 |
- Added "preplay_timeout", "slicing", "type_enc", "sound", |
|
990 |
"max_mono_iters", and "max_new_mono_instances" options. |
|
991 |
- Removed "explicit_apply" and "full_types" options as well as "Full |
|
992 |
Types" Proof General menu item. INCOMPATIBILITY. |
|
993 |
||
994 |
* Metis: |
|
995 |
- Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. |
|
996 |
- Obsoleted "metisFT" -- use "metis (full_types)" instead. |
|
997 |
INCOMPATIBILITY. |
|
998 |
||
999 |
* Command 'try': |
|
1000 |
- Renamed 'try_methods' and added "simp:", "intro:", "dest:", and |
|
1001 |
"elim:" options. INCOMPATIBILITY. |
|
1002 |
- Introduced 'try' that not only runs 'try_methods' but also |
|
1003 |
'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. |
|
1004 |
||
1005 |
* Quickcheck: |
|
1006 |
- Added "eval" option to evaluate terms for the found counterexample |
|
1007 |
(currently only supported by the default (exhaustive) tester). |
|
1008 |
- Added post-processing of terms to obtain readable counterexamples |
|
1009 |
(currently only supported by the default (exhaustive) tester). |
|
1010 |
- New counterexample generator quickcheck[narrowing] enables |
|
1011 |
narrowing-based testing. Requires the Glasgow Haskell compiler |
|
1012 |
with its installation location defined in the Isabelle settings |
|
1013 |
environment as ISABELLE_GHC. |
|
1014 |
- Removed quickcheck tester "SML" based on the SML code generator |
|
1015 |
(formly in HOL/Library). |
|
1016 |
||
1017 |
* Function package: discontinued option "tailrec". INCOMPATIBILITY, |
|
1018 |
use 'partial_function' instead. |
|
1019 |
||
1020 |
* Theory Library/Extended_Reals replaces now the positive extended |
|
1021 |
reals found in probability theory. This file is extended by |
|
1022 |
Multivariate_Analysis/Extended_Real_Limits. |
|
1023 |
||
44974 | 1024 |
* Theory Library/Old_Recdef: old 'recdef' package has been moved here, |
1025 |
from where it must be imported explicitly if it is really required. |
|
1026 |
INCOMPATIBILITY. |
|
44968 | 1027 |
|
1028 |
* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has |
|
1029 |
been moved here. INCOMPATIBILITY. |
|
1030 |
||
1031 |
* Theory Library/Saturated provides type of numbers with saturated |
|
1032 |
arithmetic. |
|
1033 |
||
1034 |
* Theory Library/Product_Lattice defines a pointwise ordering for the |
|
1035 |
product type 'a * 'b, and provides instance proofs for various order |
|
1036 |
and lattice type classes. |
|
1037 |
||
1038 |
* Theory Library/Countable now provides the "countable_datatype" proof |
|
1039 |
method for proving "countable" class instances for datatypes. |
|
1040 |
||
1041 |
* Theory Library/Cset_Monad allows do notation for computable sets |
|
1042 |
(cset) via the generic monad ad-hoc overloading facility. |
|
1043 |
||
1044 |
* Library: Theories of common data structures are split into theories |
|
1045 |
for implementation, an invariant-ensuring type, and connection to an |
|
1046 |
abstract type. INCOMPATIBILITY. |
|
1047 |
||
1048 |
- RBT is split into RBT and RBT_Mapping. |
|
1049 |
- AssocList is split and renamed into AList and AList_Mapping. |
|
1050 |
- DList is split into DList_Impl, DList, and DList_Cset. |
|
1051 |
- Cset is split into Cset and List_Cset. |
|
1052 |
||
1053 |
* Theory Library/Nat_Infinity has been renamed to |
|
1054 |
Library/Extended_Nat, with name changes of the following types and |
|
1055 |
constants: |
|
1056 |
||
1057 |
type inat ~> type enat |
|
1058 |
Fin ~> enat |
|
1059 |
Infty ~> infinity (overloaded) |
|
1060 |
iSuc ~> eSuc |
|
1061 |
the_Fin ~> the_enat |
|
1062 |
||
1063 |
Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has |
|
1064 |
been renamed accordingly. INCOMPATIBILITY. |
|
1065 |
||
1066 |
* Session Multivariate_Analysis: The euclidean_space type class now |
|
1067 |
fixes a constant "Basis :: 'a set" consisting of the standard |
|
1068 |
orthonormal basis for the type. Users now have the option of |
|
1069 |
quantifying over this set instead of using the "basis" function, e.g. |
|
1070 |
"ALL x:Basis. P x" vs "ALL i<DIM('a). P (basis i)". |
|
1071 |
||
1072 |
* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed |
|
1073 |
to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants |
|
1074 |
"Cart_nth" and "Cart_lambda" have been respectively renamed to |
|
1075 |
"vec_nth" and "vec_lambda"; theorems mentioning those names have |
|
1076 |
changed to match. Definition theorems for overloaded constants now use |
|
1077 |
the standard "foo_vec_def" naming scheme. A few other theorems have |
|
1078 |
been renamed as follows (INCOMPATIBILITY): |
|
1079 |
||
1080 |
Cart_eq ~> vec_eq_iff |
|
1081 |
dist_nth_le_cart ~> dist_vec_nth_le |
|
1082 |
tendsto_vector ~> vec_tendstoI |
|
1083 |
Cauchy_vector ~> vec_CauchyI |
|
1084 |
||
1085 |
* Session Multivariate_Analysis: Several duplicate theorems have been |
|
1086 |
removed, and other theorems have been renamed or replaced with more |
|
1087 |
general versions. INCOMPATIBILITY. |
|
1088 |
||
1089 |
finite_choice ~> finite_set_choice |
|
1090 |
eventually_conjI ~> eventually_conj |
|
1091 |
eventually_and ~> eventually_conj_iff |
|
1092 |
eventually_false ~> eventually_False |
|
1093 |
setsum_norm ~> norm_setsum |
|
1094 |
Lim_sequentially ~> LIMSEQ_def |
|
1095 |
Lim_ident_at ~> LIM_ident |
|
1096 |
Lim_const ~> tendsto_const |
|
1097 |
Lim_cmul ~> tendsto_scaleR [OF tendsto_const] |
|
1098 |
Lim_neg ~> tendsto_minus |
|
1099 |
Lim_add ~> tendsto_add |
|
1100 |
Lim_sub ~> tendsto_diff |
|
1101 |
Lim_mul ~> tendsto_scaleR |
|
1102 |
Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] |
|
1103 |
Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] |
|
1104 |
Lim_linear ~> bounded_linear.tendsto |
|
1105 |
Lim_component ~> tendsto_euclidean_component |
|
1106 |
Lim_component_cart ~> tendsto_vec_nth |
|
1107 |
Lim_inner ~> tendsto_inner [OF tendsto_const] |
|
1108 |
dot_lsum ~> inner_setsum_left |
|
1109 |
dot_rsum ~> inner_setsum_right |
|
1110 |
continuous_cmul ~> continuous_scaleR [OF continuous_const] |
|
1111 |
continuous_neg ~> continuous_minus |
|
1112 |
continuous_sub ~> continuous_diff |
|
1113 |
continuous_vmul ~> continuous_scaleR [OF _ continuous_const] |
|
1114 |
continuous_mul ~> continuous_scaleR |
|
1115 |
continuous_inv ~> continuous_inverse |
|
1116 |
continuous_at_within_inv ~> continuous_at_within_inverse |
|
1117 |
continuous_at_inv ~> continuous_at_inverse |
|
1118 |
continuous_at_norm ~> continuous_norm [OF continuous_at_id] |
|
1119 |
continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] |
|
1120 |
continuous_at_component ~> continuous_component [OF continuous_at_id] |
|
1121 |
continuous_on_neg ~> continuous_on_minus |
|
1122 |
continuous_on_sub ~> continuous_on_diff |
|
1123 |
continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] |
|
1124 |
continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] |
|
1125 |
continuous_on_mul ~> continuous_on_scaleR |
|
1126 |
continuous_on_mul_real ~> continuous_on_mult |
|
1127 |
continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] |
|
1128 |
continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] |
|
1129 |
continuous_on_inverse ~> continuous_on_inv |
|
1130 |
uniformly_continuous_on_neg ~> uniformly_continuous_on_minus |
|
1131 |
uniformly_continuous_on_sub ~> uniformly_continuous_on_diff |
|
1132 |
subset_interior ~> interior_mono |
|
1133 |
subset_closure ~> closure_mono |
|
1134 |
closure_univ ~> closure_UNIV |
|
1135 |
real_arch_lt ~> reals_Archimedean2 |
|
1136 |
real_arch ~> reals_Archimedean3 |
|
1137 |
real_abs_norm ~> abs_norm_cancel |
|
1138 |
real_abs_sub_norm ~> norm_triangle_ineq3 |
|
1139 |
norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 |
|
1140 |
||
1141 |
* Session HOL-Probability: |
|
1142 |
- Caratheodory's extension lemma is now proved for ring_of_sets. |
|
1143 |
- Infinite products of probability measures are now available. |
|
1144 |
- Sigma closure is independent, if the generator is independent |
|
1145 |
- Use extended reals instead of positive extended |
|
1146 |
reals. INCOMPATIBILITY. |
|
1147 |
||
45049 | 1148 |
* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY. |
1149 |
||
1150 |
expand_fun_below ~> fun_below_iff |
|
1151 |
below_fun_ext ~> fun_belowI |
|
1152 |
expand_cfun_eq ~> cfun_eq_iff |
|
1153 |
ext_cfun ~> cfun_eqI |
|
1154 |
expand_cfun_below ~> cfun_below_iff |
|
1155 |
below_cfun_ext ~> cfun_belowI |
|
1156 |
monofun_fun_fun ~> fun_belowD |
|
1157 |
monofun_fun_arg ~> monofunE |
|
1158 |
monofun_lub_fun ~> adm_monofun [THEN admD] |
|
1159 |
cont_lub_fun ~> adm_cont [THEN admD] |
|
1160 |
cont2cont_Rep_CFun ~> cont2cont_APP |
|
1161 |
cont_Rep_CFun_app ~> cont_APP_app |
|
1162 |
cont_Rep_CFun_app_app ~> cont_APP_app_app |
|
1163 |
cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE] |
|
1164 |
cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE] |
|
1165 |
contlub_cfun ~> lub_APP [symmetric] |
|
1166 |
contlub_LAM ~> lub_LAM [symmetric] |
|
1167 |
thelubI ~> lub_eqI |
|
1168 |
UU_I ~> bottomI |
|
1169 |
lift_distinct1 ~> lift.distinct(1) |
|
1170 |
lift_distinct2 ~> lift.distinct(2) |
|
1171 |
Def_not_UU ~> lift.distinct(2) |
|
1172 |
Def_inject ~> lift.inject |
|
1173 |
below_UU_iff ~> below_bottom_iff |
|
1174 |
eq_UU_iff ~> eq_bottom_iff |
|
1175 |
||
44903 | 1176 |
|
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
41667
diff
changeset
|
1177 |
*** Document preparation *** |
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
41667
diff
changeset
|
1178 |
|
44800 | 1179 |
* Antiquotation @{rail} layouts railroad syntax diagrams, see also |
1180 |
isar-ref manual, both for description and actual application of the |
|
1181 |
same. |
|
1182 |
||
1183 |
* Antiquotation @{value} evaluates the given term and presents its |
|
1184 |
result. |
|
1185 |
||
1186 |
* Antiquotations: term style "isub" provides ad-hoc conversion of |
|
1187 |
variables x1, y23 into subscripted form x\<^isub>1, |
|
1188 |
y\<^isub>2\<^isub>3. |
|
41651 | 1189 |
|
42484 | 1190 |
* Predefined LaTeX macros for Isabelle symbols \<bind> and \<then> |
1191 |
(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). |
|
1192 |
||
44967 | 1193 |
* Localized \isabellestyle switch can be used within blocks or groups |
1194 |
like this: |
|
1195 |
||
1196 |
\isabellestyle{it} %preferred default |
|
1197 |
{\isabellestylett @{text "typewriter stuff"}} |
|
1198 |
||
1199 |
* Discontinued special treatment of hard tabulators. Implicit |
|
1200 |
tab-width is now defined as 1. Potential INCOMPATIBILITY for visual |
|
1201 |
layouts. |
|
44800 | 1202 |
|
41651 | 1203 |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1204 |
*** ML *** |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1205 |
|
43731
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1206 |
* The inner syntax of sort/type/term/prop supports inlined YXML |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1207 |
representations within quoted string tokens. By encoding logical |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1208 |
entities via Term_XML (in ML or Scala) concrete syntax can be |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1209 |
bypassed, which is particularly useful for producing bits of text |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1210 |
under external program control. |
70072780e095
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents:
43709
diff
changeset
|
1211 |
|
43565 | 1212 |
* Antiquotations for ML and document preparation are managed as theory |
1213 |
data, which requires explicit setup. |
|
1214 |
||
42897 | 1215 |
* Isabelle_Process.is_active allows tools to check if the official |
1216 |
process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop |
|
1217 |
(better known as Proof General). |
|
1218 |
||
42360 | 1219 |
* Structure Proof_Context follows standard naming scheme. Old |
1220 |
ProofContext is still available for some time as legacy alias. |
|
1221 |
||
42015
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
1222 |
* Structure Timing provides various operations for timing; supersedes |
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
1223 |
former start_timing/end_timing etc. |
7b6e72a1b7dd
NEWS: structure Timing provides various operations for timing;
wenzelm
parents:
41999
diff
changeset
|
1224 |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1225 |
* Path.print is the official way to show file-system paths to users |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1226 |
(including quotes etc.). |
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1227 |
|
42056
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
1228 |
* Inner syntax: identifiers in parse trees of generic categories |
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
1229 |
"logic", "aprop", "idt" etc. carry position information (disguised as |
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
1230 |
type constraints). Occasional INCOMPATIBILITY with non-compliant |
42057
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1231 |
translations that choke on unexpected type constraints. Positions can |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1232 |
be stripped in ML translations via Syntax.strip_positions / |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1233 |
Syntax.strip_positions_ast, or via the syntax constant |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1234 |
"_strip_positions" within parse trees. As last resort, positions can |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1235 |
be disabled via the configuration option Syntax.positions, which is |
3eba96ff3d3e
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents:
42056
diff
changeset
|
1236 |
called "syntax_positions" in Isar attribute syntax. |
42056
160a630b2c7e
enable inner syntax source positions by default (controlled via configuration option);
wenzelm
parents:
42015
diff
changeset
|
1237 |
|
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
1238 |
* Discontinued special status of various ML structures that contribute |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
1239 |
to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
1240 |
pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
1241 |
refer directly to Ast.Constant, Lexicon.is_identifier, |
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42284
diff
changeset
|
1242 |
Syntax_Trans.mk_binder_tr etc. |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42180
diff
changeset
|
1243 |
|
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
1244 |
* Typed print translation: discontinued show_sorts argument, which is |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
1245 |
already available via context of "advanced" translation. |
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42239
diff
changeset
|
1246 |
|
42370 | 1247 |
* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic |
1248 |
goal states; body tactic needs to address all subgoals uniformly. |
|
1249 |
||
42403
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
1250 |
* Slightly more special eq_list/eq_set, with shortcut involving |
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
1251 |
pointer equality (assumes that eq relation is reflexive). |
38b29c9fc742
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;
wenzelm
parents:
42370
diff
changeset
|
1252 |
|
42793 | 1253 |
* Classical tactics use proper Proof.context instead of historic types |
1254 |
claset/clasimpset. Old-style declarations like addIs, addEs, addDs |
|
1255 |
operate directly on Proof.context. Raw type claset retains its use as |
|
1256 |
snapshot of the classical context, which can be recovered via |
|
1257 |
(put_claset HOL_cs) etc. Type clasimpset has been discontinued. |
|
1258 |
INCOMPATIBILITY, classical tactics and derived proof methods require |
|
1259 |
proper Proof.context. |
|
1260 |
||
44803 | 1261 |
|
1262 |
*** System *** |
|
1263 |
||
44968 | 1264 |
* Discontinued support for Poly/ML 5.2, which was the last version |
1265 |
without proper multithreading and TimeLimit implementation. |
|
1266 |
||
1267 |
* Discontinued old lib/scripts/polyml-platform, which has been |
|
1268 |
obsolete since Isabelle2009-2. |
|
1269 |
||
44967 | 1270 |
* Various optional external tools are referenced more robustly and |
1271 |
uniformly by explicit Isabelle settings as follows: |
|
1272 |
||
1273 |
ISABELLE_CSDP (formerly CSDP_EXE) |
|
1274 |
ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) |
|
1275 |
ISABELLE_OCAML (formerly EXEC_OCAML) |
|
1276 |
ISABELLE_SWIPL (formerly EXEC_SWIPL) |
|
1277 |
ISABELLE_YAP (formerly EXEC_YAP) |
|
1278 |
||
1279 |
Note that automated detection from the file-system or search path has |
|
1280 |
been discontinued. INCOMPATIBILITY. |
|
1281 |
||
43752 | 1282 |
* Scala layer provides JVM method invocation service for static |
44800 | 1283 |
methods of type (String)String, see Invoke_Scala.method in ML. For |
1284 |
example: |
|
43752 | 1285 |
|
1286 |
Invoke_Scala.method "java.lang.System.getProperty" "java.home" |
|
1287 |
||
44967 | 1288 |
Together with YXML.string_of_body/parse_body and XML.Encode/Decode |
1289 |
this allows to pass structured values between ML and Scala. |
|
44800 | 1290 |
|
44803 | 1291 |
* The IsabelleText fonts includes some further glyphs to support the |
1292 |
Prover IDE. Potential INCOMPATIBILITY: users who happen to have |
|
1293 |
installed a local copy (which is normally *not* required) need to |
|
1294 |
delete or update it from ~~/lib/fonts/. |
|
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
1295 |
|
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
41685
diff
changeset
|
1296 |
|
45089 | 1297 |
|
41512 | 1298 |
New in Isabelle2011 (January 2011) |
1299 |
---------------------------------- |
|
37383 | 1300 |
|
37536
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1301 |
*** General *** |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1302 |
|
41573 | 1303 |
* Experimental Prover IDE based on Isabelle/Scala and jEdit (see |
41612 | 1304 |
src/Tools/jEdit). This also serves as IDE for Isabelle/ML, with |
1305 |
useful tooltips and hyperlinks produced from its static analysis. The |
|
1306 |
bundled component provides an executable Isabelle tool that can be run |
|
1307 |
like this: |
|
1308 |
||
1309 |
Isabelle2011/bin/isabelle jedit |
|
41573 | 1310 |
|
40948 | 1311 |
* Significantly improved Isabelle/Isar implementation manual. |
1312 |
||
41594 | 1313 |
* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER |
41595 | 1314 |
(and thus refers to something like $HOME/.isabelle/Isabelle2011), |
41594 | 1315 |
while the default heap location within that directory lacks that extra |
1316 |
suffix. This isolates multiple Isabelle installations from each |
|
1317 |
other, avoiding problems with old settings in new versions. |
|
1318 |
INCOMPATIBILITY, need to copy/upgrade old user settings manually. |
|
1319 |
||
40947 | 1320 |
* Source files are always encoded as UTF-8, instead of old-fashioned |
1321 |
ISO-Latin-1. INCOMPATIBILITY. Isabelle LaTeX documents might require |
|
40948 | 1322 |
the following package declarations: |
40947 | 1323 |
|
1324 |
\usepackage[utf8]{inputenc} |
|
1325 |
\usepackage{textcomp} |
|
1326 |
||
41440 | 1327 |
* Explicit treatment of UTF-8 sequences as Isabelle symbols, such that |
37536
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1328 |
a Unicode character is treated as a single symbol, not a sequence of |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1329 |
non-ASCII bytes as before. Since Isabelle/ML string literals may |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1330 |
contain symbols without further backslash escapes, Unicode can now be |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1331 |
used here as well. Recall that Symbol.explode in ML provides a |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1332 |
consistent view on symbols, while raw explode (or String.explode) |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1333 |
merely give a byte-oriented representation. |
c62aa9281101
explicit treatment of UTF8 sequences as Isabelle symbols;
wenzelm
parents:
37484
diff
changeset
|
1334 |
|
41594 | 1335 |
* Theory loader: source files are primarily located via the master |
1336 |
directory of each theory node (where the .thy file itself resides). |
|
1337 |
The global load path is still partially available as legacy feature. |
|
1338 |
Minor INCOMPATIBILITY due to subtle change in file lookup: use |
|
1339 |
explicit paths, relatively to the theory. |
|
38135
2b9bfa0b44f1
theory loading: only the master source file is looked-up in the implicit load path;
wenzelm
parents:
38110
diff
changeset
|
1340 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
1341 |
* Special treatment of ML file names has been discontinued. |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
1342 |
Historically, optional extensions .ML or .sml were added on demand -- |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
1343 |
at the cost of clarity of file dependencies. Recall that Isabelle/ML |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
1344 |
files exclusively use the .ML extension. Minor INCOMPATIBILTY. |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37868
diff
changeset
|
1345 |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38864
diff
changeset
|
1346 |
* Various options that affect pretty printing etc. are now properly |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
1347 |
handled within the context via configuration options, instead of |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
1348 |
unsynchronized references or print modes. There are both ML Config.T |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
1349 |
entities and Isar declaration attributes to access these. |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
1350 |
|
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1351 |
ML (Config.T) Isar (attribute) |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1352 |
|
39128
93a7365fb4ee
turned eta_contract into proper configuration option;
wenzelm
parents:
39126
diff
changeset
|
1353 |
eta_contract eta_contract |
39137
ccb53edd59f0
turned show_brackets into proper configuration option;
wenzelm
parents:
39134
diff
changeset
|
1354 |
show_brackets show_brackets |
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39128
diff
changeset
|
1355 |
show_sorts show_sorts |
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39128
diff
changeset
|
1356 |
show_types show_types |
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1357 |
show_question_marks show_question_marks |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1358 |
show_consts show_consts |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
1359 |
show_abbrevs show_abbrevs |
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1360 |
|
41379 | 1361 |
Syntax.ast_trace syntax_ast_trace |
1362 |
Syntax.ast_stat syntax_ast_stat |
|
39126
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1363 |
Syntax.ambiguity_level syntax_ambiguity_level |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1364 |
|
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1365 |
Goal_Display.goals_limit goals_limit |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1366 |
Goal_Display.show_main_goal show_main_goal |
ee117c5b3b75
configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;
wenzelm
parents:
39125
diff
changeset
|
1367 |
|
41379 | 1368 |
Method.rule_trace rule_trace |
1369 |
||
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1370 |
Thy_Output.display thy_output_display |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1371 |
Thy_Output.quotes thy_output_quotes |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1372 |
Thy_Output.indent thy_output_indent |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1373 |
Thy_Output.source thy_output_source |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1374 |
Thy_Output.break thy_output_break |
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
39105
diff
changeset
|
1375 |
|
41440 | 1376 |
Note that corresponding "..._default" references in ML may only be |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
1377 |
changed globally at the ROOT session setup, but *not* within a theory. |
40879
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
1378 |
The option "show_abbrevs" supersedes the former print mode |
ca132ef44944
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
wenzelm
parents:
40878
diff
changeset
|
1379 |
"no_abbrevs" with inverted meaning. |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
38708
diff
changeset
|
1380 |
|
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
1381 |
* More systematic naming of some configuration options. |
41294 | 1382 |
INCOMPATIBILITY. |
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
1383 |
|
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
1384 |
trace_simp ~> simp_trace |
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
1385 |
debug_simp ~> simp_debug |
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
40866
diff
changeset
|
1386 |
|
40291 | 1387 |
* Support for real valued configuration options, using simplistic |
1388 |
floating-point notation that coincides with the inner syntax for |
|
1389 |
float_token. |
|
1390 |
||
41594 | 1391 |
* Support for real valued preferences (with approximative PGIP type): |
1392 |
front-ends need to accept "pgint" values in float notation. |
|