author | wenzelm |
Mon, 07 Jun 2010 11:27:08 +0200 | |
changeset 37351 | f34699c3e98e |
parent 37316 | 52dc576f1759 |
child 37352 | c4f393759c59 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
37144 | 4 |
New in Isabelle2009-2 (June 2010) |
5 |
--------------------------------- |
|
33993 | 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 |
|
36508
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
36461
diff
changeset
|
61 |
* Concrete syntax may be attached to local entities without a proof |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
36461
diff
changeset
|
62 |
body, too. This works via regular mixfix annotations for 'fix', |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
36461
diff
changeset
|
63 |
'def', 'obtain' etc. or via the explicit 'write' command, which is |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
36461
diff
changeset
|
64 |
similar to the 'notation' command in theory specifications. |
03d2a2d0ee4a
allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;
wenzelm
parents:
36461
diff
changeset
|
65 |
|
37351 | 66 |
* Discontinued unnamed infix syntax (legacy feature for many years) -- |
67 |
need to specify constant name and syntax separately. Internal ML |
|
68 |
datatype constructors have been renamed from InfixName to Infix etc. |
|
69 |
Minor INCOMPATIBILITY. |
|
70 |
||
71 |
* Schematic theorem statements need to be explicitly markup as such, |
|
72 |
via commands 'schematic_lemma', 'schematic_theorem', |
|
73 |
'schematic_corollary'. Thus the relevance of the proof is made |
|
74 |
syntactically clear, which impacts performance in a parallel or |
|
75 |
asynchronous interactive environment. Minor INCOMPATIBILITY. |
|
76 |
||
35613 | 77 |
* Use of cumulative prems via "!" in some proof methods has been |
37351 | 78 |
discontinued (old legacy feature). |
35613 | 79 |
|
35979
12bb31230550
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents:
35845
diff
changeset
|
80 |
* References 'trace_simp' and 'debug_simp' have been replaced by |
36857 | 81 |
configuration options stored in the context. Enabling tracing (the |
82 |
case of debugging is similar) in proofs works via |
|
83 |
||
84 |
using [[trace_simp = true]] |
|
85 |
||
86 |
Tracing is then active for all invocations of the simplifier in |
|
87 |
subsequent goal refinement steps. Tracing may also still be enabled or |
|
88 |
disabled via the ProofGeneral settings menu. |
|
35979
12bb31230550
replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
boehmes
parents:
35845
diff
changeset
|
89 |
|
36177
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
36162
diff
changeset
|
90 |
* Separate commands 'hide_class', 'hide_type', 'hide_const', |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
36162
diff
changeset
|
91 |
'hide_fact' replace the former 'hide' KIND command. Minor |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
36162
diff
changeset
|
92 |
INCOMPATIBILITY. |
8e0770d2e499
separate commands 'hide_class', 'hide_type', 'hide_const', 'hide_fact';
wenzelm
parents:
36162
diff
changeset
|
93 |
|
37298
1f3ca94ccb84
improved parallelism of proof term normalization;
wenzelm
parents:
37273
diff
changeset
|
94 |
* Improved parallelism of proof term normalization: usedir -p2 -q0 is |
1f3ca94ccb84
improved parallelism of proof term normalization;
wenzelm
parents:
37273
diff
changeset
|
95 |
more efficient than combinations with -q1 or -q2. |
1f3ca94ccb84
improved parallelism of proof term normalization;
wenzelm
parents:
37273
diff
changeset
|
96 |
|
35260 | 97 |
|
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
98 |
*** Pure *** |
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
99 |
|
37351 | 100 |
* Proofterms record type-class reasoning explicitly, using the |
101 |
"unconstrain" operation internally. This eliminates all sort |
|
102 |
constraints from a theorem and proof, introducing explicit |
|
103 |
OFCLASS-premises. On the proof term level, this operation is |
|
104 |
automatically applied at theorem boundaries, such that closed proofs |
|
105 |
are always free of sort constraints. INCOMPATIBILITY for tools that |
|
106 |
inspect proof terms. |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36096
diff
changeset
|
107 |
|
35765
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
108 |
* Local theory specifications may depend on extra type variables that |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
109 |
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
|
110 |
are added internally. For example: |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
111 |
|
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
112 |
definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)" |
09e238561460
local theory specifications handle hidden polymorphism implicitly;
wenzelm
parents:
35763
diff
changeset
|
113 |
|
37351 | 114 |
* Predicates of locales introduced by classes carry a mandatory |
115 |
"class" prefix. INCOMPATIBILITY. |
|
116 |
||
117 |
* Vacuous class specifications observe default sort. INCOMPATIBILITY. |
|
118 |
||
119 |
* Old 'axclass' command has been discontinued. INCOMPATIBILITY, use |
|
120 |
'class' instead. |
|
121 |
||
122 |
* Command 'code_reflect' allows to incorporate generated ML code into |
|
123 |
runtime environment; replaces immature code_datatype antiquotation. |
|
124 |
INCOMPATIBILITY. |
|
125 |
||
126 |
* Code generator: simple concept for abstract datatypes obeying |
|
127 |
invariants. |
|
128 |
||
36857 | 129 |
* Code generator: details of internal data cache have no impact on the |
130 |
user space functionality any longer. |
|
131 |
||
37351 | 132 |
* Methods "unfold_locales" and "intro_locales" ignore non-locale |
133 |
subgoals. This is more appropriate for interpretations with 'where'. |
|
36857 | 134 |
INCOMPATIBILITY. |
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
135 |
|
36356
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36348
diff
changeset
|
136 |
* Command 'example_proof' opens an empty proof body. This allows to |
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36348
diff
changeset
|
137 |
experiment with Isar, without producing any persistent result. |
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36348
diff
changeset
|
138 |
|
35413 | 139 |
* Commands 'type_notation' and 'no_type_notation' declare type syntax |
140 |
within a local theory context, with explicit checking of the |
|
141 |
constructors involved (in contrast to the raw 'syntax' versions). |
|
142 |
||
36178
0e5c133b48b6
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents:
36177
diff
changeset
|
143 |
* Commands 'types' and 'typedecl' now work within a local theory |
0e5c133b48b6
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents:
36177
diff
changeset
|
144 |
context -- without introducing dependencies on parameters or |
0e5c133b48b6
keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents:
36177
diff
changeset
|
145 |
assumptions, which is not possible in Isabelle/Pure. |
35681 | 146 |
|
36857 | 147 |
* Command 'defaultsort' has been renamed to 'default_sort', it works |
148 |
within a local theory context. Minor INCOMPATIBILITY. |
|
36454
f2b5bcc61a8c
command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;
wenzelm
parents:
36446
diff
changeset
|
149 |
|
34170
254ac75e4c38
reduced code generator cache to the baremost minimum; corrected spelling
haftmann
parents:
34076
diff
changeset
|
150 |
|
33993 | 151 |
*** HOL *** |
152 |
||
37351 | 153 |
* Command 'typedef' now works within a local theory context -- without |
154 |
introducing dependencies on parameters or assumptions, which is not |
|
155 |
possible in Isabelle/Pure/HOL. Note that the logical environment may |
|
156 |
contain multiple interpretations of local typedefs (with different |
|
157 |
non-emptiness proofs), even in a global theory context. |
|
158 |
||
159 |
* New package for quotient types. Commands 'quotient_type' and |
|
160 |
'quotient_definition' may be used for defining types and constants by |
|
161 |
quotient constructions. An example is the type of integers created by |
|
162 |
quotienting pairs of natural numbers: |
|
163 |
||
164 |
fun |
|
165 |
intrel :: "(nat * nat) => (nat * nat) => bool" |
|
166 |
where |
|
167 |
"intrel (x, y) (u, v) = (x + v = u + y)" |
|
168 |
||
169 |
quotient_type int = "nat × nat" / intrel |
|
170 |
by (auto simp add: equivp_def expand_fun_eq) |
|
171 |
||
172 |
quotient_definition |
|
173 |
"0::int" is "(0::nat, 0::nat)" |
|
174 |
||
175 |
The method "lifting" can be used to lift of theorems from the |
|
176 |
underlying "raw" type to the quotient type. The example |
|
177 |
src/HOL/Quotient_Examples/FSet.thy includes such a quotient |
|
178 |
construction and provides a reasoning infrastructure for finite sets. |
|
179 |
||
180 |
* Renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid |
|
181 |
clash with new theory Quotient in Main HOL. |
|
182 |
||
183 |
* Moved the SMT binding into the main HOL session, eliminating |
|
184 |
separate HOL-SMT session. |
|
185 |
||
37020 | 186 |
* List membership infix mem operation is only an input abbreviation. |
187 |
INCOMPATIBILITY. |
|
188 |
||
37144 | 189 |
* Theory Library/Word.thy has been removed. Use library Word/Word.thy |
190 |
for future developements; former Library/Word.thy is still present in |
|
191 |
the AFP entry RSAPPS. |
|
36963
9a017146675f
dropped old Library/Word.thy and toy example ex/Adder.thy
haftmann
parents:
36953
diff
changeset
|
192 |
|
36857 | 193 |
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is no |
194 |
longer shadowed. INCOMPATIBILITY. |
|
36808
cbeb3484fa07
theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct
haftmann
parents:
36714
diff
changeset
|
195 |
|
36836
49156805321c
removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents:
36830
diff
changeset
|
196 |
* Dropped theorem duplicate comp_arith; use semiring_norm instead. |
49156805321c
removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents:
36830
diff
changeset
|
197 |
INCOMPATIBILITY. |
49156805321c
removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents:
36830
diff
changeset
|
198 |
|
49156805321c
removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents:
36830
diff
changeset
|
199 |
* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead. |
49156805321c
removed lemma real_sq_order; use power2_le_imp_le instead
huffman
parents:
36830
diff
changeset
|
200 |
INCOMPATIBILITY. |
36714 | 201 |
|
36857 | 202 |
* Dropped normalizing_semiring etc; use the facts in semiring classes |
203 |
instead. INCOMPATIBILITY. |
|
204 |
||
36979
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
205 |
* Dropped several real-specific versions of lemmas about floor and |
37351 | 206 |
ceiling; use the generic lemmas from theory "Archimedean_Field" |
207 |
instead. INCOMPATIBILITY. |
|
36979
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
208 |
|
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
209 |
floor_number_of_eq ~> floor_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
210 |
le_floor_eq_number_of ~> number_of_le_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
211 |
le_floor_eq_zero ~> zero_le_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
212 |
le_floor_eq_one ~> one_le_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
213 |
floor_less_eq_number_of ~> floor_less_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
214 |
floor_less_eq_zero ~> floor_less_zero |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
215 |
floor_less_eq_one ~> floor_less_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
216 |
less_floor_eq_number_of ~> number_of_less_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
217 |
less_floor_eq_zero ~> zero_less_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
218 |
less_floor_eq_one ~> one_less_floor |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
219 |
floor_le_eq_number_of ~> floor_le_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
220 |
floor_le_eq_zero ~> floor_le_zero |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
221 |
floor_le_eq_one ~> floor_le_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
222 |
floor_subtract_number_of ~> floor_diff_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
223 |
floor_subtract_one ~> floor_diff_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
224 |
ceiling_number_of_eq ~> ceiling_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
225 |
ceiling_le_eq_number_of ~> ceiling_le_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
226 |
ceiling_le_zero_eq ~> ceiling_le_zero |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
227 |
ceiling_le_eq_one ~> ceiling_le_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
228 |
less_ceiling_eq_number_of ~> number_of_less_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
229 |
less_ceiling_eq_zero ~> zero_less_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
230 |
less_ceiling_eq_one ~> one_less_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
231 |
ceiling_less_eq_number_of ~> ceiling_less_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
232 |
ceiling_less_eq_zero ~> ceiling_less_zero |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
233 |
ceiling_less_eq_one ~> ceiling_less_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
234 |
le_ceiling_eq_number_of ~> number_of_le_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
235 |
le_ceiling_eq_zero ~> zero_le_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
236 |
le_ceiling_eq_one ~> one_le_ceiling |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
237 |
ceiling_subtract_number_of ~> ceiling_diff_number_of |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
238 |
ceiling_subtract_one ~> ceiling_diff_one |
da7c06ab3169
remove several redundant lemmas about floor and ceiling
huffman
parents:
36972
diff
changeset
|
239 |
|
37144 | 240 |
* Theory "Finite_Set": various folding_XXX locales facilitate the |
36857 | 241 |
application of the various fold combinators on finite sets. |
242 |
||
243 |
* Library theory "RBT" renamed to "RBT_Impl"; new library theory "RBT" |
|
244 |
provides abstract red-black tree type which is backed by "RBT_Impl" as |
|
245 |
implementation. INCOMPATIBILTY. |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36096
diff
changeset
|
246 |
|
36830 | 247 |
* Theory Library/Coinductive_List has been removed -- superseded by |
35763
765f8adf10f9
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
wenzelm
parents:
35745
diff
changeset
|
248 |
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
|
249 |
|
36829 | 250 |
* Theory PReal, including the type "preal" and related operations, has |
251 |
been removed. INCOMPATIBILITY. |
|
252 |
||
37351 | 253 |
* Split off theory "Big_Operators" containing setsum, setprod, |
254 |
Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. |
|
36857 | 255 |
|
256 |
* Theory "Rational" renamed to "Rat", for consistency with "Nat", |
|
257 |
"Int" etc. INCOMPATIBILITY. |
|
258 |
||
37351 | 259 |
* Constant Rat.normalize needs to be qualified. INCOMPATIBILITY. |
37143 | 260 |
|
36857 | 261 |
* New set of rules "ac_simps" provides combined assoc / commute |
262 |
rewrites for all interpretations of the appropriate generic locales. |
|
263 |
||
264 |
* Renamed theory "OrderedGroup" to "Groups" and split theory |
|
265 |
"Ring_and_Field" into theories "Rings" and "Fields"; for more |
|
266 |
appropriate and more consistent names suitable for name prefixes |
|
267 |
within the HOL theories. INCOMPATIBILITY. |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35042
diff
changeset
|
268 |
|
35084 | 269 |
* Some generic constants have been put to appropriate theories: |
36857 | 270 |
- less_eq, less: Orderings |
271 |
- zero, one, plus, minus, uminus, times, abs, sgn: Groups |
|
272 |
- inverse, divide: Rings |
|
35084 | 273 |
INCOMPATIBILITY. |
274 |
||
36857 | 275 |
* More consistent naming of type classes involving orderings (and |
276 |
lattices): |
|
35027
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
277 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
278 |
lower_semilattice ~> semilattice_inf |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
279 |
upper_semilattice ~> semilattice_sup |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
280 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
281 |
dense_linear_order ~> dense_linorder |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
282 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
283 |
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
|
284 |
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
|
285 |
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
|
286 |
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
|
287 |
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
|
288 |
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
|
289 |
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
|
290 |
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
|
291 |
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
|
292 |
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
|
293 |
pordered_ring ~> ordered_ring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
294 |
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
|
295 |
pordered_semiring ~> ordered_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
296 |
|
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
297 |
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
|
298 |
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
|
299 |
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
|
300 |
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
|
301 |
ordered_field ~> linordered_field |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
ordered_idom ~> linordered_idom |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
306 |
ordered_ring ~> linordered_ring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
307 |
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
|
308 |
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
|
309 |
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
|
310 |
ordered_semidom ~> linordered_semidom |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
311 |
ordered_semiring ~> linordered_semiring |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
|
36857 | 316 |
The following slightly odd type classes have been moved to a |
37351 | 317 |
separate theory Library/Lattice_Algebras: |
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
318 |
|
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
319 |
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
|
320 |
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
|
321 |
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
|
322 |
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
|
323 |
lordered_ring ~> lattice_ring |
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
35027
diff
changeset
|
324 |
|
35027
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
325 |
INCOMPATIBILITY. |
ed7d12bcf8f8
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34974
diff
changeset
|
326 |
|
36416 | 327 |
* Refined field classes: |
36857 | 328 |
- classes division_ring_inverse_zero, field_inverse_zero, |
329 |
linordered_field_inverse_zero include rule inverse 0 = 0 -- |
|
330 |
subsumes former division_by_zero class; |
|
331 |
- numerous lemmas have been ported from field to division_ring. |
|
332 |
INCOMPATIBILITY. |
|
36416 | 333 |
|
334 |
* Refined algebra theorem collections: |
|
36857 | 335 |
- dropped theorem group group_simps, use algebra_simps instead; |
336 |
- dropped theorem group ring_simps, use field_simps instead; |
|
337 |
- proper theorem collection field_simps subsumes former theorem |
|
338 |
groups field_eq_simps and field_simps; |
|
339 |
- dropped lemma eq_minus_self_iff which is a duplicate for |
|
340 |
equal_neg_zero. |
|
341 |
INCOMPATIBILITY. |
|
35009 | 342 |
|
343 |
* 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
|
344 |
sets to lattices: |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
345 |
|
34007
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
346 |
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
|
347 |
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
|
348 |
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
|
349 |
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
|
350 |
Inter_fold_inter ~> Inf_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
351 |
Union_fold_union ~> Sup_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
352 |
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
|
353 |
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
|
354 |
INTER_fold_inter ~> INFI_fold_inf |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
355 |
UNION_fold_union ~> SUPR_fold_sup |
aea892559fc5
tuned lattices theory fragements; generlized some lemmas from sets to lattices
haftmann
parents:
33994
diff
changeset
|
356 |
|
37351 | 357 |
* Theory "Complete_Lattice": lemmas top_def and bot_def have been |
36416 | 358 |
replaced by the more convenient lemmas Inf_empty and Sup_empty. |
359 |
Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed |
|
360 |
by Inf_insert and Sup_insert. Lemmas Inf_UNIV and Sup_UNIV replace |
|
361 |
former Inf_Univ and Sup_Univ. Lemmas inf_top_right and sup_bot_right |
|
362 |
subsume inf_top and sup_bot respectively. INCOMPATIBILITY. |
|
363 |
||
36857 | 364 |
* Reorganized theory Multiset: swapped notation of pointwise and |
365 |
multiset order: |
|
37351 | 366 |
|
36857 | 367 |
- pointwise ordering is instance of class order with standard syntax |
368 |
<= and <; |
|
369 |
- multiset ordering has syntax <=# and <#; partial order properties |
|
370 |
are provided by means of interpretation with prefix |
|
371 |
multiset_order; |
|
372 |
- less duplication, less historical organization of sections, |
|
373 |
conversion from associations lists to multisets, rudimentary code |
|
374 |
generation; |
|
375 |
- use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, |
|
376 |
if needed. |
|
37351 | 377 |
|
36903 | 378 |
Renamed: |
37351 | 379 |
|
380 |
multiset_eq_conv_count_eq ~> multiset_ext_iff |
|
381 |
multi_count_ext ~> multiset_ext |
|
382 |
diff_union_inverse2 ~> diff_union_cancelR |
|
383 |
||
36857 | 384 |
INCOMPATIBILITY. |
36416 | 385 |
|
36903 | 386 |
* Theory Permutation: replaced local "remove" by List.remove1. |
387 |
||
36416 | 388 |
* Code generation: ML and OCaml code is decorated with signatures. |
389 |
||
35009 | 390 |
* Theory List: added transpose. |
391 |
||
35810 | 392 |
* Library/Nat_Bijection.thy is a collection of bijective functions |
393 |
between nat and other types, which supersedes the older libraries |
|
394 |
Library/Nat_Int_Bij.thy and HOLCF/NatIso.thy. INCOMPATIBILITY. |
|
395 |
||
396 |
Constants: |
|
397 |
Nat_Int_Bij.nat2_to_nat ~> prod_encode |
|
398 |
Nat_Int_Bij.nat_to_nat2 ~> prod_decode |
|
399 |
Nat_Int_Bij.int_to_nat_bij ~> int_encode |
|
400 |
Nat_Int_Bij.nat_to_int_bij ~> int_decode |
|
401 |
Countable.pair_encode ~> prod_encode |
|
402 |
NatIso.prod2nat ~> prod_encode |
|
403 |
NatIso.nat2prod ~> prod_decode |
|
404 |
NatIso.sum2nat ~> sum_encode |
|
405 |
NatIso.nat2sum ~> sum_decode |
|
406 |
NatIso.list2nat ~> list_encode |
|
407 |
NatIso.nat2list ~> list_decode |
|
408 |
NatIso.set2nat ~> set_encode |
|
409 |
NatIso.nat2set ~> set_decode |
|
410 |
||
411 |
Lemmas: |
|
412 |
Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_decode |
|
413 |
Nat_Int_Bij.nat2_to_nat_inj ~> inj_prod_encode |
|
414 |
Nat_Int_Bij.nat2_to_nat_surj ~> surj_prod_encode |
|
415 |
Nat_Int_Bij.nat_to_nat2_inj ~> inj_prod_decode |
|
416 |
Nat_Int_Bij.nat_to_nat2_surj ~> surj_prod_decode |
|
417 |
Nat_Int_Bij.i2n_n2i_id ~> int_encode_inverse |
|
418 |
Nat_Int_Bij.n2i_i2n_id ~> int_decode_inverse |
|
419 |
Nat_Int_Bij.surj_nat_to_int_bij ~> surj_int_encode |
|
420 |
Nat_Int_Bij.surj_int_to_nat_bij ~> surj_int_decode |
|
421 |
Nat_Int_Bij.inj_nat_to_int_bij ~> inj_int_encode |
|
422 |
Nat_Int_Bij.inj_int_to_nat_bij ~> inj_int_decode |
|
423 |
Nat_Int_Bij.bij_nat_to_int_bij ~> bij_int_encode |
|
424 |
Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode |
|
425 |
||
36929 | 426 |
* Sledgehammer: |
427 |
- Renamed ATP commands: |
|
428 |
atp_info ~> sledgehammer running_atps |
|
429 |
atp_kill ~> sledgehammer kill_atps |
|
430 |
atp_messages ~> sledgehammer messages |
|
431 |
atp_minimize ~> sledgehammer minimize |
|
432 |
print_atps ~> sledgehammer available_atps |
|
433 |
INCOMPATIBILITY. |
|
434 |
- Added user's manual ("isabelle doc sledgehammer"). |
|
435 |
- Added option syntax and "sledgehammer_params" to customize |
|
436 |
Sledgehammer's behavior. See the manual for details. |
|
437 |
- Modified the Isar proof reconstruction code so that it produces |
|
438 |
direct proofs rather than proofs by contradiction. (This feature |
|
439 |
is still experimental.) |
|
440 |
- Made Isar proof reconstruction work for SPASS, remote ATPs, and in |
|
441 |
full-typed mode. |
|
442 |
- Added support for TPTP syntax for SPASS via the "spass_tptp" ATP. |
|
443 |
||
36928 | 444 |
* Nitpick: |
445 |
- Added and implemented "binary_ints" and "bits" options. |
|
446 |
- Added "std" option and implemented support for nonstandard models. |
|
447 |
- Added and implemented "finitize" option to improve the precision |
|
448 |
of infinite datatypes based on a monotonicity analysis. |
|
449 |
- Added support for quotient types. |
|
450 |
- Added support for "specification" and "ax_specification" |
|
451 |
constructs. |
|
452 |
- Added support for local definitions (for "function" and |
|
453 |
"termination" proofs). |
|
454 |
- Added support for term postprocessors. |
|
455 |
- Optimized "Multiset.multiset" and "FinFun.finfun". |
|
456 |
- Improved efficiency of "destroy_constrs" optimization. |
|
457 |
- Fixed soundness bugs related to "destroy_constrs" optimization and |
|
458 |
record getters. |
|
37272 | 459 |
- Fixed soundness bug related to higher-order constructors. |
460 |
- Fixed soundness bug when "full_descrs" is enabled. |
|
36928 | 461 |
- Improved precision of set constructs. |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37158
diff
changeset
|
462 |
- Added "atoms" option. |
36928 | 463 |
- Added cache to speed up repeated Kodkod invocations on the same |
464 |
problems. |
|
465 |
- Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and |
|
466 |
"SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and |
|
467 |
"SAT4J_Light". INCOMPATIBILITY. |
|
468 |
- Removed "skolemize", "uncurry", "sym_break", "flatten_prop", |
|
469 |
"sharing_depth", and "show_skolems" options. INCOMPATIBILITY. |
|
37264
8b931fb51cc6
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
blanchet
parents:
37260
diff
changeset
|
470 |
- Removed "nitpick_intro" attribute. INCOMPATIBILITY. |
36928 | 471 |
|
33993 | 472 |
|
36828 | 473 |
*** HOLCF *** |
474 |
||
475 |
* Variable names in lemmas generated by the domain package have |
|
476 |
changed; the naming scheme is now consistent with the HOL datatype |
|
477 |
package. Some proof scripts may be affected, INCOMPATIBILITY. |
|
478 |
||
479 |
* The domain package no longer defines the function "foo_copy" for |
|
480 |
recursive domain "foo". The reach lemma is now stated directly in |
|
481 |
terms of "foo_take". Lemmas and proofs that mention "foo_copy" must |
|
482 |
be reformulated in terms of "foo_take", INCOMPATIBILITY. |
|
483 |
||
484 |
* Most definedness lemmas generated by the domain package (previously |
|
485 |
of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form |
|
486 |
like "foo$x = UU <-> x = UU", which works better as a simp rule. |
|
37351 | 487 |
Proofs that used definedness lemmas as intro rules may break, |
36828 | 488 |
potential INCOMPATIBILITY. |
489 |
||
490 |
* Induction and casedist rules generated by the domain package now |
|
491 |
declare proper case_names (one called "bottom", and one named for each |
|
492 |
constructor). INCOMPATIBILITY. |
|
493 |
||
494 |
* For mutually-recursive domains, separate "reach" and "take_lemma" |
|
495 |
rules are generated for each domain, INCOMPATIBILITY. |
|
496 |
||
497 |
foo_bar.reach ~> foo.reach bar.reach |
|
498 |
foo_bar.take_lemmas ~> foo.take_lemma bar.take_lemma |
|
499 |
||
500 |
* Some lemmas generated by the domain package have been renamed for |
|
501 |
consistency with the datatype package, INCOMPATIBILITY. |
|
502 |
||
503 |
foo.ind ~> foo.induct |
|
504 |
foo.finite_ind ~> foo.finite_induct |
|
505 |
foo.coind ~> foo.coinduct |
|
506 |
foo.casedist ~> foo.exhaust |
|
507 |
foo.exhaust ~> foo.nchotomy |
|
508 |
||
509 |
* For consistency with other definition packages, the fixrec package |
|
510 |
now generates qualified theorem names, INCOMPATIBILITY. |
|
511 |
||
512 |
foo_simps ~> foo.simps |
|
513 |
foo_unfold ~> foo.unfold |
|
514 |
foo_induct ~> foo.induct |
|
515 |
||
37087 | 516 |
* The "fixrec_simp" attribute has been removed. The "fixrec_simp" |
517 |
method and internal fixrec proofs now use the default simpset instead. |
|
518 |
INCOMPATIBILITY. |
|
519 |
||
36828 | 520 |
* The "contlub" predicate has been removed. Proof scripts should use |
521 |
lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY. |
|
522 |
||
523 |
* The "admw" predicate has been removed, INCOMPATIBILITY. |
|
524 |
||
525 |
* The constants cpair, cfst, and csnd have been removed in favor of |
|
526 |
Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY. |
|
527 |
||
528 |
||
33993 | 529 |
*** ML *** |
530 |
||
37351 | 531 |
* Antiquotations for basic formal entities: |
532 |
||
533 |
@{class NAME} -- type class |
|
534 |
@{class_syntax NAME} -- syntax representation of the above |
|
535 |
||
536 |
@{type_name NAME} -- logical type |
|
537 |
@{type_abbrev NAME} -- type abbreviation |
|
538 |
@{nonterminal NAME} -- type of concrete syntactic category |
|
539 |
@{type_syntax NAME} -- syntax representation of any of the above |
|
540 |
||
541 |
@{const_name NAME} -- logical constant (INCOMPATIBILITY) |
|
542 |
@{const_abbrev NAME} -- abbreviated constant |
|
543 |
@{const_syntax NAME} -- syntax representation of any of the above |
|
544 |
||
545 |
* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw |
|
546 |
syntax constant (cf. 'syntax' command). |
|
547 |
||
548 |
* Antiquotation @{make_string} inlines a function to print arbitrary |
|
549 |
values similar to the ML toplevel. The result is compiler dependent |
|
550 |
and may fall back on "?" in certain situations. |
|
551 |
||
552 |
* Diagnostic commands 'ML_val' and 'ML_command' may refer to |
|
553 |
antiquotations @{Isar.state} and @{Isar.goal}. This replaces impure |
|
554 |
Isar.state() and Isar.goal(), which belong to the old TTY loop and do |
|
555 |
not work with the asynchronous Isar document model. |
|
556 |
||
557 |
* Configuration options now admit dynamic default values, depending on |
|
558 |
the context or even global references. |
|
559 |
||
560 |
* SHA1.digest digests strings according to SHA-1 (see RFC 3174). It |
|
561 |
uses an efficient external library if available (for Poly/ML). |
|
562 |
||
37144 | 563 |
* Renamed some important ML structures, while keeping the old names |
564 |
for some time as aliases within the structure Legacy: |
|
565 |
||
566 |
OuterKeyword ~> Keyword |
|
567 |
OuterLex ~> Token |
|
568 |
OuterParse ~> Parse |
|
569 |
OuterSyntax ~> Outer_Syntax |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37158
diff
changeset
|
570 |
PrintMode ~> Print_Mode |
37144 | 571 |
SpecParse ~> Parse_Spec |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37158
diff
changeset
|
572 |
ThyInfo ~> Thy_Info |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37158
diff
changeset
|
573 |
ThyLoad ~> Thy_Load |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37158
diff
changeset
|
574 |
ThyOutput ~> Thy_Output |
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
37144
diff
changeset
|
575 |
TypeInfer ~> Type_Infer |
37144 | 576 |
|
577 |
Note that "open Legacy" simplifies porting of sources, but forgetting |
|
578 |
to remove it again will complicate porting again in the future. |
|
579 |
||
580 |
* Most operations that refer to a global context are named |
|
581 |
accordingly, e.g. Simplifier.global_context or |
|
582 |
ProofContext.init_global. There are some situations where a global |
|
583 |
context actually works, but under normal circumstances one needs to |
|
584 |
pass the proper local context through the code! |
|
585 |
||
586 |
* Discontinued old TheoryDataFun with its copy/init operation -- data |
|
587 |
needs to be pure. Functor Theory_Data_PP retains the traditional |
|
588 |
Pretty.pp argument to merge, which is absent in the standard |
|
589 |
Theory_Data version. |
|
36429
9d6b3be996d4
monotonic sort certification: sorts are no longer minimized at the kernel boundary, only when reading input from the end-user;
wenzelm
parents:
36416
diff
changeset
|
590 |
|
37144 | 591 |
* Sorts.certify_sort and derived "cert" operations for types and terms |
592 |
no longer minimize sorts. Thus certification at the boundary of the |
|
593 |
inference kernel becomes invariant under addition of class relations, |
|
594 |
which is an important monotonicity principle. Sorts are now minimized |
|
595 |
in the syntax layer only, at the boundary between the end-user and the |
|
596 |
system. Subtle INCOMPATIBILITY, may have to use Sign.minimize_sort |
|
597 |
explicitly in rare situations. |
|
598 |
||
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
|
599 |
* 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
|
600 |
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
|
601 |
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
|
602 |
|
34076
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
603 |
* 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
|
604 |
usual for resolution. Rare INCOMPATIBILITY. |
e3daf3c07381
Subgoal.FOCUS (and variants): resulting goal state is normalized as usual for resolution;
wenzelm
parents:
34062
diff
changeset
|
605 |
|
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35810
diff
changeset
|
606 |
* Renamed varify/unvarify operations to varify_global/unvarify_global |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35810
diff
changeset
|
607 |
to emphasize that these only work in a global situation (which is |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35810
diff
changeset
|
608 |
quite rare). |
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35810
diff
changeset
|
609 |
|
37144 | 610 |
* Curried take and drop in library.ML; negative length is interpreted |
611 |
as infinity (as in chop). Subtle INCOMPATIBILITY. |
|
36961 | 612 |
|
37351 | 613 |
* Proof terms: type substitutions on proof constants now use canonical |
614 |
order of type variables. INCOMPATIBILITY for tools working with proof |
|
615 |
terms. |
|
616 |
||
617 |
* Raw axioms/defs may no longer carry sort constraints, and raw defs |
|
618 |
may no longer carry premises. User-level specifications are |
|
619 |
transformed accordingly by Thm.add_axiom/add_def. |
|
620 |
||
33993 | 621 |
|
34238 | 622 |
*** System *** |
623 |
||
624 |
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; |
|
625 |
ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that |
|
626 |
proof terms are enabled unconditionally in the new HOL-Proofs image. |
|
627 |
||
34255
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
628 |
* Discontinued old ISABELLE and ISATOOL environment settings (legacy |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
629 |
feature since Isabelle2009). Use ISABELLE_PROCESS and ISABELLE_TOOL, |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
630 |
respectively. |
2dd2547acb41
discontinued old ISABELLE and ISATOOL environment settings;
wenzelm
parents:
34238
diff
changeset
|
631 |
|
36201
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
632 |
* Old lib/scripts/polyml-platform is superseded by the |
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
633 |
ISABELLE_PLATFORM setting variable, which defaults to the 32 bit |
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
634 |
variant, even on a 64 bit machine. The following example setting |
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
635 |
prefers 64 bit if available: |
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
636 |
|
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
637 |
ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" |
07d4f74abd12
polyml-platform script is superseded by ISABELLE_PLATFORM;
wenzelm
parents:
36178
diff
changeset
|
638 |
|
37218 | 639 |
* The preliminary Isabelle/jEdit application demonstrates the emerging |
640 |
Isabelle/Scala layer for advanced prover interaction and integration. |
|
641 |
See src/Tools/jEdit or "isabelle jedit" provided by the properly built |
|
642 |
component. |
|
643 |
||
34238 | 644 |
|
33993 | 645 |
|
33842 | 646 |
New in Isabelle2009-1 (December 2009) |
647 |
------------------------------------- |
|
30904 | 648 |
|
31547 | 649 |
*** General *** |
650 |
||
651 |
* Discontinued old form of "escaped symbols" such as \\<forall>. Only |
|
652 |
one backslash should be used, even in ML sources. |
|
653 |
||
654 |
||
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
655 |
*** Pure *** |
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
656 |
|
32846
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
657 |
* Locale interpretation propagates mixins along the locale hierarchy. |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
658 |
The currently only available mixins are the equations used to map |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
659 |
local definitions to terms of the target domain of an interpretation. |
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
660 |
|
33842 | 661 |
* Reactivated diagnostic command 'print_interps'. Use "print_interps |
662 |
loc" to print all interpretations of locale "loc" in the theory. |
|
663 |
Interpretations in proofs are not shown. |
|
32846
29941e925c82
News entry: inheritance of mixins; print_interps.
ballarin
parents:
32775
diff
changeset
|
664 |
|
32983 | 665 |
* Thoroughly revised locales tutorial. New section on conditional |
666 |
interpretation. |
|
667 |
||
33843 | 668 |
* On instantiation of classes, remaining undefined class parameters |
669 |
are formally declared. INCOMPATIBILITY. |
|
670 |
||
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
671 |
|
33842 | 672 |
*** Document preparation *** |
673 |
||
674 |
* New generalized style concept for printing terms: @{foo (style) ...} |
|
675 |
instead of @{foo_style style ...} (old form is still retained for |
|
676 |
backward compatibility). Styles can be also applied for |
|
677 |
antiquotations prop, term_type and typeof. |
|
32891 | 678 |
|
679 |
||
30930 | 680 |
*** HOL *** |
681 |
||
33842 | 682 |
* New proof method "smt" for a combination of first-order logic with |
683 |
equality, linear and nonlinear (natural/integer/real) arithmetic, and |
|
684 |
fixed-size bitvectors; there is also basic support for higher-order |
|
685 |
features (esp. lambda abstractions). It is an incomplete decision |
|
686 |
procedure based on external SMT solvers using the oracle mechanism; |
|
687 |
for the SMT solver Z3, this method is proof-producing. Certificates |
|
688 |
are provided to avoid calling the external solvers solely for |
|
689 |
re-checking proofs. Due to a remote SMT service there is no need for |
|
690 |
installing SMT solvers locally. See src/HOL/SMT. |
|
691 |
||
692 |
* New commands to load and prove verification conditions generated by |
|
693 |
the Boogie program verifier or derived systems (e.g. the Verifying C |
|
694 |
Compiler (VCC) or Spec#). See src/HOL/Boogie. |
|
695 |
||
696 |
* New counterexample generator tool 'nitpick' based on the Kodkod |
|
697 |
relational model finder. See src/HOL/Tools/Nitpick and |
|
698 |
src/HOL/Nitpick_Examples. |
|
699 |
||
33860 | 700 |
* New commands 'code_pred' and 'values' to invoke the predicate |
701 |
compiler and to enumerate values of inductive predicates. |
|
702 |
||
703 |
* A tabled implementation of the reflexive transitive closure. |
|
704 |
||
705 |
* New implementation of quickcheck uses generic code generator; |
|
706 |
default generators are provided for all suitable HOL types, records |
|
707 |
and datatypes. Old quickcheck can be re-activated importing theory |
|
708 |
Library/SML_Quickcheck. |
|
709 |
||
33843 | 710 |
* New testing tool Mirabelle for automated proof tools. Applies |
711 |
several tools and tactics like sledgehammer, metis, or quickcheck, to |
|
712 |
every proof step in a theory. To be used in batch mode via the |
|
713 |
"mirabelle" utility. |
|
714 |
||
715 |
* New proof method "sos" (sum of squares) for nonlinear real |
|
716 |
arithmetic (originally due to John Harison). It requires theory |
|
717 |
Library/Sum_Of_Squares. It is not a complete decision procedure but |
|
718 |
works well in practice on quantifier-free real arithmetic with +, -, |
|
719 |
*, ^, =, <= and <, i.e. boolean combinations of equalities and |
|
720 |
inequalities between polynomials. It makes use of external |
|
721 |
semidefinite programming solvers. Method "sos" generates a |
|
722 |
certificate that can be pasted into the proof thus avoiding the need |
|
723 |
to call an external tool every time the proof is checked. See |
|
724 |
src/HOL/Library/Sum_Of_Squares. |
|
725 |
||
726 |
* New method "linarith" invokes existing linear arithmetic decision |
|
727 |
procedure only. |
|
728 |
||
729 |
* New command 'atp_minimal' reduces result produced by Sledgehammer. |
|
730 |
||
731 |
* New Sledgehammer option "Full Types" in Proof General settings menu. |
|
732 |
Causes full type information to be output to the ATPs. This slows |
|
733 |
ATPs down considerably but eliminates a source of unsound "proofs" |
|
734 |
that fail later. |
|
735 |
||
736 |
* New method "metisFT": A version of metis that uses full type |
|
737 |
information in order to avoid failures of proof reconstruction. |
|
738 |
||
739 |
* New evaluator "approximate" approximates an real valued term using |
|
740 |
the same method as the approximation method. |
|
741 |
||
742 |
* Method "approximate" now supports arithmetic expressions as |
|
743 |
boundaries of intervals and implements interval splitting and Taylor |
|
744 |
series expansion. |
|
745 |
||
746 |
* ML antiquotation @{code_datatype} inserts definition of a datatype |
|
747 |
generated by the code generator; e.g. see src/HOL/Predicate.thy. |
|
748 |
||
33860 | 749 |
* New theory SupInf of the supremum and infimum operators for sets of |
750 |
reals. |
|
751 |
||
752 |
* New theory Probability, which contains a development of measure |
|
753 |
theory, eventually leading to Lebesgue integration and probability. |
|
754 |
||
755 |
* Extended Multivariate Analysis to include derivation and Brouwer's |
|
756 |
fixpoint theorem. |
|
33843 | 757 |
|
33842 | 758 |
* Reorganization of number theory, INCOMPATIBILITY: |
33873 | 759 |
- new number theory development for nat and int, in theories Divides |
760 |
and GCD as well as in new session Number_Theory |
|
761 |
- some constants and facts now suffixed with _nat and _int |
|
762 |
accordingly |
|
763 |
- former session NumberTheory now named Old_Number_Theory, including |
|
764 |
theories Legacy_GCD and Primes (prefer Number_Theory if possible) |
|
33842 | 765 |
- moved theory Pocklington from src/HOL/Library to |
766 |
src/HOL/Old_Number_Theory |
|
32479 | 767 |
|
33873 | 768 |
* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and |
769 |
lcm of finite and infinite sets. It is shown that they form a complete |
|
32600 | 770 |
lattice. |
771 |
||
772 |
* Class semiring_div requires superclass no_zero_divisors and proof of |
|
773 |
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2, |
|
774 |
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been |
|
775 |
generalized to class semiring_div, subsuming former theorems |
|
776 |
zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and |
|
777 |
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. |
|
778 |
INCOMPATIBILITY. |
|
779 |
||
32588
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
780 |
* Refinements to lattice classes and sets: |
32064 | 781 |
- less default intro/elim rules in locale variant, more default |
782 |
intro/elim rules in class variant: more uniformity |
|
33842 | 783 |
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with |
784 |
le_inf_iff |
|
785 |
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and |
|
786 |
sup_aci) |
|
32064 | 787 |
- renamed ACI to inf_sup_aci |
32600 | 788 |
- new class "boolean_algebra" |
33842 | 789 |
- class "complete_lattice" moved to separate theory |
33860 | 790 |
"Complete_Lattice"; corresponding constants (and abbreviations) |
33842 | 791 |
renamed and with authentic syntax: |
33860 | 792 |
Set.Inf ~> Complete_Lattice.Inf |
793 |
Set.Sup ~> Complete_Lattice.Sup |
|
794 |
Set.INFI ~> Complete_Lattice.INFI |
|
795 |
Set.SUPR ~> Complete_Lattice.SUPR |
|
796 |
Set.Inter ~> Complete_Lattice.Inter |
|
797 |
Set.Union ~> Complete_Lattice.Union |
|
798 |
Set.INTER ~> Complete_Lattice.INTER |
|
799 |
Set.UNION ~> Complete_Lattice.UNION |
|
32600 | 800 |
- authentic syntax for |
801 |
Set.Pow |
|
802 |
Set.image |
|
32588
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
803 |
- mere abbreviations: |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
804 |
Set.empty (for bot) |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
805 |
Set.UNIV (for top) |
33860 | 806 |
Set.inter (for inf, formerly Set.Int) |
807 |
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
|
808 |
Complete_Lattice.Inter (for Inf) |
5e06a1634e55
Inter and Union are mere abbreviations for Inf and Sup; tuned
haftmann
parents:
32485
diff
changeset
|
809 |
Complete_Lattice.Union (for Sup) |
32606
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32600
diff
changeset
|
810 |
Complete_Lattice.INTER (for INFI) |
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32600
diff
changeset
|
811 |
Complete_Lattice.UNION (for SUPR) |
32600 | 812 |
- object-logic definitions as far as appropriate |
32217 | 813 |
|
32691 | 814 |
INCOMPATIBILITY. Care is required when theorems Int_subset_iff or |
33842 | 815 |
Un_subset_iff are explicitly deleted as default simp rules; then also |
816 |
their lattice counterparts le_inf_iff and le_sup_iff have to be |
|
32691 | 817 |
deleted to achieve the desired effect. |
32064 | 818 |
|
33842 | 819 |
* Rules inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp |
820 |
rules by default any longer; the same applies to min_max.inf_absorb1 |
|
821 |
etc. INCOMPATIBILITY. |
|
822 |
||
823 |
* Rules sup_Int_eq and sup_Un_eq are no longer declared as |
|
824 |
pred_set_conv by default. INCOMPATIBILITY. |
|
825 |
||
826 |
* Power operations on relations and functions are now one dedicated |
|
32706 | 827 |
constant "compow" with infix syntax "^^". Power operation on |
31547 | 828 |
multiplicative monoids retains syntax "^" and is now defined generic |
829 |
in class power. INCOMPATIBILITY. |
|
830 |
||
33842 | 831 |
* Relation composition "R O S" now has a more standard argument order: |
832 |
"R O S = {(x, z). EX y. (x, y) : R & (y, z) : S}". INCOMPATIBILITY, |
|
833 |
rewrite propositions with "S O R" --> "R O S". Proofs may occasionally |
|
834 |
break, since the O_assoc rule was not rewritten like this. Fix using |
|
835 |
O_assoc[symmetric]. The same applies to the curried version "R OO S". |
|
32427 | 836 |
|
33057 | 837 |
* Function "Inv" is renamed to "inv_into" and function "inv" is now an |
33842 | 838 |
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. |
32988 | 839 |
INCOMPATIBILITY. |
840 |
||
33860 | 841 |
* Most rules produced by inductive and datatype package have mandatory |
842 |
prefixes. INCOMPATIBILITY. |
|
31790 | 843 |
|
33842 | 844 |
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by |
845 |
the attribute of the same name. Each of the theorems in the list |
|
846 |
DERIV_intros assumes composition with an additional function and |
|
847 |
matches a variable to the derivative, which has to be solved by the |
|
848 |
Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative |
|
33873 | 849 |
of most elementary terms. Former Maclauren.DERIV_tac and |
850 |
Maclauren.deriv_tac should be replaced by (auto intro!: DERIV_intros). |
|
851 |
INCOMPATIBILITY. |
|
33860 | 852 |
|
853 |
* Code generator attributes follow the usual underscore convention: |
|
854 |
code_unfold replaces code unfold |
|
855 |
code_post replaces code post |
|
856 |
etc. |
|
857 |
INCOMPATIBILITY. |
|
31900 | 858 |
|
33471 | 859 |
* Renamed methods: |
860 |
sizechange -> size_change |
|
861 |
induct_scheme -> induction_schema |
|
33860 | 862 |
INCOMPATIBILITY. |
33673 | 863 |
|
33843 | 864 |
* Discontinued abbreviation "arbitrary" of constant "undefined". |
865 |
INCOMPATIBILITY, use "undefined" directly. |
|
866 |
||
33860 | 867 |
* Renamed theorems: |
868 |
Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
|
869 |
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
|
870 |
Suc_plus1 -> Suc_eq_plus1 |
|
871 |
*anti_sym -> *antisym* |
|
872 |
vector_less_eq_def -> vector_le_def |
|
873 |
INCOMPATIBILITY. |
|
874 |
||
875 |
* Added theorem List.map_map as [simp]. Removed List.map_compose. |
|
876 |
INCOMPATIBILITY. |
|
877 |
||
878 |
* Removed predicate "M hassize n" (<--> card M = n & finite M). |
|
879 |
INCOMPATIBILITY. |
|
880 |
||
31812 | 881 |
|
33825 | 882 |
*** HOLCF *** |
883 |
||
33842 | 884 |
* Theory Representable defines a class "rep" of domains that are |
885 |
representable (via an ep-pair) in the universal domain type "udom". |
|
33825 | 886 |
Instances are provided for all type constructors defined in HOLCF. |
887 |
||
888 |
* The 'new_domain' command is a purely definitional version of the |
|
889 |
domain package, for representable domains. Syntax is identical to the |
|
890 |
old domain package. The 'new_domain' package also supports indirect |
|
891 |
recursion using previously-defined type constructors. See |
|
33842 | 892 |
src/HOLCF/ex/New_Domain.thy for examples. |
893 |
||
894 |
* Method "fixrec_simp" unfolds one step of a fixrec-defined constant |
|
33825 | 895 |
on the left-hand side of an equation, and then performs |
896 |
simplification. Rewriting is done using rules declared with the |
|
33842 | 897 |
"fixrec_simp" attribute. The "fixrec_simp" method is intended as a |
898 |
replacement for "fixpat"; see src/HOLCF/ex/Fixrec_ex.thy for examples. |
|
33825 | 899 |
|
900 |
* The pattern-match compiler in 'fixrec' can now handle constructors |
|
901 |
with HOL function types. Pattern-match combinators for the Pair |
|
902 |
constructor are pre-configured. |
|
903 |
||
904 |
* The 'fixrec' package now produces better fixed-point induction rules |
|
905 |
for mutually-recursive definitions: Induction rules have conclusions |
|
906 |
of the form "P foo bar" instead of "P <foo, bar>". |
|
907 |
||
908 |
* The constant "sq_le" (with infix syntax "<<" or "\<sqsubseteq>") has |
|
909 |
been renamed to "below". The name "below" now replaces "less" in many |
|
33842 | 910 |
theorem names. (Legacy theorem names using "less" are still supported |
911 |
as well.) |
|
33825 | 912 |
|
913 |
* The 'fixrec' package now supports "bottom patterns". Bottom |
|
914 |
patterns can be used to generate strictness rules, or to make |
|
915 |
functions more strict (much like the bang-patterns supported by the |
|
33873 | 916 |
Glasgow Haskell Compiler). See src/HOLCF/ex/Fixrec_ex.thy for |
917 |
examples. |
|
33825 | 918 |
|
919 |
||
31304 | 920 |
*** ML *** |
921 |
||
33843 | 922 |
* Support for Poly/ML 5.3.0, with improved reporting of compiler |
923 |
errors and run-time exceptions, including detailed source positions. |
|
924 |
||
925 |
* Structure Name_Space (formerly NameSpace) now manages uniquely |
|
926 |
identified entries, with some additional information such as source |
|
927 |
position, logical grouping etc. |
|
928 |
||
33524
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
929 |
* 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
|
930 |
modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
931 |
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
|
932 |
copy operation) is still available for some time. |
a08e6c1cbc04
updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm
parents:
33472
diff
changeset
|
933 |
|
32742 | 934 |
* Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) |
935 |
provides a high-level programming interface to synchronized state |
|
936 |
variables with atomic update. This works via pure function |
|
937 |
application within a critical section -- its runtime should be as |
|
938 |
short as possible; beware of deadlocks if critical code is nested, |
|
939 |
either directly or indirectly via other synchronized variables! |
|
940 |
||
941 |
* Structure Unsynchronized (cf. src/Pure/ML-Systems/unsynchronized.ML) |
|
942 |
wraps raw ML references, explicitly indicating their non-thread-safe |
|
943 |
behaviour. The Isar toplevel keeps this structure open, to |
|
944 |
accommodate Proof General as well as quick and dirty interactive |
|
945 |
experiments with references. |
|
946 |
||
32365 | 947 |
* PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for |
948 |
parallel tactical reasoning. |
|
949 |
||
32427 | 950 |
* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS |
951 |
are similar to SUBPROOF, but are slightly more flexible: only the |
|
952 |
specified parts of the subgoal are imported into the context, and the |
|
953 |
body tactic may introduce new subgoals and schematic variables. |
|
954 |
||
955 |
* Old tactical METAHYPS, which does not observe the proof context, has |
|
956 |
been renamed to Old_Goals.METAHYPS and awaits deletion. Use SUBPROOF |
|
957 |
or Subgoal.FOCUS etc. |
|
32216 | 958 |
|
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
959 |
* 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
|
960 |
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
|
961 |
separately.) Minor INCOMPATIBILITY. |
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31901
diff
changeset
|
962 |
|
31901 | 963 |
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY. |
964 |
||
33842 | 965 |
* Renamed several structures FooBar to Foo_Bar. Occasional, |
966 |
INCOMPATIBILITY. |
|
967 |
||
33843 | 968 |
* Operations of structure Skip_Proof no longer require quick_and_dirty |
969 |
mode, which avoids critical setmp. |
|
970 |
||
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
971 |
* Eliminated old Attrib.add_attributes, Method.add_methods and related |
33842 | 972 |
combinators for "args". INCOMPATIBILITY, need to use simplified |
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
973 |
Attrib/Method.setup introduced in Isabelle2009. |
31304 | 974 |
|
32151
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
975 |
* 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
|
976 |
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
|
977 |
last resort. INCOMPATIBILITY. |
2f65c45c2e7e
Proper context for simpset_of, claset_of, clasimpset_of.
wenzelm
parents:
32136
diff
changeset
|
978 |
|
32092
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
979 |
* Display.pretty_thm now requires a proper context (cf. former |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
980 |
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
|
981 |
or even Display.pretty_thm_without_context as last resort. |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
982 |
INCOMPATIBILITY. |
6a5995438266
Display.pretty_thm now requires a proper context;
wenzelm
parents:
32079
diff
changeset
|
983 |
|
32433 | 984 |
* Discontinued Display.pretty_ctyp/cterm etc. INCOMPATIBILITY, use |
985 |
Syntax.pretty_typ/term directly, preferably with proper context |
|
986 |
instead of global theory. |
|
987 |
||
31304 | 988 |
|
31308 | 989 |
*** System *** |
990 |
||
33842 | 991 |
* Further fine tuning of parallel proof checking, scales up to 8 cores |
992 |
(max. speedup factor 5.0). See also Goal.parallel_proofs in ML and |
|
993 |
usedir option -q. |
|
994 |
||
32326 | 995 |
* Support for additional "Isabelle components" via etc/components, see |
996 |
also the system manual. |
|
997 |
||
998 |
* The isabelle makeall tool now operates on all components with |
|
999 |
IsaMakefile, not just hardwired "logics". |
|
1000 |
||
33842 | 1001 |
* Removed "compress" option from isabelle-process and isabelle usedir; |
1002 |
this is always enabled. |
|
33818 | 1003 |
|
31308 | 1004 |
* Discontinued support for Poly/ML 4.x versions. |
1005 |
||
33842 | 1006 |
* Isabelle tool "wwwfind" provides web interface for 'find_theorems' |
1007 |
on a given logic image. This requires the lighttpd webserver and is |
|
1008 |
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
|
1009 |
|
31308 | 1010 |
|
31304 | 1011 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1012 |
New in Isabelle2009 (April 2009) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1013 |
-------------------------------- |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1014 |
|
27599 | 1015 |
*** General *** |
1016 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1017 |
* 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
|
1018 |
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
|
1019 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1020 |
- 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
|
1021 |
"isatool." |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1022 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1023 |
- 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
|
1024 |
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
|
1025 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
1026 |
- 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
|
1027 |
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
|
1028 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1029 |
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
|
1030 |
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
|
1031 |
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
|
1032 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
1033 |
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
|
1034 |
the interface was uninstalled or changed otherwise. Individual |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
1035 |
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
|
1036 |
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
|
1037 |
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
|
1038 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
1039 |
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
|
1040 |
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
|
1041 |
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
|
1042 |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
1043 |
* 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
|
1044 |
old ~/isabelle, which was slightly non-standard and apt to cause |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1045 |
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
|
1046 |
|
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
1047 |
INCOMPATIBILITY, need to move existing ~/isabelle/etc, |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
1048 |
~/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
|
1049 |
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
|
1050 |
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
|
1051 |
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
|
1052 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
1053 |
* Proofs of fully specified statements are run in parallel on |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1054 |
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
|
1055 |
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
|
1056 |
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
|
1057 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1058 |
* The main reference manuals ("isar-ref", "implementation", and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1059 |
"system") have been updated and extended. Formally checked references |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1060 |
as hyperlinks are now available uniformly. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1061 |
|
30163
faf95eb3f375
* New prover for coherent logic (see src/Tools/coherent.ML).
wenzelm
parents:
30106
diff
changeset
|
1062 |
|
27599 | 1063 |
*** Pure *** |
1064 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1065 |
* Complete re-implementation of locales. INCOMPATIBILITY in several |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1066 |
respects. The most important changes are listed below. See the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1067 |
Tutorial on Locales ("locales" manual) for details. |
29253 | 1068 |
|
1069 |
- In locale expressions, instantiation replaces renaming. Parameters |
|
1070 |
must be declared in a for clause. To aid compatibility with previous |
|
1071 |
parameter inheritance, in locale declarations, parameters that are not |
|
1072 |
'touched' (instantiation position "_" or omitted) are implicitly added |
|
1073 |
with their syntax at the beginning of the for clause. |
|
1074 |
||
1075 |
- Syntax from abbreviations and definitions in locales is available in |
|
1076 |
locale expressions and context elements. The latter is particularly |
|
1077 |
useful in locale declarations. |
|
1078 |
||
1079 |
- More flexible mechanisms to qualify names generated by locale |
|
1080 |
expressions. Qualifiers (prefixes) may be specified in locale |
|
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1081 |
expressions, and can be marked as mandatory (syntax: "name!:") or |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1082 |
optional (syntax "name?:"). The default depends for plain "name:" |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1083 |
depends on the situation where a locale expression is used: in |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1084 |
commands 'locale' and 'sublocale' prefixes are optional, in |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1085 |
'interpretation' and 'interpret' prefixes are mandatory. The old |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1086 |
implicit qualifiers derived from the parameter names of a locale are |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1087 |
no longer generated. |
30106 | 1088 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1089 |
- Command "sublocale l < e" replaces "interpretation l < e". The |
30106 | 1090 |
instantiation clause in "interpretation" and "interpret" (square |
1091 |
brackets) is no longer available. Use locale expressions. |
|
29253 | 1092 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1093 |
- When converting proof scripts, mandatory qualifiers in |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
1094 |
'interpretation' and 'interpret' should be retained by default, even |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1095 |
if this is an INCOMPATIBILITY compared to former behavior. In the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1096 |
worst case, use the "name?:" form for non-mandatory ones. Qualifiers |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1097 |
in locale expressions range over a single locale instance only. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1098 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1099 |
- Dropped locale element "includes". This is a major INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1100 |
In existing theorem specifications replace the includes element by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1101 |
respective context elements of the included locale, omitting those |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1102 |
that are already present in the theorem specification. Multiple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1103 |
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
|
1104 |
involving the locale predicate. In the proof body, declarations (most |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1105 |
notably theorems) may be regained by interpreting the respective |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1106 |
locales in the proof context as required (command "interpret"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1107 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1108 |
If using "includes" in replacement of a target solely because the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1109 |
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
|
1110 |
consider declaring a new locale with additional type constraints on |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1111 |
the parameters (context element "constrains"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1112 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1113 |
- Discontinued "locale (open)". INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1114 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1115 |
- Locale interpretation commands no longer attempt to simplify goal. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1116 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1117 |
methods intro_locales and unfold_locales to clarify. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1118 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1119 |
- Locale interpretation commands no longer accept interpretation |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1120 |
attributes. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1121 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1122 |
* 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
|
1123 |
list any longer, but is inferred from the specification. Particularly |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1124 |
in HOL, write |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1125 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1126 |
class foo = ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1127 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1128 |
instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1129 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1130 |
class foo = type + ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1131 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1132 |
* Class target: global versions of theorems stemming do not carry a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1133 |
parameter prefix any longer. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1134 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1135 |
* Class 'instance' command no longer accepts attached definitions. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1136 |
INCOMPATIBILITY, use proper 'instantiation' target instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1137 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1138 |
* Recovered hiding of consts, which was accidentally broken in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1139 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1140 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1141 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1142 |
* Slightly more coherent Pure syntax, with updated documentation in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1143 |
isar-ref manual. Removed locales meta_term_syntax and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1144 |
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1145 |
INCOMPATIBILITY in rare situations. Note that &&& should not be used |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1146 |
directly in regular applications. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1147 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1148 |
* There is a new syntactic category "float_const" for signed decimal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1149 |
fractions (e.g. 123.45 or -123.45). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1150 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1151 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1152 |
interface with 'setup' command instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1153 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1154 |
* 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
|
1155 |
theory context. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1156 |
|
28114 | 1157 |
* The 'axiomatization' command now only works within a global theory |
1158 |
context. INCOMPATIBILITY. |
|
1159 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1160 |
* Goal-directed proof now enforces strict proof irrelevance wrt. sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1161 |
hypotheses. Sorts required in the course of reasoning need to be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1162 |
covered by the constraints in the initial statement, completed by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1163 |
type instance information of the background theory. Non-trivial sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1164 |
hypotheses, which rarely occur in practice, may be specified via |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1165 |
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1166 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1167 |
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
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 |
The result contains an implicit sort hypotheses as before -- |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1170 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1171 |
normalization. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1172 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1173 |
* Generalized Isar history, with support for linear undo, direct state |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1174 |
addressing etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1175 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1176 |
* Changed defaults for unify configuration options: |
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 |
unify_trace_bound = 50 (formerly 25) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1179 |
unify_search_bound = 60 (formerly 30) |
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 |
* Different bookkeeping for code equations (INCOMPATIBILITY): |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1182 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1183 |
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
|
1184 |
constant is taken (in accordance with the policy applied by other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1185 |
parts of the code generator framework). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1186 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1187 |
b) Code equations stemming from explicit declarations (e.g. code |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1188 |
attribute) gain priority over default code equations stemming |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1189 |
from definition, primrec, fun etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1190 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1191 |
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1192 |
|
30965 | 1193 |
* Unified theorem tables for both code generators. Thus [code |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1194 |
func] has disappeared and only [code] remains. INCOMPATIBILITY. |
30577 | 1195 |
|
1196 |
* Command 'find_consts' searches for constants based on type and name |
|
1197 |
patterns, e.g. |
|
29883 | 1198 |
|
1199 |
find_consts "_ => bool" |
|
1200 |
||
30106 | 1201 |
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
|
1202 |
the whole type. Searching by name is possible. Multiple queries are |
30106 | 1203 |
conjunctive and queries may be negated by prefixing them with a |
1204 |
hyphen: |
|
29883 | 1205 |
|
1206 |
find_consts strict: "_ => bool" name: "Int" -"int => int" |
|
29861
3c348f5873f3
updated NEWS etc with "solves" criterion and auto_solves
kleing
parents:
29823
diff
changeset
|
1207 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1208 |
* New 'find_theorems' criterion "solves" matches theorems that |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1209 |
directly solve the current goal (modulo higher-order unification). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1210 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1211 |
* Auto solve feature for main theorem statements: whenever a new goal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1212 |
is stated, "find_theorems solves" is called; any theorems that could |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1213 |
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
|
1214 |
Cf. associated options in Proof General Isabelle settings menu, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1215 |
enabled by default, with reasonable timeout for pathological cases of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1216 |
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
|
1217 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1218 |
|
27381 | 1219 |
*** Document preparation *** |
1220 |
||
1221 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 1222 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
1223 |
syntax just like the Isar command 'by'. |
27381 | 1224 |
|
1225 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1226 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
1227 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1228 |
* Integrated main parts of former image HOL-Complex with HOL. Entry |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1229 |
points Main and Complex_Main remain as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1230 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1231 |
* 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
|
1232 |
tools available (inductive, datatype, primrec, ...). This facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1233 |
experimentation and tool development. Note that user applications |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1234 |
(and library theories) should never refer to anything below theory |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1235 |
Main, as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1236 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1237 |
* Logic image HOL-Main stops at theory Main, and thus facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1238 |
experimentation due to shorter build times. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1239 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1240 |
* Logic image HOL-NSA contains theories of nonstandard analysis which |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1241 |
were previously part of former HOL-Complex. Entry point Hyperreal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1242 |
remains valid, but theories formerly using Complex_Main should now use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1243 |
new entry point Hypercomplex. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1244 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1245 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1246 |
Posix processes. Avoids potentially expensive forking of the ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1247 |
process. New thread-based implementation also works on non-Unix |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1248 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1249 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1250 |
commands are covered in the isar-ref manual. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1251 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1252 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1253 |
sledgehammer without local ATP installation (Vampire etc.). Other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1254 |
provers may be included via suitable ML wrappers, see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1255 |
src/HOL/ATP_Linkup.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1256 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1257 |
* 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
|
1258 |
menu. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1259 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1260 |
* 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
|
1261 |
(contains the empty clause). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1262 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1263 |
* 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
|
1264 |
an exception, if it determines that it cannot prove the theorem. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1265 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1266 |
* Method "coherent" implements a prover for coherent logic (see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1267 |
src/Tools/coherent.ML). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1268 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1269 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1270 |
"undefined" is the right choice to replace "arbitrary", though |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1271 |
logically there is no difference. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1272 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1273 |
* Command "value" now integrates different evaluation mechanisms. The |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1274 |
result of the first successful evaluation mechanism is printed. In |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1275 |
square brackets a particular named evaluation mechanisms may be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1276 |
specified (currently, [SML], [code] or [nbe]). See further |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1277 |
src/HOL/ex/Eval_Examples.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1278 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1279 |
* Normalization by evaluation now allows non-leftlinear equations. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1280 |
Declare with attribute [code nbe]. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1281 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1282 |
* 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
|
1283 |
as the structured Isar versions "cases" and "induct", cf. the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1284 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1285 |
are now presented as a list of individual projections |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1286 |
(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
|
1287 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1288 |
rare situations a different rule is selected --- notably nested tuple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1289 |
elimination instead of former prod.exhaust: use explicit (case_tac t |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1290 |
rule: prod.exhaust) here. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1291 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1292 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1293 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1294 |
* Removed fact "case_split_thm", which duplicates "case_split". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1295 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1296 |
* 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
|
1297 |
option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY. |
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 |
* New predicate "strict_mono" classifies strict functions on partial |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1300 |
orders. With strict functions on linear orders, reasoning about |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1301 |
(in)equalities is facilitated by theorems "strict_mono_eq", |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1302 |
"strict_mono_less_eq" and "strict_mono_less". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1303 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1304 |
* Some set operations are now proper qualified constants with |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1305 |
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
|
1306 |
|
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
1307 |
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
|
1308 |
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
|
1309 |
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
|
1310 |
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
|
1311 |
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
|
1312 |
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
|
1313 |
{} ~> 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
|
1314 |
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
|
1315 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1316 |
* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1317 |
theory Set. |
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 |
* Auxiliary class "itself" has disappeared -- classes without any |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1320 |
parameter are treated as expected by the 'class' command. |
29797 | 1321 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
1322 |
* 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
|
1323 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1324 |
* Common decision procedures (Cooper, MIR, Ferrack, Approximation, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1325 |
Dense_Linear_Order) are now in directory HOL/Decision_Procs. |
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 |
* Theory src/HOL/Decision_Procs/Approximation provides the new proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1328 |
method "approximation". It proves formulas on real values by using |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1329 |
interval arithmetic. In the formulas are also the transcendental |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1330 |
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
|
1331 |
allowed. For examples see |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1332 |
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
|
1333 |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
1334 |
* Theory "Reflection" now resides in HOL/Library. |
29650 | 1335 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1336 |
* Entry point to Word library now simply named "Word". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1337 |
INCOMPATIBILITY. |
29628 | 1338 |
|
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1339 |
* Made source layout more coherent with logical distribution |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1340 |
structure: |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1341 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1342 |
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
|
1343 |
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
|
1344 |
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
|
1345 |
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
|
1346 |
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
|
1347 |
src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1348 |
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
|
1349 |
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
|
1350 |
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
|
1351 |
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
|
1352 |
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
|
1353 |
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
|
1354 |
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
|
1355 |
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
|
1356 |
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
|
1357 |
src/HOL/Complex/Complex.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1358 |
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/ |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
1359 |
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
|
1360 |
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
|
1361 |
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
|
1362 |
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
|
1363 |
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
|
1364 |
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
|
1365 |
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
|
1366 |
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
|
1367 |
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
|
1368 |
src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1369 |
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
|
1370 |
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
|
1371 |
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
|
1372 |
src/HOL/Real/Float ~> src/HOL/Library/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1373 |
src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
1374 |
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
|
1375 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
1376 |
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
|
1377 |
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
|
1378 |
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
|
1379 |
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
|
1380 |
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
|
1381 |
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
|
1382 |
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
|
1383 |
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
|
1384 |
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
|
1385 |
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
|
1386 |
|
29398 | 1387 |
src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL |
1388 |
src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL |
|
1389 |
src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL |
|
1390 |
src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL |
|
1391 |
src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL |
|
1392 |
src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL |
|
1393 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1394 |
* If methods "eval" and "evaluation" encounter a structured proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1395 |
state with !!/==>, only the conclusion is evaluated to True (if |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1396 |
possible), avoiding strange error messages. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1397 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1398 |
* Method "sizechange" automates termination proofs using (a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1399 |
modification of) the size-change principle. Requires SAT solver. See |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1400 |
src/HOL/ex/Termination.thy for examples. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1401 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1402 |
* Simplifier: simproc for let expressions now unfolds if bound |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1403 |
variable occurs at most once in let expression body. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1404 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1405 |
* Method "arith": Linear arithmetic now ignores all inequalities when |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
1406 |
fast_arith_neq_limit is exceeded, instead of giving up entirely. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 releas |