author | wenzelm |
Sat, 13 Mar 2010 20:33:14 +0100 | |
changeset 35765 | 09e238561460 |
parent 35763 | 765f8adf10f9 |
child 35810 | a50237ec0ecd |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
33993 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
35260 | 7 |
*** General *** |
8 |
||
35436 | 9 |
* Authentic syntax for *all* logical entities (type classes, type |
10 |
constructors, term constants): provides simple and robust |
|
11 |
correspondence between formal entities and concrete syntax. Within |
|
12 |
the parse tree / AST representations, "constants" are decorated by |
|
13 |
their category (class, type, const) and spelled out explicitly with |
|
14 |
their full internal name. |
|
15 |
||
16 |
Substantial INCOMPATIBILITY concerning low-level syntax declarations |
|
17 |
and translations (translation rules and translation functions in ML). |
|
18 |
Some hints on upgrading: |
|
35260 | 19 |
|
20 |
- Many existing uses of 'syntax' and 'translations' can be replaced |
|
35436 | 21 |
by more modern 'type_notation', 'notation' and 'abbreviation', |
22 |
which are independent of this issue. |
|
35260 | 23 |
|
24 |
- 'translations' require markup within the AST; the term syntax |
|
25 |
provides the following special forms: |
|
26 |
||
27 |
CONST c -- produces syntax version of constant c from context |
|
35261 | 28 |
XCONST c -- literally c, checked as constant from context |
29 |
c -- literally c, if declared by 'syntax' |
|
30 |
||
31 |
Plain identifiers are treated as AST variables -- occasionally the |
|
32 |
system indicates accidental variables via the error "rhs contains |
|
33 |
extra variables". |
|
35260 | 34 |
|
35436 | 35 |
Type classes and type constructors are marked according to their |
36 |
concrete syntax. Some old translations rules need to be written |
|
37 |
for the "type" category, using type constructor application |
|
38 |
instead of pseudo-term application of the default category |
|
39 |
"logic". |
|
40 |
||
35260 | 41 |
- 'parse_translation' etc. in ML may use the following |
42 |
antiquotations: |
|
43 |
||
35436 | 44 |
@{class_syntax c} -- type class c within parse tree / AST |
45 |
@{term_syntax c} -- type constructor c within parse tree / AST |
|
35260 | 46 |
@{const_syntax c} -- ML version of "CONST c" above |
47 |
@{syntax_const c} -- literally c (checked wrt. 'syntax' declarations) |
|
48 |
||
35436 | 49 |
- Literal types within 'typed_print_translations', i.e. those *not* |
50 |
represented as pseudo-terms are represented verbatim. Use @{class |
|
51 |
c} or @{type_name c} here instead of the above syntax |
|
52 |
antiquotations. |
|
53 |
||
35260 | 54 |
Note that old non-authentic syntax was based on unqualified base |
35436 | 55 |
names, so all of the above "constant" names would coincide. Recall |
56 |
that 'print_syntax' and ML_command "set Syntax.trace_ast" help to |
|
57 |
diagnose syntax problems. |
|
35260 | 58 |
|
35351
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35306
diff
changeset
|
59 |
* Type constructors admit general mixfix syntax, not just infix. |
7425aece4ee3
allow general mixfix syntax for type constructors;
wenzelm
parents:
35306
diff
changeset
|
60 |
|
35613 | 61 |
* Use of cumulative prems via "!" in some proof methods has been |
62 |
discontinued (legacy feature). |
|
63 |
||
35260 | 64 |
|
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
65 |
*** Pure *** |
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
66 |
|
35765
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
67 |
* Local theory specifications may depend on extra type variables that |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
68 |
are not present in the result type -- arguments TYPE('a) :: 'a itself |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
69 |
are added internally. For example: |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
70 |
|
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
71 |
definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)" |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
72 |
|
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
73 |
* Code generator: details of internal data cache have no impact on |
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
74 |
the user space functionality any longer. |
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
75 |
|
35129 | 76 |
* Discontinued unnamed infix syntax (legacy feature for many years) -- |
35130 | 77 |
need to specify constant name and syntax separately. Internal ML |
78 |
datatype constructors have been renamed from InfixName to Infix etc. |
|
79 |
Minor INCOMPATIBILITY. |
|
35129 | 80 |
|
35413 | 81 |
* Commands 'type_notation' and 'no_type_notation' declare type syntax |
82 |
within a local theory context, with explicit checking of the |
|
83 |
constructors involved (in contrast to the raw 'syntax' versions). |
|
84 |
||
35681 | 85 |
* Command 'typedecl' now works within a local theory context -- |
86 |
without introducing dependencies on parameters or assumptions, which |
|
87 |
is not possible in Isabelle/Pure. |
|
88 |
||
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
89 |
|
33993 | 90 |
*** HOL *** |
91 |
||
35745
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
92 |
* Command 'typedef' now works within a local theory context -- without |
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
93 |
introducing dependencies on parameters or assumptions, which is not |
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
94 |
possible in Isabelle/Pure/HOL. Note that the logical environment may |
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
95 |
contain multiple interpretations of local typedefs (with different |
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
96 |
non-emptiness proofs), even in a global theory context. |
1416f568b2b6
command 'typedef' now works within a local theory context;
wenzelm
parents:
35728
diff
changeset
|
97 |
|
35763
765f8adf10f9
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents:
35745
diff
changeset
|
98 |
* Theory Library/Coinductive_List has been removed -- superceded by |
765f8adf10f9
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents:
35745
diff
changeset
|
99 |
AFP/thys/Coinductive. |
765f8adf10f9
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents:
35745
diff
changeset
|
100 |
|
35728 | 101 |
* Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, |
102 |
Min, Max from theory Finite_Set. INCOMPATIBILITY. |
|
103 |
||
35372 | 104 |
* Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. |
105 |
INCOMPATIBILITY. |
|
106 |
||
35042 | 107 |
* New set of rules "ac_simps" provides combined assoc / commute rewrites |
108 |
for all interpretations of the appropriate generic locales. |
|
109 |
||
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
110 |
* Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field" |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
111 |
into theories "Rings" and "Fields"; for more appropriate and more |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
112 |
consistent names suitable for name prefixes within the HOL theories. |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
113 |
INCOMPATIBILITY. |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
114 |
|
35084 | 115 |
* Some generic constants have been put to appropriate theories: |
116 |
||
35093 | 117 |
less_eq, less: Orderings |
35264 | 118 |
zero, one, plus, minus, uminus, times, abs, sgn: Groups |
35084 | 119 |
inverse, divide: Rings |
120 |
||
121 |
INCOMPATIBILITY. |
|
122 |
||
35721 | 123 |
* Class division_ring also requires proof of fact divide_inverse. However instantiation |
35084 | 124 |
of parameter divide has also been required previously. INCOMPATIBILITY. |
125 |
||
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
126 |
* More consistent naming of type classes involving orderings (and lattices): |
35027
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
127 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
128 |
lower_semilattice ~> semilattice_inf |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
129 |
upper_semilattice ~> semilattice_sup |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
130 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
131 |
dense_linear_order ~> dense_linorder |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
132 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
133 |
pordered_ab_group_add ~> ordered_ab_group_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
134 |
pordered_ab_group_add_abs ~> ordered_ab_group_add_abs |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
135 |
pordered_ab_semigroup_add ~> ordered_ab_semigroup_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
136 |
pordered_ab_semigroup_add_imp_le ~> ordered_ab_semigroup_add_imp_le |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
137 |
pordered_cancel_ab_semigroup_add ~> ordered_cancel_ab_semigroup_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
138 |
pordered_cancel_comm_semiring ~> ordered_cancel_comm_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
139 |
pordered_cancel_semiring ~> ordered_cancel_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
140 |
pordered_comm_monoid_add ~> ordered_comm_monoid_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
141 |
pordered_comm_ring ~> ordered_comm_ring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
142 |
pordered_comm_semiring ~> ordered_comm_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
143 |
pordered_ring ~> ordered_ring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
144 |
pordered_ring_abs ~> ordered_ring_abs |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
145 |
pordered_semiring ~> ordered_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
146 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
147 |
ordered_ab_group_add ~> linordered_ab_group_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
148 |
ordered_ab_semigroup_add ~> linordered_ab_semigroup_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
149 |
ordered_cancel_ab_semigroup_add ~> linordered_cancel_ab_semigroup_add |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
150 |
ordered_comm_semiring_strict ~> linordered_comm_semiring_strict |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
151 |
ordered_field ~> linordered_field |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
152 |
ordered_field_no_lb ~> linordered_field_no_lb |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
153 |
ordered_field_no_ub ~> linordered_field_no_ub |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
154 |
ordered_field_dense_linear_order ~> dense_linordered_field |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
155 |
ordered_idom ~> linordered_idom |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
156 |
ordered_ring ~> linordered_ring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
157 |
ordered_ring_le_cancel_factor ~> linordered_ring_le_cancel_factor |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
158 |
ordered_ring_less_cancel_factor ~> linordered_ring_less_cancel_factor |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
159 |
ordered_ring_strict ~> linordered_ring_strict |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
160 |
ordered_semidom ~> linordered_semidom |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
161 |
ordered_semiring ~> linordered_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
162 |
ordered_semiring_1 ~> linordered_semiring_1 |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
163 |
ordered_semiring_1_strict ~> linordered_semiring_1_strict |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
164 |
ordered_semiring_strict ~> linordered_semiring_strict |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
165 |
|
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
166 |
The following slightly odd type classes have been moved to |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
167 |
a separate theory Library/Lattice_Algebras.thy: |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
168 |
|
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
169 |
lordered_ab_group_add ~> lattice_ab_group_add |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
170 |
lordered_ab_group_add_abs ~> lattice_ab_group_add_abs |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
171 |
lordered_ab_group_add_meet ~> semilattice_inf_ab_group_add |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
172 |
lordered_ab_group_add_join ~> semilattice_sup_ab_group_add |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
173 |
lordered_ring ~> lattice_ring |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
174 |
|
35027
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
175 |
INCOMPATIBILITY. |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
176 |
|
34962
807f6ce0273d
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents:
34946
diff
changeset
|
177 |
* HOLogic.strip_psplit: types are returned in syntactic order, similar |
807f6ce0273d
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents:
34946
diff
changeset
|
178 |
to other strip and tuple operations. INCOMPATIBILITY. |
807f6ce0273d
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents:
34946
diff
changeset
|
179 |
|
34946 | 180 |
* Various old-style primrec specifications in the HOL theories have been |
181 |
replaced by new-style primrec, especially in theory List. The corresponding |
|
182 |
constants now have authentic syntax. INCOMPATIBILITY. |
|
183 |
||
35276 | 184 |
* Reorganized theory Multiset: swapped notation of pointwise and multiset order: |
185 |
* pointwise ordering is instance of class order with standard syntax <= and <; |
|
186 |
* multiset ordering has syntax <=# and <#; partial order properties are provided |
|
187 |
by means of interpretation with prefix multiset_order. |
|
188 |
Less duplication, less historical organization of sections, |
|
35270 | 189 |
conversion from associations lists to multisets, rudimentary code generation. |
190 |
Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed. |
|
191 |
INCOMPATIBILITY. |
|
34946 | 192 |
|
35009 | 193 |
* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax. |
194 |
INCOMPATIBILITY. |
|
33993 | 195 |
|
196 |
* Code generation: ML and OCaml code is decorated with signatures. |
|
197 |
||
35009 | 198 |
* Theory Complete_Lattice: lemmas top_def and bot_def have been |
199 |
replaced by the more convenient lemmas Inf_empty and Sup_empty. |
|
200 |
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed |
|
201 |
by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace |
|
202 |
former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right |
|
203 |
subsume inf_top and sup_bot respectively. INCOMPATIBILITY. |
|
204 |
||
205 |
* Theory Finite_Set and List: some lemmas have been generalized from |
|
34076
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
206 |
sets to lattices: |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
207 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
208 |
fun_left_comm_idem_inter ~> fun_left_comm_idem_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
209 |
fun_left_comm_idem_union ~> fun_left_comm_idem_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
210 |
inter_Inter_fold_inter ~> inf_Inf_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
211 |
union_Union_fold_union ~> sup_Sup_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
212 |
Inter_fold_inter ~> Inf_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
213 |
Union_fold_union ~> Sup_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
214 |
inter_INTER_fold_inter ~> inf_INFI_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
215 |
union_UNION_fold_union ~> sup_SUPR_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
216 |
INTER_fold_inter ~> INFI_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
217 |
UNION_fold_union ~> SUPR_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
218 |
|
35009 | 219 |
* Theory List: added transpose. |
220 |
||
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
35093
diff
changeset
|
221 |
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid |
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
35093
diff
changeset
|
222 |
clash with new theory Quotient in Main HOL. |
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
35093
diff
changeset
|
223 |
|
33993 | 224 |
|
225 |
*** ML *** |
|
226 |
||
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
227 |
* Antiquotations for basic formal entities: |
35396 | 228 |
|
229 |
@{class NAME} -- type class |
|
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
230 |
@{class_syntax NAME} -- syntax representation of the above |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
231 |
|
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
232 |
@{type_name NAME} -- logical type |
35361
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35351
diff
changeset
|
233 |
@{type_abbrev NAME} -- type abbreviation |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35351
diff
changeset
|
234 |
@{nonterminal NAME} -- type of concrete syntactic category |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35351
diff
changeset
|
235 |
@{type_syntax NAME} -- syntax representation of any of the above |
4c7c849b70aa
more orthogonal antiquotations for type constructors;
wenzelm
parents:
35351
diff
changeset
|
236 |
|
35401
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
237 |
@{const_name NAME} -- logical constant (INCOMPATIBILITY) |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
238 |
@{const_abbrev NAME} -- abbreviated constant |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
239 |
@{const_syntax NAME} -- syntax representation of any of the above |
bfcbab8592ba
clarified @{const_name} (only logical consts) vs. @{const_abbrev};
wenzelm
parents:
35396
diff
changeset
|
240 |
|
35111 | 241 |
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw |
242 |
syntax constant (cf. 'syntax' command). |
|
243 |
||
35021
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35009
diff
changeset
|
244 |
* Renamed old-style Drule.standard to Drule.export_without_context, to |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35009
diff
changeset
|
245 |
emphasize that this is in no way a standard operation. |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35009
diff
changeset
|
246 |
INCOMPATIBILITY. |
c839a4c670c6
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
35009
diff
changeset
|
247 |
|
34076
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
248 |
* Curried take and drop in library.ML; negative length is interpreted |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
249 |
as infinity (as in chop). INCOMPATIBILITY. |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
250 |
|
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
251 |
* Subgoal.FOCUS (and variants): resulting goal state is normalized as |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
252 |
usual for resolution. Rare INCOMPATIBILITY. |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
253 |
|
34259
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents:
34255
diff
changeset
|
254 |
* Discontinued old TheoryDataFun with its copy/init operation -- data |
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents:
34255
diff
changeset
|
255 |
needs to be pure. Functor Theory_Data_PP retains the traditional |
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents:
34255
diff
changeset
|
256 |
Pretty.pp argument to merge, which is absent in the standard |
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents:
34255
diff
changeset
|
257 |
Theory_Data version. |
2ba492b8b6e8
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
wenzelm
parents:
34255
diff
changeset
|
258 |
|
33993 | 259 |
|
34238 | 260 |
*** System *** |
261 |
||
262 |
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
|
263 |
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that |
|
264 |
proof terms are enabled unconditionally in the new HOL-Proofs image. |
|
265 |
||
34255
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
266 |
* Discontinued old ISABELLE and ISATOOL environment settings (legacy |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
267 |
feature since Isabelle2009). Use ISABELLE_PROCESS and ISABELLE_TOOL, |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
268 |
respectively. |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
269 |
|
34238 | 270 |
|
33993 | 271 |
|
33842 | 272 |
New in Isabelle2009-1 (December 2009) |
273 |
------------------------------------- |
|
30904 | 274 |
|
31547 | 275 |
*** General *** |
276 |
||
277 |
* Discontinued old form of "escaped symbols" such as \\<forall>. Only |
|
278 |
one backslash should be used, even in ML sources. |
|
279 |
||
280 |
||
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
281 |
*** Pure *** |
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
282 |
|
32846
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
283 |
* Locale interpretation propagates mixins along the locale hierarchy. |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
284 |
The currently only available mixins are the equations used to map |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
285 |
local definitions to terms of the target domain of an interpretation. |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
286 |
|
33842 | 287 |
* Reactivated diagnostic command 'print_interps'. Use "print_interps |
288 |
loc" to print all interpretations of locale "loc" in the theory. |
|
289 |
Interpretations in proofs are not shown. |
|
32846
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
290 |
|
32983 | 291 |
* Thoroughly revised locales tutorial. New section on conditional |
292 |
interpretation. |
|
293 |
||
33843 | 294 |
* On instantiation of classes, remaining undefined class parameters |
295 |
are formally declared. INCOMPATIBILITY. |
|
296 |
||
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
297 |
|
33842 | 298 |
*** Document preparation *** |
299 |
||
300 |
* New generalized style concept for printing terms: @{foo (style) ...} |
|
301 |
instead of @{foo_style style ...} (old form is still retained for |
|
302 |
backward compatibility). Styles can be also applied for |
|
303 |
antiquotations prop, term_type and typeof. |
|
32891 | 304 |
|
305 |
||
30930 | 306 |
*** HOL *** |
307 |
||
33842 | 308 |
* New proof method "smt" for a combination of first-order logic with |
309 |
equality, linear and nonlinear (natural/integer/real) arithmetic, and |
|
310 |
fixed-size bitvectors; there is also basic support for higher-order |
|
311 |
features (esp. lambda abstractions). It is an incomplete decision |
|
312 |
procedure based on external SMT solvers using the oracle mechanism; |
|
313 |
for the SMT solver Z3, this method is proof-producing. Certificates |
|
314 |
are provided to avoid calling the external solvers solely for |
|
315 |
re-checking proofs. Due to a remote SMT service there is no need for |
|
316 |
installing SMT solvers locally. See src/HOL/SMT. |
|
317 |
||
318 |
* New commands to load and prove verification conditions generated by |
|
319 |
the Boogie program verifier or derived systems (e.g. the Verifying C |
|
320 |
Compiler (VCC) or Spec#). See src/HOL/Boogie. |
|
321 |
||
322 |
* New counterexample generator tool 'nitpick' based on the Kodkod |
|
323 |
relational model finder. See src/HOL/Tools/Nitpick and |
|
324 |
src/HOL/Nitpick_Examples. |
|
325 |
||
33860 | 326 |
* New commands 'code_pred' and 'values' to invoke the predicate |
327 |
compiler and to enumerate values of inductive predicates. |
|
328 |
||
329 |
* A tabled implementation of the reflexive transitive closure. |
|
330 |
||
331 |
* New implementation of quickcheck uses generic code generator; |
|
332 |
default generators are provided for all suitable HOL types, records |
|
333 |
and datatypes. Old quickcheck can be re-activated importing theory |
|
334 |
Library/SML_Quickcheck. |
|
335 |
||
33843 | 336 |
* New testing tool Mirabelle for automated proof tools. Applies |
337 |
several tools and tactics like sledgehammer, metis, or quickcheck, to |
|
338 |
every proof step in a theory. To be used in batch mode via the |
|
339 |
"mirabelle" utility. |
|
340 |
||
341 |
* New proof method "sos" (sum of squares) for nonlinear real |
|
342 |
arithmetic (originally due to John Harison). It requires theory |
|
343 |
Library/Sum_Of_Squares. It is not a complete decision procedure but |
|
344 |
works well in practice on quantifier-free real arithmetic with +, -, |
|
345 |
*, ^, =, <= and <, i.e. boolean combinations of equalities and |
|
346 |
inequalities between polynomials. It makes use of external |
|
347 |
semidefinite programming solvers. Method "sos" generates a |
|
348 |
certificate that can be pasted into the proof thus avoiding the need |
|
349 |
to call an external tool every time the proof is checked. See |
|
350 |
src/HOL/Library/Sum_Of_Squares. |
|
351 |
||
352 |
* New method "linarith" invokes existing linear arithmetic decision |
|
353 |
procedure only. |
|
354 |
||
355 |
* New command 'atp_minimal' reduces result produced by Sledgehammer. |
|
356 |
||
357 |
* New Sledgehammer option "Full Types" in Proof General settings menu. |
|
358 |
Causes full type information to be output to the ATPs. This slows |
|
359 |
ATPs down considerably but eliminates a source of unsound "proofs" |
|
360 |
that fail later. |
|
361 |
||
362 |
* New method "metisFT": A version of metis that uses full type |
|
363 |
information in order to avoid failures of proof reconstruction. |
|
364 |
||
365 |
* New evaluator "approximate" approximates an real valued term using |
|
366 |
the same method as the approximation method. |
|
367 |
||
368 |
* Method "approximate" now supports arithmetic expressions as |
|
369 |
boundaries of intervals and implements interval splitting and Taylor |
|
370 |
series expansion. |
|
371 |
||
372 |
* ML antiquotation @{code_datatype} inserts definition of a datatype |
|
373 |
generated by the code generator; e.g. see src/HOL/Predicate.thy. |
|
374 |
||
33860 | 375 |
* New theory SupInf of the supremum and infimum operators for sets of |
376 |
reals. |
|
377 |
||
378 |
* New theory Probability, which contains a development of measure |
|
379 |
theory, eventually leading to Lebesgue integration and probability. |
|
380 |
||
381 |
* Extended Multivariate Analysis to include derivation and Brouwer's |
|
382 |
fixpoint theorem. |
|
33843 | 383 |
|
33842 | 384 |
* Reorganization of number theory, INCOMPATIBILITY: |
33873 | 385 |
- new number theory development for nat and int, in theories Divides |
386 |
and GCD as well as in new session Number_Theory |
|
387 |
- some constants and facts now suffixed with _nat and _int |
|
388 |
accordingly |
|
389 |
- former session NumberTheory now named Old_Number_Theory, including |
|
390 |
theories Legacy_GCD and Primes (prefer Number_Theory if possible) |
|
33842 | 391 |
- moved theory Pocklington from src/HOL/Library to |
392 |
src/HOL/Old_Number_Theory |
|
32479 | 393 |
|
33873 | 394 |
* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and |
395 |
lcm of finite and infinite sets. It is shown that they form a complete |
|
32600 | 396 |
lattice. |
397 |
||
398 |
* Class semiring_div requires superclass no_zero_divisors and proof of |
|
399 |
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
|
400 |
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
|
401 |
generalized to class semiring_div, subsuming former theorems |
|
402 |
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and |
|
403 |
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. |
|
404 |
INCOMPATIBILITY. |
|
405 |
||
32588
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
406 |
* Refinements to lattice classes and sets: |
32064 | 407 |
- less default intro/elim rules in locale variant, more default |
408 |
intro/elim rules in class variant: more uniformity |
|
33842 | 409 |
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with |
410 |
le_inf_iff |
|
411 |
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and |
|
412 |
sup_aci) |
|
32064 | 413 |
- renamed ACI to inf_sup_aci |
32600 | 414 |
- new class "boolean_algebra" |
33842 | 415 |
- class "complete_lattice" moved to separate theory |
33860 | 416 |
"Complete_Lattice"; corresponding constants (and abbreviations) |
33842 | 417 |
renamed and with authentic syntax: |
33860 | 418 |
Set.Inf ~> Complete_Lattice.Inf |
419 |
Set.Sup ~> Complete_Lattice.Sup |
|
420 |
Set.INFI ~> Complete_Lattice.INFI |
|
421 |
Set.SUPR ~> Complete_Lattice.SUPR |
|
422 |
Set.Inter ~> Complete_Lattice.Inter |
|
423 |
Set.Union ~> Complete_Lattice.Union |
|
424 |
Set.INTER ~> Complete_Lattice.INTER |
|
425 |
Set.UNION ~> Complete_Lattice.UNION |
|
32600 | 426 |
- authentic syntax for |
427 |
Set.Pow |
|
428 |
Set.image |
|
32588
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
429 |
- mere abbreviations: |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
430 |
Set.empty (for bot) |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
431 |
Set.UNIV (for top) |
33860 | 432 |
Set.inter (for inf, formerly Set.Int) |
433 |
Set.union (for sup, formerly Set.Un) |
|
32588
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
434 |
Complete_Lattice.Inter (for Inf) |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
435 |
Complete_Lattice.Union (for Sup) |
32606
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32600
diff
changeset
|
436 |
Complete_Lattice.INTER (for INFI) |
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32600
diff
changeset
|
437 |
Complete_Lattice.UNION (for SUPR) |
32600 | 438 |
- object-logic definitions as far as appropriate |
32217 | 439 |
|
32691 | 440 |
INCOMPATIBILITY. Care is required when theorems Int_subset_iff or |
33842 | 441 |
Un_subset_iff are explicitly deleted as default simp rules; then also |
442 |
their lattice counterparts le_inf_iff and le_sup_iff have to be |
|
32691 | 443 |
deleted to achieve the desired effect. |
32064 | 444 |
|
33842 | 445 |
* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp |
446 |
rules by default any longer; the same applies to min_max.inf_absorb1 |
|
447 |
etc. INCOMPATIBILITY. |
|
448 |
||
449 |
* Rules sup_Int_eq and sup_Un_eq are no longer declared as |
|
450 |
pred_set_conv by default. INCOMPATIBILITY. |
|
451 |
||
452 |
* Power operations on relations and functions are now one dedicated |
|
32706 | 453 |
constant "compow" with infix syntax "^^". Power operation on |
31547 | 454 |
multiplicative monoids retains syntax "^" and is now defined generic |
455 |
in class power. INCOMPATIBILITY. |
|
456 |
||
33842 | 457 |
* Relation composition "R O S" now has a more standard argument order: |
458 |
"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}". INCOMPATIBILITY, |
|
459 |
rewrite propositions with "S O R" --> "R O S". Proofs may occasionally |
|
460 |
break, since the O_assoc rule was not rewritten like this. Fix using |
|
461 |
O_assoc[symmetric]. The same applies to the curried version "R OO S". |
|
32427 | 462 |
|
33057 | 463 |
* Function "Inv" is renamed to "inv_into" and function "inv" is now an |
33842 | 464 |
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. |
32988 | 465 |
INCOMPATIBILITY. |
466 |
||
33860 | 467 |
* Most rules produced by inductive and datatype package have mandatory |
468 |
prefixes. INCOMPATIBILITY. |
|
31790 | 469 |
|
33842 | 470 |
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by |
471 |
the attribute of the same name. Each of the theorems in the list |
|
472 |
DERIV_intros assumes composition with an additional function and |
|
473 |
matches a variable to the derivative, which has to be solved by the |
|
474 |
Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative |
|
33873 | 475 |
of most elementary terms. Former Maclauren.DERIV_tac and |
476 |
Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros). |
|
477 |
INCOMPATIBILITY. |
|
33860 | 478 |
|
479 |
* Code generator attributes follow the usual underscore convention: |
|
480 |
code_unfold replaces code unfold |
|
481 |
code_post replaces code post |
|
482 |
etc. |
|
483 |
INCOMPATIBILITY. |
|
31900 | 484 |
|
33471 | 485 |
* Renamed methods: |
486 |
sizechange -> size_change |
|
487 |
induct_scheme -> induction_schema |
|
33860 | 488 |
INCOMPATIBILITY. |
33673 | 489 |
|
33843 | 490 |
* Discontinued abbreviation "arbitrary" of constant "undefined". |
491 |
INCOMPATIBILITY, use "undefined" directly. |
|
492 |
||
33860 | 493 |
* Renamed theorems: |
494 |
Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
|
495 |
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
|
496 |
Suc_plus1 -> Suc_eq_plus1 |
|
497 |
*anti_sym -> *antisym* |
|
498 |
vector_less_eq_def -> vector_le_def |
|
499 |
INCOMPATIBILITY. |
|
500 |
||
501 |
* Added theorem List.map_map as [simp]. Removed List.map_compose. |
|
502 |
INCOMPATIBILITY. |
|
503 |
||
504 |
* Removed predicate "M hassize n" (<--> card M = n & finite M). |
|
505 |
INCOMPATIBILITY. |
|
506 |
||
31812 | 507 |
|
33825 | 508 |
*** HOLCF *** |
509 |
||
33842 | 510 |
* Theory Representable defines a class "rep" of domains that are |
511 |
representable (via an ep-pair) in the universal domain type "udom". |
|
33825 | 512 |
Instances are provided for all type constructors defined in HOLCF. |
513 |
||
514 |
* The 'new_domain' command is a purely definitional version of the |
|
515 |
domain package, for representable domains. Syntax is identical to the |
|
516 |
old domain package. The 'new_domain' package also supports indirect |
|
517 |
recursion using previously-defined type constructors. See |
|
33842 | 518 |
src/HOLCF/ex/New_Domain.thy for examples. |
519 |
||
520 |
* Method "fixrec_simp" unfolds one step of a fixrec-defined constant |
|
33825 | 521 |
on the left-hand side of an equation, and then performs |
522 |
simplification. Rewriting is done using rules declared with the |
|
33842 | 523 |
"fixrec_simp" attribute. The "fixrec_simp" method is intended as a |
524 |
replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples. |
|
33825 | 525 |
|
526 |
* The pattern-match compiler in 'fixrec' can now handle constructors |
|
527 |
with HOL function types. Pattern-match combinators for the Pair |
|
528 |
constructor are pre-configured. |
|
529 |
||
530 |
* The 'fixrec' package now produces better fixed-point induction rules |
|
531 |
for mutually-recursive definitions: Induction rules have conclusions |
|
532 |
of the form "P foo bar" instead of "P <foo, bar>". |
|
533 |
||
534 |
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has |
|
535 |
been renamed to "below". The name "below" now replaces "less" in many |
|
33842 | 536 |
theorem names. (Legacy theorem names using "less" are still supported |
537 |
as well.) |
|
33825 | 538 |
|
539 |
* The 'fixrec' package now supports "bottom patterns". Bottom |
|
540 |
patterns can be used to generate strictness rules, or to make |
|
541 |
functions more strict (much like the bang-patterns supported by the |
|
33873 | 542 |
Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for |
543 |
examples. |
|
33825 | 544 |
|
545 |
||
31304 | 546 |
*** ML *** |
547 |
||
33843 | 548 |
* Support for Poly/ML 5.3.0, with improved reporting of compiler |
549 |
errors and run-time exceptions, including detailed source positions. |
|
550 |
||
551 |
* Structure Name_Space (formerly NameSpace) now manages uniquely |
|
552 |
identified entries, with some additional information such as source |
|
553 |
position, logical grouping etc. |
|
554 |
||
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
555 |
* Theory and context data is now introduced by the simplified and |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
556 |
modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
557 |
to be pure, but the old TheoryDataFun for mutable data (with explicit |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
558 |
copy operation) is still available for some time. |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
559 |
|
32742 | 560 |
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) |
561 |
provides a high-level programming interface to synchronized state |
|
562 |
variables with atomic update. This works via pure function |
|
563 |
application within a critical section -- its runtime should be as |
|
564 |
short as possible; beware of deadlocks if critical code is nested, |
|
565 |
either directly or indirectly via other synchronized variables! |
|
566 |
||
567 |
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML) |
|
568 |
wraps raw ML references, explicitly indicating their non-thread-safe |
|
569 |
behaviour. The Isar toplevel keeps this structure open, to |
|
570 |
accommodate Proof General as well as quick and dirty interactive |
|
571 |
experiments with references. |
|
572 |
||
32365 | 573 |
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for |
574 |
parallel tactical reasoning. |
|
575 |
||
32427 | 576 |
* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS |
577 |
are similar to SUBPROOF, but are slightly more flexible: only the |
|
578 |
specified parts of the subgoal are imported into the context, and the |
|
579 |
body tactic may introduce new subgoals and schematic variables. |
|
580 |
||
581 |
* Old tactical METAHYPS, which does not observe the proof context, has |
|
582 |
been renamed to Old_Goals.METAHYPS and awaits deletion. Use SUBPROOF |
|
583 |
or Subgoal.FOCUS etc. |
|
32216 | 584 |
|
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
585 |
* Renamed functor TableFun to Table, and GraphFun to Graph. (Since |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
586 |
functors have their own ML name space there is no point to mark them |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
587 |
separately.) Minor INCOMPATIBILITY. |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
588 |
|
31901 | 589 |
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY. |
590 |
||
33842 | 591 |
* Renamed several structures FooBar to Foo_Bar. Occasional, |
592 |
INCOMPATIBILITY. |
|
593 |
||
33843 | 594 |
* Operations of structure Skip_Proof no longer require quick_and_dirty |
595 |
mode, which avoids critical setmp. |
|
596 |
||
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
597 |
* Eliminated old Attrib.add_attributes, Method.add_methods and related |
33842 | 598 |
combinators for "args". INCOMPATIBILITY, need to use simplified |
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
599 |
Attrib/Method.setup introduced in Isabelle2009. |
31304 | 600 |
|
32151
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
601 |
* Proper context for simpset_of, claset_of, clasimpset_of. May fall |
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
602 |
back on global_simpset_of, global_claset_of, global_clasimpset_of as |
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
603 |
last resort. INCOMPATIBILITY. |
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
604 |
|
32092
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
605 |
* Display.pretty_thm now requires a proper context (cf. former |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
606 |
ProofContext.pretty_thm). May fall back on Display.pretty_thm_global |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
607 |
or even Display.pretty_thm_without_context as last resort. |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
608 |
INCOMPATIBILITY. |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
609 |
|
32433 | 610 |
* Discontinued Display.pretty_ctyp/cterm etc. INCOMPATIBILITY, use |
611 |
Syntax.pretty_typ/term directly, preferably with proper context |
|
612 |
instead of global theory. |
|
613 |
||
31304 | 614 |
|
31308 | 615 |
*** System *** |
616 |
||
33842 | 617 |
* Further fine tuning of parallel proof checking, scales up to 8 cores |
618 |
(max. speedup factor 5.0). See also Goal.parallel_proofs in ML and |
|
619 |
usedir option -q. |
|
620 |
||
32326 | 621 |
* Support for additional "Isabelle components" via etc/components, see |
622 |
also the system manual. |
|
623 |
||
624 |
* The isabelle makeall tool now operates on all components with |
|
625 |
IsaMakefile, not just hardwired "logics". |
|
626 |
||
33842 | 627 |
* Removed "compress" option from isabelle-process and isabelle usedir; |
628 |
this is always enabled. |
|
33818 | 629 |
|
31308 | 630 |
* Discontinued support for Poly/ML 4.x versions. |
631 |
||
33842 | 632 |
* Isabelle tool "wwwfind" provides web interface for 'find_theorems' |
633 |
on a given logic image. This requires the lighttpd webserver and is |
|
634 |
currently supported on Linux only. |
|
32061
11f8ee55662d
parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents:
31997
diff
changeset
|
635 |
|
31308 | 636 |
|
31304 | 637 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
638 |
New in Isabelle2009 (April 2009) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
639 |
-------------------------------- |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
640 |
|
27599 | 641 |
*** General *** |
642 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
643 |
* Simplified main Isabelle executables, with less surprises on |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
644 |
case-insensitive file-systems (such as Mac OS). |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
645 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
646 |
- The main Isabelle tool wrapper is now called "isabelle" instead of |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
647 |
"isatool." |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
648 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
649 |
- The former "isabelle" alias for "isabelle-process" has been |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
650 |
removed (should rarely occur to regular users). |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
651 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
652 |
- The former "isabelle-interface" and its alias "Isabelle" have been |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
653 |
removed (interfaces are now regular Isabelle tools). |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
654 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
655 |
Within scripts and make files, the Isabelle environment variables |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
656 |
ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE, |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
657 |
respectively. (The latter are still available as legacy feature.) |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
658 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
659 |
The old isabelle-interface wrapper could react in confusing ways if |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
660 |
the interface was uninstalled or changed otherwise. Individual |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
661 |
interface tool configuration is now more explicit, see also the |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
662 |
Isabelle system manual. In particular, Proof General is now available |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
663 |
via "isabelle emacs". |
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
664 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
665 |
INCOMPATIBILITY, need to adapt derivative scripts. Users may need to |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
666 |
purge installed copies of Isabelle executables and re-run "isabelle |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
667 |
install -p ...", or use symlinks. |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
668 |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
669 |
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
670 |
old ~/isabelle, which was slightly non-standard and apt to cause |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
671 |
surprises on case-insensitive file-systems (such as Mac OS). |
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
672 |
|
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
673 |
INCOMPATIBILITY, need to move existing ~/isabelle/etc, |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
674 |
~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
675 |
care is required when using older releases of Isabelle. Note that |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
676 |
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
677 |
Isabelle distribution, in order to use the new ~/.isabelle uniformly. |
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
678 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
679 |
* Proofs of fully specified statements are run in parallel on |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
680 |
multi-core systems. A speedup factor of 2.5 to 3.2 can be expected on |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
681 |
a regular 4-core machine, if the initial heap space is made reasonably |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
682 |
large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
683 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
684 |
* The main reference manuals ("isar-ref", "implementation", and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
685 |
"system") have been updated and extended. Formally checked references |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
686 |
as hyperlinks are now available uniformly. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
687 |
|
30163
faf95eb3f375
* New prover for coherent logic (see src/Tools/coherent.ML).
wenzelm
parents:
30106
diff
changeset
|
688 |
|
27599 | 689 |
*** Pure *** |
690 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
691 |
* Complete re-implementation of locales. INCOMPATIBILITY in several |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
692 |
respects. The most important changes are listed below. See the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
693 |
Tutorial on Locales ("locales" manual) for details. |
29253 | 694 |
|
695 |
- In locale expressions, instantiation replaces renaming. Parameters |
|
696 |
must be declared in a for clause. To aid compatibility with previous |
|
697 |
parameter inheritance, in locale declarations, parameters that are not |
|
698 |
'touched' (instantiation position "_" or omitted) are implicitly added |
|
699 |
with their syntax at the beginning of the for clause. |
|
700 |
||
701 |
- Syntax from abbreviations and definitions in locales is available in |
|
702 |
locale expressions and context elements. The latter is particularly |
|
703 |
useful in locale declarations. |
|
704 |
||
705 |
- More flexible mechanisms to qualify names generated by locale |
|
706 |
expressions. Qualifiers (prefixes) may be specified in locale |
|
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
707 |
expressions, and can be marked as mandatory (syntax: "name!:") or |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
708 |
optional (syntax "name?:"). The default depends for plain "name:" |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
709 |
depends on the situation where a locale expression is used: in |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
710 |
commands 'locale' and 'sublocale' prefixes are optional, in |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
711 |
'interpretation' and 'interpret' prefixes are mandatory. The old |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
712 |
implicit qualifiers derived from the parameter names of a locale are |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
713 |
no longer generated. |
30106 | 714 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
715 |
- Command "sublocale l < e" replaces "interpretation l < e". The |
30106 | 716 |
instantiation clause in "interpretation" and "interpret" (square |
717 |
brackets) is no longer available. Use locale expressions. |
|
29253 | 718 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
719 |
- When converting proof scripts, mandatory qualifiers in |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
720 |
'interpretation' and 'interpret' should be retained by default, even |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
721 |
if this is an INCOMPATIBILITY compared to former behavior. In the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
722 |
worst case, use the "name?:" form for non-mandatory ones. Qualifiers |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
723 |
in locale expressions range over a single locale instance only. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
724 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
725 |
- Dropped locale element "includes". This is a major INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
726 |
In existing theorem specifications replace the includes element by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
727 |
respective context elements of the included locale, omitting those |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
728 |
that are already present in the theorem specification. Multiple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
729 |
assume elements of a locale should be replaced by a single one |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
730 |
involving the locale predicate. In the proof body, declarations (most |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
731 |
notably theorems) may be regained by interpreting the respective |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
732 |
locales in the proof context as required (command "interpret"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
733 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
734 |
If using "includes" in replacement of a target solely because the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
735 |
parameter types in the theorem are not as general as in the target, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
736 |
consider declaring a new locale with additional type constraints on |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
737 |
the parameters (context element "constrains"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
738 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
739 |
- Discontinued "locale (open)". INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
740 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
741 |
- Locale interpretation commands no longer attempt to simplify goal. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
742 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
743 |
methods intro_locales and unfold_locales to clarify. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
744 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
745 |
- Locale interpretation commands no longer accept interpretation |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
746 |
attributes. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
747 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
748 |
* Class declaration: so-called "base sort" must not be given in import |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
749 |
list any longer, but is inferred from the specification. Particularly |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
750 |
in HOL, write |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
751 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
752 |
class foo = ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
753 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
754 |
instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
755 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
756 |
class foo = type + ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
757 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
758 |
* Class target: global versions of theorems stemming do not carry a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
759 |
parameter prefix any longer. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
760 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
761 |
* Class 'instance' command no longer accepts attached definitions. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
762 |
INCOMPATIBILITY, use proper 'instantiation' target instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
763 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
764 |
* Recovered hiding of consts, which was accidentally broken in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
765 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
766 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
767 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
768 |
* Slightly more coherent Pure syntax, with updated documentation in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
769 |
isar-ref manual. Removed locales meta_term_syntax and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
770 |
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
771 |
INCOMPATIBILITY in rare situations. Note that &&& should not be used |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
772 |
directly in regular applications. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
773 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
774 |
* There is a new syntactic category "float_const" for signed decimal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
775 |
fractions (e.g. 123.45 or -123.45). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
776 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
777 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
778 |
interface with 'setup' command instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
779 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
780 |
* Command 'local_setup' is similar to 'setup', but operates on a local |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
781 |
theory context. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
782 |
|
28114 | 783 |
* The 'axiomatization' command now only works within a global theory |
784 |
context. INCOMPATIBILITY. |
|
785 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
786 |
* Goal-directed proof now enforces strict proof irrelevance wrt. sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
787 |
hypotheses. Sorts required in the course of reasoning need to be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
788 |
covered by the constraints in the initial statement, completed by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
789 |
type instance information of the background theory. Non-trivial sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
790 |
hypotheses, which rarely occur in practice, may be specified via |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
791 |
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
792 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
793 |
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
794 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
795 |
The result contains an implicit sort hypotheses as before -- |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
796 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
797 |
normalization. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
798 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
799 |
* Generalized Isar history, with support for linear undo, direct state |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
800 |
addressing etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
801 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
802 |
* Changed defaults for unify configuration options: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
803 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
804 |
unify_trace_bound = 50 (formerly 25) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
805 |
unify_search_bound = 60 (formerly 30) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
806 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
807 |
* Different bookkeeping for code equations (INCOMPATIBILITY): |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
808 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
809 |
a) On theory merge, the last set of code equations for a particular |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
810 |
constant is taken (in accordance with the policy applied by other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
811 |
parts of the code generator framework). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
812 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
813 |
b) Code equations stemming from explicit declarations (e.g. code |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
814 |
attribute) gain priority over default code equations stemming |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
815 |
from definition, primrec, fun etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
816 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
817 |
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
818 |
|
30965 | 819 |
* Unified theorem tables for both code generators. Thus [code |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
820 |
func] has disappeared and only [code] remains. INCOMPATIBILITY. |
30577 | 821 |
|
822 |
* Command 'find_consts' searches for constants based on type and name |
|
823 |
patterns, e.g. |
|
29883 | 824 |
|
825 |
find_consts "_ => bool" |
|
826 |
||
30106 | 827 |
By default, matching is against subtypes, but it may be restricted to |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
828 |
the whole type. Searching by name is possible. Multiple queries are |
30106 | 829 |
conjunctive and queries may be negated by prefixing them with a |
830 |
hyphen: |
|
29883 | 831 |
|
832 |
find_consts strict: "_ => bool" name: "Int" -"int => int" |
|
29861
3c348f5873f3
updated NEWS etc with "solves" criterion and auto_solves
kleing
parents:
29823
diff
changeset
|
833 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
834 |
* New 'find_theorems' criterion "solves" matches theorems that |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
835 |
directly solve the current goal (modulo higher-order unification). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
836 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
837 |
* Auto solve feature for main theorem statements: whenever a new goal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
838 |
is stated, "find_theorems solves" is called; any theorems that could |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
839 |
solve the lemma directly are listed as part of the goal state. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
840 |
Cf. associated options in Proof General Isabelle settings menu, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
841 |
enabled by default, with reasonable timeout for pathological cases of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
842 |
higher-order unification. |
30415
9501af91c4a3
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
30399
diff
changeset
|
843 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
844 |
|
27381 | 845 |
*** Document preparation *** |
846 |
||
847 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 848 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
849 |
syntax just like the Isar command 'by'. |
27381 | 850 |
|
851 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
852 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
853 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
854 |
* Integrated main parts of former image HOL-Complex with HOL. Entry |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
855 |
points Main and Complex_Main remain as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
856 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
857 |
* Logic image HOL-Plain provides a minimal HOL with the most important |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
858 |
tools available (inductive, datatype, primrec, ...). This facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
859 |
experimentation and tool development. Note that user applications |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
860 |
(and library theories) should never refer to anything below theory |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
861 |
Main, as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
862 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
863 |
* Logic image HOL-Main stops at theory Main, and thus facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
864 |
experimentation due to shorter build times. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
865 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
866 |
* Logic image HOL-NSA contains theories of nonstandard analysis which |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
867 |
were previously part of former HOL-Complex. Entry point Hyperreal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
868 |
remains valid, but theories formerly using Complex_Main should now use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
869 |
new entry point Hypercomplex. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
870 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
871 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
872 |
Posix processes. Avoids potentially expensive forking of the ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
873 |
process. New thread-based implementation also works on non-Unix |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
874 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
875 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
876 |
commands are covered in the isar-ref manual. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
877 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
878 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
879 |
sledgehammer without local ATP installation (Vampire etc.). Other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
880 |
provers may be included via suitable ML wrappers, see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
881 |
src/HOL/ATP_Linkup.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
882 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
883 |
* ATP selection (E/Vampire/Spass) is now via Proof General's settings |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
884 |
menu. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
885 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
886 |
* The metis method no longer fails because the theorem is too trivial |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
887 |
(contains the empty clause). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
888 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
889 |
* The metis method now fails in the usual manner, rather than raising |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
890 |
an exception, if it determines that it cannot prove the theorem. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
891 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
892 |
* Method "coherent" implements a prover for coherent logic (see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
893 |
src/Tools/coherent.ML). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
894 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
895 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
896 |
"undefined" is the right choice to replace "arbitrary", though |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
897 |
logically there is no difference. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
898 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
899 |
* Command "value" now integrates different evaluation mechanisms. The |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
900 |
result of the first successful evaluation mechanism is printed. In |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
901 |
square brackets a particular named evaluation mechanisms may be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
902 |
specified (currently, [SML], [code] or [nbe]). See further |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
903 |
src/HOL/ex/Eval_Examples.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
904 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
905 |
* Normalization by evaluation now allows non-leftlinear equations. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
906 |
Declare with attribute [code nbe]. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
907 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
908 |
* Methods "case_tac" and "induct_tac" now refer to the very same rules |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
909 |
as the structured Isar versions "cases" and "induct", cf. the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
910 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
911 |
are now presented as a list of individual projections |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
912 |
(e.g. foo_bar.inducts for types foo and bar); the old format with |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
913 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
914 |
rare situations a different rule is selected --- notably nested tuple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
915 |
elimination instead of former prod.exhaust: use explicit (case_tac t |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
916 |
rule: prod.exhaust) here. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
917 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
918 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
919 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
920 |
* Removed fact "case_split_thm", which duplicates "case_split". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
921 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
922 |
* The option datatype has been moved to a new theory Option. Renamed |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
923 |
option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
924 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
925 |
* New predicate "strict_mono" classifies strict functions on partial |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
926 |
orders. With strict functions on linear orders, reasoning about |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
927 |
(in)equalities is facilitated by theorems "strict_mono_eq", |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
928 |
"strict_mono_less_eq" and "strict_mono_less". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
929 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
930 |
* Some set operations are now proper qualified constants with |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
931 |
authentic syntax. INCOMPATIBILITY: |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
932 |
|
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
933 |
op Int ~> Set.Int |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
934 |
op Un ~> Set.Un |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
935 |
INTER ~> Set.INTER |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
936 |
UNION ~> Set.UNION |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
937 |
Inter ~> Set.Inter |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
938 |
Union ~> Set.Union |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
939 |
{} ~> Set.empty |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
940 |
UNIV ~> Set.UNIV |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
941 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
942 |
* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
943 |
theory Set. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
944 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
945 |
* Auxiliary class "itself" has disappeared -- classes without any |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
946 |
parameter are treated as expected by the 'class' command. |
29797 | 947 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
948 |
* Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
949 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
950 |
* Common decision procedures (Cooper, MIR, Ferrack, Approximation, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
951 |
Dense_Linear_Order) are now in directory HOL/Decision_Procs. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
952 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
953 |
* Theory src/HOL/Decision_Procs/Approximation provides the new proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
954 |
method "approximation". It proves formulas on real values by using |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
955 |
interval arithmetic. In the formulas are also the transcendental |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
956 |
functions sin, cos, tan, atan, ln, exp and the constant pi are |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
957 |
allowed. For examples see |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
958 |
src/HOL/Descision_Procs/ex/Approximation_Ex.thy. |
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
959 |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
960 |
* Theory "Reflection" now resides in HOL/Library. |
29650 | 961 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
962 |
* Entry point to Word library now simply named "Word". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
963 |
INCOMPATIBILITY. |
29628 | 964 |
|
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
965 |
* Made source layout more coherent with logical distribution |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
966 |
structure: |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
967 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
968 |
src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
969 |
src/HOL/Library/Code_Message.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
970 |
src/HOL/Library/GCD.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
971 |
src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
972 |
src/HOL/Library/Parity.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
973 |
src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
974 |
src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
975 |
src/HOL/Real/Lubs.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
976 |
src/HOL/Real/PReal.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
977 |
src/HOL/Real/Rational.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
978 |
src/HOL/Real/RComplete.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
979 |
src/HOL/Real/RealDef.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
980 |
src/HOL/Real/RealPow.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
981 |
src/HOL/Real/Real.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
982 |
src/HOL/Complex/Complex_Main.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
983 |
src/HOL/Complex/Complex.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
984 |
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/ |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
985 |
src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
986 |
src/HOL/Hyperreal/Deriv.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
987 |
src/HOL/Hyperreal/Fact.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
988 |
src/HOL/Hyperreal/Integration.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
989 |
src/HOL/Hyperreal/Lim.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
990 |
src/HOL/Hyperreal/Ln.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
991 |
src/HOL/Hyperreal/Log.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
992 |
src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
993 |
src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
994 |
src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
995 |
src/HOL/Hyperreal/SEQ.thy ~> src/HOL/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
996 |
src/HOL/Hyperreal/Taylor.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
997 |
src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
998 |
src/HOL/Real/Float ~> src/HOL/Library/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
999 |
src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1000 |
src/HOL/Real/RealVector.thy ~> src/HOL/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1001 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1002 |
src/HOL/arith_data.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1003 |
src/HOL/hologic.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1004 |
src/HOL/simpdata.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1005 |
src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1006 |
src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1007 |
src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1008 |
src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1009 |
src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1010 |
src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1011 |
src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1012 |
|
29398 | 1013 |
src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL |
1014 |
src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL |
|
1015 |
src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL |
|
1016 |
src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL |
|
1017 |
src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL |
|
1018 |
src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL |
|
1019 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1020 |
* If methods "eval" and "evaluation" encounter a structured proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1021 |
state with !!/==>, only the conclusion is evaluated to True (if |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1022 |
possible), avoiding strange error messages. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1023 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1024 |
* Method "sizechange" automates termination proofs using (a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1025 |
modification of) the size-change principle. Requires SAT solver. See |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1026 |
src/HOL/ex/Termination.thy for examples. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1027 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1028 |
* Simplifier: simproc for let expressions now unfolds if bound |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1029 |
variable occurs at most once in let expression body. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1030 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1031 |
* Method "arith": Linear arithmetic now ignores all inequalities when |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1032 |
fast_arith_neq_limit is exceeded, instead of giving up entirely. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1033 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1034 |
* New attribute "arith" for facts that should always be used |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1035 |
automatically by arithmetic. It is intended to be used locally in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1036 |
proofs, e.g. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1037 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1038 |
assumes [arith]: "x > 0" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1039 |
|
30706 | 1040 |
Global usage is discouraged because of possible performance impact. |
1041 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1042 |
* New classes "top" and "bot" with corresponding operations "top" and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1043 |
"bot" in theory Orderings; instantiation of class "complete_lattice" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1044 |
requires instantiation of classes "top" and "bot". INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1045 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1046 |
* Changed definition lemma "less_fun_def" in order to provide an |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1047 |
instance for preorders on functions; use lemma "less_le" instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1048 |
INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1049 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1050 |
* Theory Orderings: class "wellorder" moved here, with explicit |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1051 |
induction rule "less_induct" as assumption. For instantiation of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1052 |
"wellorder" by means of predicate "wf", use rule wf_wellorderI. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1053 |
INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1054 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1055 |
* Theory Orderings: added class "preorder" as superclass of "order". |
27793 | 1056 |
INCOMPATIBILITY: Instantiation proofs for order, linorder |
1057 |
etc. slightly changed. Some theorems named order_class.* now named |
|
1058 |
preorder_class.*. |
|
1059 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1060 |
* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1061 |
"diag" to "Id_on". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1062 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1063 |
* Theory Finite_Set: added a new fold combinator of type |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1064 |
|
28855 | 1065 |
('a => 'b => 'b) => 'b => 'a set => 'b |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1066 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1067 |
Occasionally this is more convenient than the old fold combinator |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1068 |
which is now defined in terms of the new one and renamed to |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1069 |
fold_image. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1070 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1071 |
* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1072 |
and "ring_simps" have been replaced by "algebra_simps" (which can be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1073 |
extended with further lemmas!). At the moment both still exist but |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1074 |
the former will disappear at some point. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1075 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1076 |
* Theory Power: Lemma power_Suc is now declared as a simp rule in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1077 |
class recpower. Type-specific simp rules for various recpower types |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1078 |
have been removed. INCOMPATIBILITY, rename old lemmas as follows: |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1079 |
|
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1080 |
rat_power_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1081 |
rat_power_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1082 |
realpow_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1083 |
realpow_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1084 |
complexpow_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1085 |
complexpow_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1086 |
power_poly_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1087 |
power_poly_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
1088 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1089 |
* Theories Ring_and_Field and Divides: Definition of "op dvd" has been |
27793 | 1090 |
moved to separate class dvd in Ring_and_Field; a couple of lemmas on |
1091 |
dvd has been generalized to class comm_semiring_1. Likewise a bunch |
|
1092 |
of lemmas from Divides has been generalized from nat to class |
|
1093 |
semiring_div. INCOMPATIBILITY. This involves the following theorem |
|
1094 |
renames resulting from duplicate elimination: |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1095 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1096 |
dvd_def_mod ~> dvd_eq_mod_eq_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1097 |
zero_dvd_iff ~> dvd_0_left_iff |
28559 | 1098 |
dvd_0 ~> dvd_0_right |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1099 |
DIVISION_BY_ZERO_DIV ~> div_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1100 |
DIVISION_BY_ZERO_MOD ~> mod_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1101 |
mult_div ~> div_mult_self2_is_id |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1102 |
mult_mod ~> mod_mult_self2_is_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1103 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1104 |
* Theory IntDiv: removed many lemmas that are instances of class-based |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1105 |
generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1106 |
rename old lemmas as follows: |
30044 | 1107 |
|
1108 |
dvd_diff -> nat_dvd_diff |
|
1109 |
dvd_zminus_iff -> dvd_minus_iff |
|
30224 | 1110 |
mod_add1_eq -> mod_add_eq |
1111 |
mod_mult1_eq -> mod_mult_right_eq |
|
1112 |
mod_mult1_eq' -> mod_mult_left_eq |
|
1113 |
mod_mult_distrib_mod -> mod_mult_eq |
|
30044 | 1114 |
nat_mod_add_left_eq -> mod_add_left_eq |
1115 |
nat_mod_add_right_eq -> mod_add_right_eq |
|
1116 |
nat_mod_div_trivial -> mod_div_trivial |
|
1117 |
nat_mod_mod_trivial -> mod_mod_trivial |
|
1118 |
zdiv_zadd_self1 -> div_add_self1 |
|
1119 |
zdiv_zadd_self2 -> div_add_self2 |
|
30181 | 1120 |
zdiv_zmult_self1 -> div_mult_self2_is_id |
30044 | 1121 |
zdiv_zmult_self2 -> div_mult_self1_is_id |
1122 |
zdvd_triv_left -> dvd_triv_left |
|
1123 |
zdvd_triv_right -> dvd_triv_right |
|
1124 |
zdvd_zmult_cancel_disj -> dvd_mult_cancel_left |
|
30085 | 1125 |
zmod_eq0_zdvd_iff -> dvd_eq_mod_eq_0[symmetric] |
30044 | 1126 |
zmod_zadd_left_eq -> mod_add_left_eq |
1127 |
zmod_zadd_right_eq -> mod_add_right_eq |
|
1128 |
zmod_zadd_self1 -> mod_add_self1 |
|
1129 |
zmod_zadd_self2 -> mod_add_self2 |
|
30224 | 1130 |
zmod_zadd1_eq -> mod_add_eq |
30044 | 1131 |
zmod_zdiff1_eq -> mod_diff_eq |
1132 |
zmod_zdvd_zmod -> mod_mod_cancel |
|
1133 |
zmod_zmod_cancel -> mod_mod_cancel |
|
1134 |
zmod_zmult_self1 -> mod_mult_self2_is_0 |
|
1135 |
zmod_zmult_self2 -> mod_mult_self1_is_0 |
|
1136 |
zmod_1 -> mod_by_1 |
|
1137 |
zdiv_1 -> div_by_1 |
|
1138 |
zdvd_abs1 -> abs_dvd_iff |
|
1139 |
zdvd_abs2 -> dvd_abs_iff |
|
1140 |
zdvd_refl -> dvd_refl |
|
1141 |
zdvd_trans -> dvd_trans |
|
1142 |
zdvd_zadd -> dvd_add |
|
1143 |
zdvd_zdiff -> dvd_diff |
|
1144 |
zdvd_zminus_iff -> dvd_minus_iff |
|
1145 |
zdvd_zminus2_iff -> minus_dvd_iff |
|
1146 |
zdvd_zmultD -> dvd_mult_right |
|
1147 |
zdvd_zmultD2 -> dvd_mult_left |
|
1148 |
zdvd_zmult_mono -> mult_dvd_mono |
|
1149 |
zdvd_0_right -> dvd_0_right |
|
1150 |
zdvd_0_left -> dvd_0_left_iff |
|
1151 |
zdvd_1_left -> one_dvd |
|
1152 |
zminus_dvd_iff -> minus_dvd_iff |
|
1153 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1154 |
* Theory Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1155 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1156 |
* The real numbers offer decimal input syntax: 12.34 is translated |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1157 |
into 1234/10^2. This translation is not reversed upon output. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1158 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1159 |
* Theory Library/Polynomial defines an abstract type 'a poly of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1160 |
univariate polynomials with coefficients of type 'a. In addition to |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1161 |
the standard ring operations, it also supports div and mod. Code |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1162 |
generation is also supported, using list-style constructors. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1163 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1164 |
* Theory Library/Inner_Product defines a class of real_inner for real |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1165 |
inner product spaces, with an overloaded operation inner :: 'a => 'a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1166 |
=> real. Class real_inner is a subclass of real_normed_vector from |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1167 |
theory RealVector. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1168 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1169 |
* Theory Library/Product_Vector provides instances for the product |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1170 |
type 'a * 'b of several classes from RealVector and Inner_Product. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1171 |
Definitions of addition, subtraction, scalar multiplication, norms, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1172 |
and inner products are included. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1173 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1174 |
* Theory Library/Bit defines the field "bit" of integers modulo 2. In |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1175 |
addition to the field operations, numerals and case syntax are also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1176 |
supported. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1177 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1178 |
* Theory Library/Diagonalize provides constructive version of Cantor's |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1179 |
first diagonalization argument. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1180 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1181 |
* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
27599 | 1182 |
zlcm (for int); carried together from various gcd/lcm developements in |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1183 |
the HOL Distribution. Constants zgcd and zlcm replace former igcd and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1184 |
ilcm; corresponding theorems renamed accordingly. INCOMPATIBILITY, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1185 |
may recover tupled syntax as follows: |
27556 | 1186 |
|
1187 |
hide (open) const gcd |
|
1188 |
abbreviation gcd where |
|
1189 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
1190 |
notation (output) |
|
1191 |
GCD.gcd ("gcd '(_, _')") |
|
1192 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1193 |
The same works for lcm, zgcd, zlcm. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1194 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1195 |
* Theory Library/Nat_Infinity: added addition, numeral syntax and more |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1196 |
instantiations for algebraic structures. Removed some duplicate |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1197 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1198 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1199 |
* ML antiquotation @{code} takes a constant as argument and generates |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1200 |
corresponding code in background and inserts name of the corresponding |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1201 |
resulting ML value/function/datatype constructor binding in place. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1202 |
All occurrences of @{code} with a single ML block are generated |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
1203 |
simultaneously. Provides a generic and safe interface for |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1204 |
instrumentalizing code generation. See |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1205 |
src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1206 |
In future you ought to refrain from ad-hoc compiling generated SML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1207 |
code on the ML toplevel. Note that (for technical reasons) @{code} |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1208 |
cannot refer to constants for which user-defined serializations are |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1209 |
set. Refer to the corresponding ML counterpart directly in that |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1210 |
cases. |
27122 | 1211 |
|
1212 |
* Command 'rep_datatype': instead of theorem names the command now |
|
1213 |
takes a list of terms denoting the constructors of the type to be |
|
1214 |
represented as datatype. The characteristic theorems have to be |
|
1215 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
1216 |
have disappeared in favour of existing ones: |
|
1217 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1218 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1219 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1220 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1221 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1222 |
Suc_not_Zero Zero_not_Suc ~> nat.distinct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1223 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1224 |
|
27696 | 1225 |
*** HOL-Algebra *** |
1226 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
1227 |
* New locales for orders and lattices where the equivalence relation |
30106 | 1228 |
is not restricted to equality. INCOMPATIBILITY: all order and lattice |
1229 |
locales use a record structure with field eq for the equivalence. |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
1230 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
1231 |
* New theory of factorial domains. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
1232 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1233 |
* Units_l_inv and Units_r_inv are now simp rules by default. |
27696 | 1234 |
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
1235 |
and/or r_inv will now also require deletion of these lemmas. |
|
1236 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1237 |
* Renamed the following theorems, INCOMPATIBILITY: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1238 |
|
27696 | 1239 |
UpperD ~> Upper_memD |
1240 |
LowerD ~> Lower_memD |
|
1241 |
least_carrier ~> least_closed |
|
1242 |
greatest_carrier ~> greatest_closed |
|
1243 |
greatest_Lower_above ~> greatest_Lower_below |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
1244 |
one_zero ~> carrier_one_zero |
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
1245 |
one_not_zero ~> carrier_one_not_zero (collision with assumption) |
27696 | 1246 |
|
27793 | 1247 |
|
30849 | 1248 |
*** HOL-Nominal *** |
1249 |
||
30855 | 1250 |
* Nominal datatypes can now contain type-variables. |
1251 |
||
1252 |
* Commands 'nominal_inductive' and 'equivariance' work with local |
|
1253 |
theory targets. |
|
1254 |
||
1255 |
* Nominal primrec can now works with local theory targets and its |
|
1256 |
specification syntax now conforms to the general format as seen in |
|
1257 |
'inductive' etc. |
|
1258 |
||
1259 |
* Method "perm_simp" honours the standard simplifier attributes |
|
1260 |
(no_asm), (no_asm_use) etc. |
|
1261 |
||
1262 |
* The new predicate #* is defined like freshness, except that on the |
|
1263 |
left hand side can be a set or list of atoms. |
|
1264 |
||
1265 |
* Experimental command 'nominal_inductive2' derives strong induction |
|
1266 |
principles for inductive definitions. In contrast to |
|
1267 |
'nominal_inductive', which can only deal with a fixed number of |
|
1268 |
binders, it can deal with arbitrary expressions standing for sets of |
|
1269 |
atoms to be avoided. The only inductive definition we have at the |
|
1270 |
moment that needs this generalisation is the typing rule for Lets in |
|
1271 |
the algorithm W: |
|
1272 |
||
1273 |
Gamma |- t1 : T1 (x,close Gamma T1)::Gamma |- t2 : T2 x#Gamma |
|
1274 |
----------------------------------------------------------------- |
|
1275 |
Gamma |- Let x be t1 in t2 : T2 |
|
1276 |
||
1277 |
In this rule one wants to avoid all the binders that are introduced by |
|
1278 |
"close Gamma T1". We are looking for other examples where this |
|
1279 |
feature might be useful. Please let us know. |
|
30849 | 1280 |
|
1281 |
||
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1282 |
*** HOLCF *** |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1283 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1284 |
* Reimplemented the simplification procedure for proving continuity |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1285 |
subgoals. The new simproc is extensible; users can declare additional |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1286 |
continuity introduction rules with the attribute [cont2cont]. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1287 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1288 |
* The continuity simproc now uses a different introduction rule for |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1289 |
solving continuity subgoals on terms with lambda abstractions. In |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1290 |
some rare cases the new simproc may fail to solve subgoals that the |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1291 |
old one could solve, and "simp add: cont2cont_LAM" may be necessary. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1292 |
Potential INCOMPATIBILITY. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1293 |
|
30847 | 1294 |
* Command 'fixrec': specification syntax now conforms to the general |
30855 | 1295 |
format as seen in 'inductive' etc. See src/HOLCF/ex/Fixrec_ex.thy for |
1296 |
examples. INCOMPATIBILITY. |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1297 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1298 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1299 |
*** ZF *** |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1300 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1301 |
* Proof of Zorn's Lemma for partial orders. |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1302 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1303 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
1304 |
*** ML *** |
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
1305 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1306 |
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1307 |
Poly/ML 5.2.1 or later. Important note: the TimeLimit facility |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1308 |
depends on multithreading, so timouts will not work before Poly/ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1309 |
5.2.1! |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1310 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1311 |
* High-level support for concurrent ML programming, see |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1312 |
src/Pure/Cuncurrent. The data-oriented model of "future values" is |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1313 |
particularly convenient to organize independent functional |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1314 |
computations. The concept of "synchronized variables" provides a |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1315 |
higher-order interface for components with shared state, avoiding the |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1316 |
delicate details of mutexes and condition variables. (Requires |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1317 |
Poly/ML 5.2.1 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1318 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1319 |
* ML bindings produced via Isar commands are stored within the Isar |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1320 |
context (theory or proof). Consequently, commands like 'use' and 'ML' |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1321 |
become thread-safe and work with undo as expected (concerning |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1322 |
top-level bindings, not side-effects on global references). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1323 |
INCOMPATIBILITY, need to provide proper Isar context when invoking the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1324 |
compiler at runtime; really global bindings need to be given outside a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1325 |
theory. (Requires Poly/ML 5.2 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1326 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1327 |
* Command 'ML_prf' is analogous to 'ML' but works within a proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1328 |
context. Top-level ML bindings are stored within the proof context in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1329 |
a purely sequential fashion, disregarding the nested proof structure. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1330 |
ML bindings introduced by 'ML_prf' are discarded at the end of the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1331 |
proof. (Requires Poly/ML 5.2 or later.) |
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1332 |
|
30530 | 1333 |
* Simplified ML attribute and method setup, cf. functions Attrib.setup |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1334 |
and Method.setup, as well as Isar commands 'attribute_setup' and |
30547 | 1335 |
'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify |
1336 |
existing code accordingly, or use plain 'setup' together with old |
|
1337 |
Method.add_method. |
|
30530 | 1338 |
|
28294 | 1339 |
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
1340 |
to 'a -> thm, while results are always tagged with an authentic oracle |
|
1341 |
name. The Isar command 'oracle' is now polymorphic, no argument type |
|
1342 |
is specified. INCOMPATIBILITY, need to simplify existing oracle code |
|
1343 |
accordingly. Note that extra performance may be gained by producing |
|
1344 |
the cterm carefully, avoiding slow Thm.cterm_of. |
|
1345 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1346 |
* Simplified interface for defining document antiquotations via |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1347 |
ThyOutput.antiquotation, ThyOutput.output, and optionally |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1348 |
ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1349 |
antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1350 |
examples. |
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
1351 |
|
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1352 |
* More systematic treatment of long names, abstract name bindings, and |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1353 |
name space operations. Basic operations on qualified names have been |
30399 | 1354 |
move from structure NameSpace to Long_Name, e.g. Long_Name.base_name, |
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1355 |
Long_Name.append. Old type bstring has been mostly replaced by |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1356 |
abstract type binding (see structure Binding), which supports precise |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1357 |
qualification by packages and local theory targets, as well as proper |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1358 |
tracking of source positions. INCOMPATIBILITY, need to wrap old |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1359 |
bstring values into Binding.name, or better pass through abstract |
30399 | 1360 |
bindings everywhere. See further src/Pure/General/long_name.ML, |
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1361 |
src/Pure/General/binding.ML and src/Pure/General/name_space.ML |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
1362 |
|
28089
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
1363 |
* Result facts (from PureThy.note_thms, ProofContext.note_thms, |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
1364 |
LocalTheory.note etc.) now refer to the *full* internal name, not the |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
1365 |
bstring as before. INCOMPATIBILITY, not detected by ML type-checking! |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
1366 |
|
27287 | 1367 |
* Disposed old type and term read functions (Sign.read_def_typ, |
1368 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
1369 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
1370 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 1371 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
1372 |
resort for legacy applications. |
|
1373 |
||
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1374 |
* Disposed old declarations, tactics, tactic combinators that refer to |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1375 |
the simpset or claset of an implicit theory (such as Addsimps, |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1376 |
Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1377 |
embedded ML text, or local_simpset_of with a proper context passed as |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1378 |
explicit runtime argument. |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
1379 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1380 |
* Rules and tactics that read instantiations (read_instantiate, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1381 |
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1382 |
context, which is required for parsing and type-checking. Moreover, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1383 |
the variables are specified as plain indexnames, not string encodings |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1384 |
thereof. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1385 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1386 |
* Generic Toplevel.add_hook interface allows to analyze the result of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1387 |
transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1388 |
for theorem dependency output of transactions resulting in a new |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1389 |
theory state. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1390 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1391 |
* ML antiquotations: block-structured compilation context indicated by |
27391 | 1392 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
1393 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1394 |
@{binding name} - basic name binding |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
1395 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
1396 |
@{note name = fact} - fact abbreviation |