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