author | krauss |
Sat, 27 Dec 2008 17:35:01 +0100 | |
changeset 29182 | 9304afad825e |
parent 29162 | bad036eb71c4 |
child 29197 | 6d4cb27ed19c |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
27122 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
6 |
|
27599 | 7 |
*** General *** |
8 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
9 |
* 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
|
10 |
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
|
11 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
12 |
- 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
|
13 |
"isatool." |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
14 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
15 |
- 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
|
16 |
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
|
17 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
18 |
- 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
|
19 |
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
|
20 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
25 |
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
|
26 |
the interface was uninstalled or changed otherwise. Individual |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
35 |
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
36 |
old ~/isabelle, which was slightly non-standard and apt cause |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
37 |
surprises on case-insensitive file-systems. |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
38 |
|
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
39 |
INCOMPATIBILITY, need to move existing ~/isabelle/etc, |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
40 |
~/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
|
41 |
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
|
42 |
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
43 |
Isabelle distribution. |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
44 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
45 |
* Proofs of fully specified statements are run in parallel on |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
46 |
multi-core systems. A speedup factor of 2-3 can be expected on a |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
47 |
regular 4-core machine, if the initial heap space is made reasonably |
29162 | 48 |
large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later] |
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
49 |
|
28252 | 50 |
* The Isabelle System Manual (system) has been updated, with formally |
51 |
checked references as hyperlinks. |
|
52 |
||
27599 | 53 |
* Generalized Isar history, with support for linear undo, direct state |
54 |
addressing etc. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
55 |
|
27191 | 56 |
* Recovered hiding of consts, which was accidentally broken in |
57 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
|
58 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
|
59 |
||
27599 | 60 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
61 |
interface instead. |
|
62 |
||
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
63 |
* There is a new syntactic category "float_const" for signed decimal |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
64 |
fractions (e.g. 123.45 or -123.45). |
28964 | 65 |
|
27599 | 66 |
|
67 |
*** Pure *** |
|
68 |
||
28965 | 69 |
* Type Binding.T gradually replaces formerly used type bstring for names |
70 |
to be bound. Name space interface for declarations has been simplified: |
|
71 |
||
72 |
NameSpace.declare: NameSpace.naming |
|
73 |
-> Binding.T -> NameSpace.T -> string * NameSpace.T |
|
74 |
NameSpace.bind: NameSpace.naming |
|
75 |
-> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table |
|
76 |
(*exception Symtab.DUP*) |
|
77 |
||
78 |
See further modules src/Pure/General/binding.ML and |
|
79 |
src/Pure/General/name_space.ML |
|
80 |
||
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
81 |
* Module moves in repository: |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
82 |
src/Pure/Tools/value.ML ~> src/Tools/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
83 |
src/Pure/Tools/quickcheck.ML ~> src/Tools/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
84 |
|
28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
85 |
* Slightly more coherent Pure syntax, with updated documentation in |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
86 |
isar-ref manual. Removed locales meta_term_syntax and |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
87 |
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
88 |
INCOMPATIBILITY in rare situations. |
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28855
diff
changeset
|
89 |
|
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
90 |
* Goal-directed proof now enforces strict proof irrelevance wrt. sort |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
91 |
hypotheses. Sorts required in the course of reasoning need to be |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
92 |
covered by the constraints in the initial statement, completed by the |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
93 |
type instance information of the background theory. Non-trivial sort |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
94 |
hypotheses, which rarely occur in practice, may be specified via |
28633 | 95 |
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: |
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
96 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
97 |
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
98 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
99 |
The result contains an implicit sort hypotheses as before -- |
28631 | 100 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
101 |
normalization. |
|
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
102 |
|
28178
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
103 |
* Changed defaults for unify configuration options: |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
104 |
|
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
105 |
unify_trace_bound = 50 (formerly 25) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
106 |
unify_search_bound = 60 (formerly 30) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
107 |
|
28143 | 108 |
* Different bookkeeping for code equations: |
109 |
a) On theory merge, the last set of code equations for a particular constant |
|
110 |
is taken (in accordance with the policy applied by other parts of the |
|
111 |
code generator framework). |
|
112 |
b) Code equations stemming from explicit declarations (e.g. code attribute) |
|
113 |
gain priority over default code equations stemming from definition, primrec, |
|
114 |
fun etc. |
|
115 |
INCOMPATIBILITY. |
|
116 |
||
28058 | 117 |
* Global versions of theorems stemming from classes do not carry |
118 |
a parameter prefix any longer. INCOMPATIBILITY. |
|
119 |
||
28710 | 120 |
* Dropped locale element "includes". This is a major INCOMPATIBILITY. |
121 |
In existing theorem specifications replace the includes element by the |
|
122 |
respective context elements of the included locale, omitting those that |
|
123 |
are already present in the theorem specification. Multiple assume |
|
124 |
elements of a locale should be replaced by a single one involving the |
|
125 |
locale predicate. In the proof body, declarations (most notably |
|
126 |
theorems) may be regained by interpreting the respective locales in the |
|
127 |
proof context as required (command "interpret"). |
|
128 |
If using "includes" in replacement of a target solely because the |
|
129 |
parameter types in the theorem are not as general as in the target, |
|
130 |
consider declaring a new locale with additional type constraints on the |
|
131 |
parameters (context element "constrains"). |
|
132 |
||
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
133 |
* Dropped "locale (open)". INCOMPATBILITY. |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
134 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
135 |
* Interpretation commands no longer attempt to simplify goal. |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
136 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
137 |
methods intro_locales and unfold_locales to clarify. |
27681 | 138 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
139 |
* Interpretation commands no longer accept interpretation attributes. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
140 |
INCOMPATBILITY. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
141 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
142 |
* Command 'instance': attached definitions no longer accepted. |
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
143 |
INCOMPATIBILITY, use proper 'instantiation' target. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
144 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
145 |
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
146 |
|
28114 | 147 |
* The 'axiomatization' command now only works within a global theory |
148 |
context. INCOMPATIBILITY. |
|
149 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
150 |
|
27381 | 151 |
*** Document preparation *** |
152 |
||
153 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 154 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
155 |
syntax just like the Isar command 'by'. |
27381 | 156 |
|
157 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
158 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
159 |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
160 |
* Made repository layout more coherent with logical |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
161 |
distribution structure: |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
162 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
163 |
src/HOL/Library/RType.thy ~> src/HOL/Typerep.thy |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
164 |
src/HOL/Library/Code_Message.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
165 |
src/HOL/Library/GCD.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
166 |
src/HOL/Library/Order_Relation.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
167 |
src/HOL/Library/Parity.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
168 |
src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
169 |
src/HOL/Real/ContNotDenum.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
170 |
src/HOL/Real/Lubs.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
171 |
src/HOL/Real/PReal.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
172 |
src/HOL/Real/Rational.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
173 |
src/HOL/Real/RComplete.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
174 |
src/HOL/Real/RealDef.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
175 |
src/HOL/Real/RealPow.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
176 |
src/HOL/Real/Real.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
177 |
src/HOL/Complex/Complex_Main.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
178 |
src/HOL/Complex/Complex.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
179 |
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
180 |
src/HOL/Hyperreal/Deriv.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
181 |
src/HOL/Hyperreal/Fact.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
182 |
src/HOL/Hyperreal/Integration.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
183 |
src/HOL/Hyperreal/Lim.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
184 |
src/HOL/Hyperreal/Ln.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
185 |
src/HOL/Hyperreal/Log.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
186 |
src/HOL/Hyperreal/MacLaurin.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
187 |
src/HOL/Hyperreal/NthRoot.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
188 |
src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
189 |
src/HOL/Hyperreal/Taylor.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
190 |
src/HOL/Hyperreal/Transcendental.thy ~> src/HOL/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
191 |
src/HOL/Real/Float ~> src/HOL/Library/ |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
192 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
193 |
src/HOL/arith_data.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
194 |
src/HOL/hologic.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
195 |
src/HOL/simpdata.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
196 |
src/HOL/int_arith1.ML ~> src/HOL/Tools/int_arith.ML |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
197 |
src/HOL/int_factor_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
198 |
src/HOL/nat_simprocs.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
199 |
src/HOL/Real/float_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
200 |
src/HOL/Real/float_syntax.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
201 |
src/HOL/Real/rat_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
202 |
src/HOL/Real/real_arith.ML ~> src/HOL/Tools |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
203 |
|
28741 | 204 |
* If methods "eval" and "evaluation" encounter a structured proof state |
205 |
with !!/==>, only the conclusion is evaluated to True (if possible), |
|
206 |
avoiding strange error messages. |
|
207 |
||
208 |
* Simplifier: simproc for let expressions now unfolds if bound variable |
|
209 |
occurs at most one time in let expression body. INCOMPATIBILITY. |
|
210 |
||
28685 | 211 |
* New classes "top" and "bot" with corresponding operations "top" and "bot" |
212 |
in theory Orderings; instantiation of class "complete_lattice" requires |
|
213 |
instantiation of classes "top" and "bot". INCOMPATIBILITY. |
|
214 |
||
215 |
* Changed definition lemma "less_fun_def" in order to provide an instance |
|
216 |
for preorders on functions; use lemma "less_le" instead. INCOMPATIBILITY. |
|
217 |
||
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
218 |
* Unified theorem tables for both code code generators. Thus |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
219 |
[code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
220 |
|
28685 | 221 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
222 |
"undefined" is the right choice to replace "arbitrary", though logically |
|
223 |
there is no difference. INCOMPATIBILITY. |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
224 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
225 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
28605 | 226 |
Posix processes. Avoids potentially expensive forking of the ML |
227 |
process. New thread-based implementation also works on non-Unix |
|
228 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
|
28606 | 229 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
230 |
commands are covered in the isar-ref manual |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
231 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
232 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
28475 | 233 |
sledgehammer without local ATP installation (Vampire etc.). See also |
234 |
ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
235 |
variable. Other provers may be included via suitable ML wrappers, see |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
236 |
also src/HOL/ATP_Linkup.thy. |
28474
d0b8b0a1fca5
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
28350
diff
changeset
|
237 |
|
28350 | 238 |
* Normalization by evaluation now allows non-leftlinear equations. |
239 |
Declare with attribute [code nbe]. |
|
240 |
||
241 |
* Command "value" now integrates different evaluation |
|
28248 | 242 |
mechanisms. The result of the first successful evaluation mechanism |
243 |
is printed. In square brackets a particular named evaluation |
|
244 |
mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
|
245 |
further src/HOL/ex/Eval_Examples.thy. |
|
28227 | 246 |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28966
diff
changeset
|
247 |
* New method "sizechange" to automate termination proofs using (a |
29182 | 248 |
modification of) the size-change principle. Requires SAT solver. See |
249 |
src/HOL/ex/Termination.thy for examples. |
|
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
28966
diff
changeset
|
250 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
251 |
* HOL/Orderings: class "wellorder" moved here, with explicit induction |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
252 |
rule "less_induct" as assumption. For instantiation of "wellorder" by |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
253 |
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
27823 | 254 |
|
27793 | 255 |
* HOL/Orderings: added class "preorder" as superclass of "order". |
256 |
INCOMPATIBILITY: Instantiation proofs for order, linorder |
|
257 |
etc. slightly changed. Some theorems named order_class.* now named |
|
258 |
preorder_class.*. |
|
259 |
||
28855 | 260 |
* HOL/Finite_Set: added a new fold combinator of type |
261 |
('a => 'b => 'b) => 'b => 'a set => 'b |
|
262 |
Occasionally this is more convenient than the old fold combinator which is |
|
263 |
now defined in terms of the new one and renamed to fold_image. |
|
264 |
||
27793 | 265 |
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been |
266 |
moved to separate class dvd in Ring_and_Field; a couple of lemmas on |
|
267 |
dvd has been generalized to class comm_semiring_1. Likewise a bunch |
|
268 |
of lemmas from Divides has been generalized from nat to class |
|
269 |
semiring_div. INCOMPATIBILITY. This involves the following theorem |
|
270 |
renames resulting from duplicate elimination: |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
271 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
272 |
dvd_def_mod ~> dvd_eq_mod_eq_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
273 |
zero_dvd_iff ~> dvd_0_left_iff |
28559 | 274 |
dvd_0 ~> dvd_0_right |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
275 |
DIVISION_BY_ZERO_DIV ~> div_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
276 |
DIVISION_BY_ZERO_MOD ~> mod_by_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
277 |
mult_div ~> div_mult_self2_is_id |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
278 |
mult_mod ~> mod_mult_self2_is_0 |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
279 |
|
27599 | 280 |
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
281 |
zlcm (for int); carried together from various gcd/lcm developements in |
|
282 |
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
283 |
corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
284 |
recover tupled syntax, use syntax declarations like: |
|
27556 | 285 |
|
286 |
hide (open) const gcd |
|
287 |
abbreviation gcd where |
|
288 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
289 |
notation (output) |
|
290 |
GCD.gcd ("gcd '(_, _')") |
|
291 |
||
292 |
(analogously for lcm, zgcd, zlcm). |
|
293 |
||
294 |
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
|
27551 | 295 |
|
28964 | 296 |
* The real numbers offer decimal input syntax: 12.34 is translated into |
297 |
1234/10^4. This translation is not reversed upon output. |
|
298 |
||
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
299 |
* New ML antiquotation @{code}: takes constant as argument, generates |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
300 |
corresponding code in background and inserts name of the corresponding |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
301 |
resulting ML value/function/datatype constructor binding in place. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
302 |
All occurrences of @{code} with a single ML block are generated |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
303 |
simultaneously. Provides a generic and safe interface for |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
304 |
instrumentalizing code generation. See HOL/ex/Code_Antiq for a toy |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
305 |
example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
306 |
application. In future you ought refrain from ad-hoc compiling |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
307 |
generated SML code on the ML toplevel. Note that (for technical |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
308 |
reasons) @{code} cannot refer to constants for which user-defined |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
309 |
serializations are set. Refer to the corresponding ML counterpart |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
310 |
directly in that cases. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
311 |
|
27424 | 312 |
* Integrated image HOL-Complex with HOL. Entry points Main.thy and |
313 |
Complex_Main.thy remain as they are. |
|
314 |
||
27599 | 315 |
* New image HOL-Plain provides a minimal HOL with the most important |
316 |
tools available (inductive, datatype, primrec, ...). By convention |
|
317 |
the corresponding theory Plain should be ancestor of every further |
|
318 |
(library) theory. Some library theories now have ancestor Plain |
|
319 |
(instead of Main), thus theory Main occasionally has to be imported |
|
320 |
explicitly. |
|
27421 | 321 |
|
28248 | 322 |
* The metis method now fails in the usual manner, rather than raising |
323 |
an exception, if it determines that it cannot prove the theorem. |
|
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28227
diff
changeset
|
324 |
|
28700
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
325 |
* The metis method no longer fails because the theorem is too trivial |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
326 |
(contains the empty clause). |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
327 |
|
27324
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
328 |
* Methods "case_tac" and "induct_tac" now refer to the very same rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
329 |
as the structured Isar versions "cases" and "induct", cf. the |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
330 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
331 |
are now presented as a list of individual projections |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
332 |
(e.g. foo_bar.inducts for types foo and bar); the old format with |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
333 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
334 |
rare situations a different rule is selected --- notably nested tuple |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
335 |
elimination instead of former prod.exhaust: use explicit (case_tac t |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
336 |
rule: prod.exhaust) here. |
27122 | 337 |
|
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
338 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
339 |
|
27122 | 340 |
* Removed fact "case_split_thm", which duplicates "case_split". |
341 |
||
342 |
* Command 'rep_datatype': instead of theorem names the command now |
|
343 |
takes a list of terms denoting the constructors of the type to be |
|
344 |
represented as datatype. The characteristic theorems have to be |
|
345 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
346 |
have disappeared in favour of existing ones: |
|
347 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
348 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
349 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
350 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
351 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
352 |
Suc_not_Zero Zero_not_Suc ~> nat.distinct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
353 |
|
27122 | 354 |
* Library/Nat_Infinity: added addition, numeral syntax and more |
355 |
instantiations for algebraic structures. Removed some duplicate |
|
356 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
357 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
358 |
* ATP selection (E/Vampire/Spass) is now via Proof General's settings |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
359 |
menu. |
28067 | 360 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
361 |
|
27696 | 362 |
*** HOL-Algebra *** |
363 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
364 |
* New locales for orders and lattices where the equivalence relation |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
365 |
is not restricted to equality. INCOMPATIBILITY: all order and |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
366 |
lattice locales use a record structure with field eq for the |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
367 |
equivalence. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
368 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
369 |
* New theory of factorial domains. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
370 |
|
27696 | 371 |
* Units_l_inv and Units_r_inv are now simprules by default. |
372 |
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
|
373 |
and/or r_inv will now also require deletion of these lemmas. |
|
374 |
||
375 |
* Renamed the following theorems. INCOMPATIBILITY. |
|
376 |
UpperD ~> Upper_memD |
|
377 |
LowerD ~> Lower_memD |
|
378 |
least_carrier ~> least_closed |
|
379 |
greatest_carrier ~> greatest_closed |
|
380 |
greatest_Lower_above ~> greatest_Lower_below |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
381 |
one_zero ~> carrier_one_zero |
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
382 |
one_not_zero ~> carrier_one_not_zero (collision with assumption) |
27696 | 383 |
|
27793 | 384 |
|
27485 | 385 |
*** HOL-NSA *** |
386 |
||
387 |
* Created new image HOL-NSA, containing theories of nonstandard |
|
388 |
analysis which were previously part of HOL-Complex. Entry point |
|
389 |
Hyperreal.thy remains valid, but theories formerly using |
|
390 |
Complex_Main.thy should now use new entry point Hypercomplex.thy. |
|
391 |
||
392 |
||
27704 | 393 |
*** ZF *** |
394 |
||
395 |
* Proof of Zorn's Lemma for partial orders. |
|
396 |
||
397 |
||
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
398 |
*** ML *** |
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
399 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
400 |
* High-level support for concurrent ML programming, see |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
401 |
src/Pure/Cuncurrent. The data-oriented model of "future values" is |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
402 |
particularly convenient to organize independent functional |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
403 |
computations. The concept of "synchronized variables" provides a |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
404 |
higher-order interface for components with shared state, avoiding the |
29162 | 405 |
delicate details of mutexes and condition variables. [Poly/ML 5.2.1 |
406 |
or later] |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
407 |
|
28294 | 408 |
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
409 |
to 'a -> thm, while results are always tagged with an authentic oracle |
|
410 |
name. The Isar command 'oracle' is now polymorphic, no argument type |
|
411 |
is specified. INCOMPATIBILITY, need to simplify existing oracle code |
|
412 |
accordingly. Note that extra performance may be gained by producing |
|
413 |
the cterm carefully, avoiding slow Thm.cterm_of. |
|
414 |
||
28282
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
415 |
* ML bindings produced via Isar commands are stored within the Isar |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
416 |
context (theory or proof). Consequently, commands like 'use' and 'ML' |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
417 |
become thread-safe and work with undo as expected (concerning |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
418 |
top-level bindings, not side-effects on global references). |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
419 |
INCOMPATIBILITY, need to provide proper Isar context when invoking the |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
420 |
compiler at runtime; really global bindings need to be given outside a |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
421 |
theory. [Poly/ML 5.2 or later] |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
422 |
|
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
423 |
* Command 'ML_prf' is analogous to 'ML' but works within a proof |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
424 |
context. Top-level ML bindings are stored within the proof context in |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
425 |
a purely sequential fashion, disregarding the nested proof structure. |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
426 |
ML bindings introduced by 'ML_prf' are discarded at the end of the |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
427 |
proof. [Poly/ML 5.2 or later] |
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
428 |
|
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
429 |
* Generic Toplevel.add_hook interface allows to analyze the result of |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
430 |
transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
431 |
for theorem dependency output of transactions resulting in a new |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
432 |
theory state. |
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
433 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
434 |
* Name bindings in higher specification mechanisms (notably |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
435 |
LocalTheory.define, LocalTheory.note, and derived packages) are now |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
436 |
formalized as type Name.binding, replacing old bstring. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
437 |
INCOMPATIBILITY, need to wrap strings via Name.binding function, see |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
438 |
also Name.name_of. Packages should pass name bindings given by the |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
439 |
user to underlying specification mechanisms; this enables precise |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
440 |
tracking of source positions, for example. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
441 |
|
28089
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
442 |
* Result facts (from PureThy.note_thms, ProofContext.note_thms, |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
443 |
LocalTheory.note etc.) now refer to the *full* internal name, not the |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
444 |
bstring as before. INCOMPATIBILITY, not detected by ML type-checking! |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
445 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
446 |
* Rules and tactics that read instantiations (read_instantiate, |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
447 |
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
448 |
context, which is required for parsing and type-checking. Moreover, |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
449 |
the variables are specified as plain indexnames, not string encodings |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
450 |
thereof. INCOMPATIBILITY. |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
451 |
|
27287 | 452 |
* Disposed old type and term read functions (Sign.read_def_typ, |
453 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
454 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
455 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 456 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
457 |
resort for legacy applications. |
|
458 |
||
27380 | 459 |
* Antiquotations: block-structured compilation context indicated by |
27391 | 460 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
461 |
||
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
462 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
463 |
@{note name = fact} - fact abbreviation |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
464 |
@{thm fact} - singleton fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
465 |
@{thms fact} - general fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
466 |
@{lemma prop by method} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
467 |
@{lemma prop by meth1 meth2} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
468 |
@{lemma prop1 ... propN by method} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
469 |
@{lemma prop1 ... propN by meth1 meth2} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
470 |
@{lemma (open) ...} - open derivation |
27380 | 471 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
472 |
|
27979 | 473 |
*** System *** |
474 |
||
28676
78688a5fafc2
multithreading support only for polyml-5.2.1 or later;
wenzelm
parents:
28633
diff
changeset
|
475 |
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for |
78688a5fafc2
multithreading support only for polyml-5.2.1 or later;
wenzelm
parents:
28633
diff
changeset
|
476 |
Poly/ML 5.2.1 or later. |
28254
d67ba23e0277
multithreading for Poly/ML 5.1 is no longer supported;
wenzelm
parents:
28252
diff
changeset
|
477 |
|
28248 | 478 |
* The Isabelle "emacs" tool provides a specific interface to invoke |
479 |
Proof General / Emacs, with more explicit failure if that is not |
|
480 |
installed (the old isabelle-interface script silently falls back on |
|
481 |
isabelle-process). The PROOFGENERAL_HOME setting determines the |
|
482 |
installation location of the Proof General distribution. |
|
483 |
||
27979 | 484 |
* Isabelle/lib/classes/Pure.jar provides basic support to integrate |
485 |
the Isabelle process into a JVM/Scala application. See |
|
486 |
Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java |
|
487 |
process wrapper has been discontinued.) |
|
488 |
||
489 |
* Status messages (with exact source position information) are |
|
490 |
emitted, if proper markup print mode is enabled. This allows |
|
491 |
user-interface components to provide detailed feedback on internal |
|
492 |
prover operations. |
|
493 |
||
494 |
* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. |
|
495 |
||
496 |
||
27143 | 497 |
|
27008 | 498 |
New in Isabelle2008 (June 2008) |
499 |
------------------------------- |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
500 |
|
25522 | 501 |
*** General *** |
502 |
||
27061 | 503 |
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized |
504 |
and updated, with formally checked references as hyperlinks. |
|
505 |
||
25994 | 506 |
* Theory loader: use_thy (and similar operations) no longer set the |
507 |
implicit ML context, which was occasionally hard to predict and in |
|
508 |
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
|
509 |
provides a proper context already. |
|
510 |
||
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
511 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
512 |
file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
513 |
'use' within a theory file will do the job. |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
514 |
|
26650 | 515 |
* Name space merge now observes canonical order, i.e. the second space |
516 |
is inserted into the first one, while existing entries in the first |
|
26659 | 517 |
space take precedence. INCOMPATIBILITY in rare situations, may try to |
26650 | 518 |
swap theory imports. |
519 |
||
27067 | 520 |
* Syntax: symbol \<chi> is now considered a letter. Potential |
521 |
INCOMPATIBILITY in identifier syntax etc. |
|
522 |
||
523 |
* Outer syntax: string tokens no longer admit escaped white space, |
|
524 |
which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
525 |
white space without escapes. |
|
526 |
||
527 |
* Outer syntax: string tokens may contain arbitrary character codes |
|
528 |
specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
|
529 |
"foo_bar". |
|
530 |
||
25522 | 531 |
|
25502 | 532 |
*** Pure *** |
533 |
||
26718 | 534 |
* Context-dependent token translations. Default setup reverts locally |
535 |
fixed variables, and adds hilite markup for undeclared frees. |
|
536 |
||
26681 | 537 |
* Unused theorems can be found using the new command 'unused_thms'. |
538 |
There are three ways of invoking it: |
|
539 |
||
540 |
(1) unused_thms |
|
541 |
Only finds unused theorems in the current theory. |
|
542 |
||
543 |
(2) unused_thms thy_1 ... thy_n - |
|
544 |
Finds unused theorems in the current theory and all of its ancestors, |
|
545 |
excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
546 |
||
547 |
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
548 |
Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
549 |
their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
550 |
their ancestors. |
|
551 |
||
26718 | 552 |
In order to increase the readability of the list produced by |
553 |
unused_thms, theorems that have been created by a particular instance |
|
26874 | 554 |
of a theory command such as 'inductive' or 'function' are considered |
555 |
to belong to the same "group", meaning that if at least one theorem in |
|
26718 | 556 |
this group is used, the other theorems in the same group are no longer |
557 |
reported as unused. Moreover, if all theorems in the group are |
|
558 |
unused, only one theorem in the group is displayed. |
|
559 |
||
560 |
Note that proof objects have to be switched on in order for |
|
561 |
unused_thms to work properly (i.e. !proofs must be >= 1, which is |
|
26874 | 562 |
usually the case when using Proof General with the default settings). |
26681 | 563 |
|
26650 | 564 |
* Authentic naming of facts disallows ad-hoc overwriting of previous |
565 |
theorems within the same name space. INCOMPATIBILITY, need to remove |
|
566 |
duplicate fact bindings, or even accidental fact duplications. Note |
|
567 |
that tools may maintain dynamically scoped facts systematically, using |
|
568 |
PureThy.add_thms_dynamic. |
|
569 |
||
26660 | 570 |
* Command 'hide' now allows to hide from "fact" name space as well. |
571 |
||
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
572 |
* Eliminated destructive theorem database, simpset, claset, and |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
573 |
clasimpset. Potential INCOMPATIBILITY, really need to observe linear |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
574 |
update of theories within ML code. |
26479 | 575 |
|
26955
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
576 |
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory. |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
577 |
INCOMPATIBILITY, object-logics depending on former Pure require |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
578 |
additional setup PureThy.old_appl_syntax_setup; object-logics |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
579 |
depending on former CPure need to refer to Pure. |
26650 | 580 |
|
26495 | 581 |
* Commands 'use' and 'ML' are now purely functional, operating on |
26479 | 582 |
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML' |
583 |
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'. |
|
584 |
INCOMPATIBILITY. |
|
585 |
||
26874 | 586 |
* Command 'setup': discontinued implicit version with ML reference. |
26434 | 587 |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
588 |
* Instantiation target allows for simultaneous specification of class |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
589 |
instance operations together with an instantiation proof. |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
590 |
Type-checking phase allows to refer to class operations uniformly. |
27067 | 591 |
See src/HOL/Complex/Complex.thy for an Isar example and |
592 |
src/HOL/Library/Eval.thy for an ML example. |
|
25502 | 593 |
|
26201
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
594 |
* Indexing of literal facts: be more serious about including only |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
595 |
facts from the visible specification/proof context, but not the |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
596 |
background context (locale etc.). Affects `prop` notation and method |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
597 |
"fact". INCOMPATIBILITY: need to name facts explicitly in rare |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
598 |
situations. |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
599 |
|
26925
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
600 |
* Method "cases", "induct", "coinduct": removed obsolete/undocumented |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
601 |
"(open)" option, which used to expose internal bound variables to the |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
602 |
proof text. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
603 |
|
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
604 |
* Isar statements: removed obsolete case "rule_context". |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
605 |
INCOMPATIBILITY, better use explicit fixes/assumes. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
606 |
|
26874 | 607 |
* Locale proofs: default proof step now includes 'unfold_locales'; |
608 |
hence 'proof' without argument may be used to unfold locale |
|
609 |
predicates. |
|
26765 | 610 |
|
611 |
||
26762 | 612 |
*** Document preparation *** |
613 |
||
26914 | 614 |
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for |
615 |
both pdf and dvi (hyperlinks usually work in xdvi as well); removed |
|
616 |
obsolete thumbpdf setup (contemporary PDF viewers do this on the |
|
617 |
spot); renamed link color from "darkblue" to "linkcolor" (default |
|
26920 | 618 |
value unchanged, can be redefined via \definecolor); no longer sets |
619 |
"a4paper" option (unnecessary or even intrusive). |
|
26914 | 620 |
|
27008 | 621 |
* Antiquotation @{lemma A method} proves proposition A by the given |
622 |
method (either a method name or a method name plus (optional) method |
|
623 |
arguments in parentheses) and prints A just like @{prop A}. |
|
26762 | 624 |
|
625 |
||
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
626 |
*** HOL *** |
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
627 |
|
27067 | 628 |
* New primrec package. Specification syntax conforms in style to |
629 |
definition/function/.... No separate induction rule is provided. The |
|
630 |
"primrec" command distinguishes old-style and new-style specifications |
|
631 |
by syntax. The former primrec package is now named OldPrimrecPackage. |
|
632 |
When adjusting theories, beware: constants stemming from new-style |
|
633 |
primrec specifications have authentic syntax. |
|
634 |
||
635 |
* Metis prover is now an order of magnitude faster, and also works |
|
636 |
with multithreading. |
|
637 |
||
638 |
* Metis: the maximum number of clauses that can be produced from a |
|
639 |
theorem is now given by the attribute max_clauses. Theorems that |
|
640 |
exceed this number are ignored, with a warning printed. |
|
641 |
||
642 |
* Sledgehammer no longer produces structured proofs by default. To |
|
643 |
enable, declare [[sledgehammer_full = true]]. Attributes |
|
644 |
reconstruction_modulus, reconstruction_sorts renamed |
|
645 |
sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. |
|
646 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
647 |
* Method "induct_scheme" derives user-specified induction rules |
27067 | 648 |
from well-founded induction and completeness of patterns. This factors |
649 |
out some operations that are done internally by the function package |
|
650 |
and makes them available separately. See |
|
651 |
src/HOL/ex/Induction_Scheme.thy for examples. |
|
652 |
||
653 |
* More flexible generation of measure functions for termination |
|
654 |
proofs: Measure functions can be declared by proving a rule of the |
|
655 |
form "is_measure f" and giving it the [measure_function] attribute. |
|
656 |
The "is_measure" predicate is logically meaningless (always true), and |
|
657 |
just guides the heuristic. To find suitable measure functions, the |
|
658 |
termination prover sets up the goal "is_measure ?f" of the appropriate |
|
659 |
type and generates all solutions by prolog-style backwards proof using |
|
660 |
the declared rules. |
|
661 |
||
662 |
This setup also deals with rules like |
|
663 |
||
664 |
"is_measure f ==> is_measure (list_size f)" |
|
665 |
||
666 |
which accommodates nested datatypes that recurse through lists. |
|
667 |
Similar rules are predeclared for products and option types. |
|
668 |
||
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
669 |
* Turned the type of sets "'a set" into an abbreviation for "'a => bool" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
670 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
671 |
INCOMPATIBILITIES: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
672 |
|
27008 | 673 |
- Definitions of overloaded constants on sets have to be replaced by |
674 |
definitions on => and bool. |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
675 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
676 |
- Some definitions of overloaded operators on sets can now be proved |
27008 | 677 |
using the definitions of the operators on => and bool. Therefore, |
678 |
the following theorems have been renamed: |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
679 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
680 |
subset_def -> subset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
681 |
psubset_def -> psubset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
682 |
set_diff_def -> set_diff_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
683 |
Compl_def -> Compl_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
684 |
Sup_set_def -> Sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
685 |
Inf_set_def -> Inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
686 |
sup_set_def -> sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
687 |
inf_set_def -> inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
688 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
689 |
- Due to the incompleteness of the HO unification algorithm, some |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
690 |
rules such as subst may require manual instantiation, if some of |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
691 |
the unknowns in the rule is a set. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
692 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
693 |
- Higher order unification and forward proofs: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
694 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
695 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
696 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
697 |
then have "EX S. P S" .. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
698 |
|
27008 | 699 |
no longer works (due to the incompleteness of the HO unification |
700 |
algorithm) and must be replaced by the pattern |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
701 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
702 |
have "EX S. P S" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
703 |
proof |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
704 |
show "P S" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
705 |
qed |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
706 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
707 |
- Calculational reasoning with subst (or similar rules): |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
708 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
709 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
710 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
711 |
also have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
712 |
finally have "P T" . |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
713 |
|
27008 | 714 |
no longer works (for similar reasons as the previous example) and |
715 |
must be replaced by something like |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
716 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
717 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
718 |
moreover have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
719 |
ultimately have "P T" by simp |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
720 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
721 |
- Tactics or packages written in ML code: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
722 |
Code performing pattern matching on types via |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
723 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
724 |
Type ("set", [T]) => ... |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
725 |
|
27008 | 726 |
must be rewritten. Moreover, functions like strip_type or |
727 |
binder_types no longer return the right value when applied to a |
|
728 |
type of the form |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
729 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
730 |
T1 => ... => Tn => U => bool |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
731 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
732 |
rather than |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
733 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
734 |
T1 => ... => Tn => U set |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
735 |
|
26874 | 736 |
* Merged theories Wellfounded_Recursion, Accessible_Part and |
27067 | 737 |
Wellfounded_Relations to theory Wellfounded. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26724
diff
changeset
|
738 |
|
26513 | 739 |
* Explicit class "eq" for executable equality. INCOMPATIBILITY. |
740 |
||
26874 | 741 |
* Class finite no longer treats UNIV as class parameter. Use class |
742 |
enum from theory Library/Enum instead to achieve a similar effect. |
|
26445 | 743 |
INCOMPATIBILITY. |
744 |
||
26874 | 745 |
* Theory List: rule list_induct2 now has explicitly named cases "Nil" |
746 |
and "Cons". INCOMPATIBILITY. |
|
747 |
||
26422
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
748 |
* HOL (and FOL): renamed variables in rules imp_elim and swap. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
749 |
Potential INCOMPATIBILITY. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
750 |
|
26874 | 751 |
* Theory Product_Type: duplicated lemmas split_Pair_apply and |
752 |
injective_fst_snd removed, use split_eta and prod_eqI instead. |
|
753 |
Renamed upd_fst to apfst and upd_snd to apsnd. INCOMPATIBILITY. |
|
26355 | 754 |
|
26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
755 |
* Theory Nat: removed redundant lemmas that merely duplicate lemmas of |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
756 |
the same name in theory Orderings: |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
757 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
758 |
less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
759 |
less_linear |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
760 |
le_imp_less_or_eq |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
761 |
le_less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
762 |
less_le_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
763 |
less_not_sym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
764 |
less_asym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
765 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
766 |
Renamed less_imp_le to less_imp_le_nat, and less_irrefl to |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
767 |
less_irrefl_nat. Potential INCOMPATIBILITY due to more general types |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
768 |
and different variable names. |
26315
cb3badaa192e
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26231
diff
changeset
|
769 |
|
26231 | 770 |
* Library/Option_ord.thy: Canonical order on option type. |
771 |
||
27008 | 772 |
* Library/RBT.thy: Red-black trees, an efficient implementation of |
773 |
finite maps. |
|
26197 | 774 |
|
26231 | 775 |
* Library/Countable.thy: Type class for countable types. |
776 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
777 |
* Theory Int: The representation of numerals has changed. The infix |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
778 |
operator BIT and the bit datatype with constructors B0 and B1 have |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
779 |
disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
780 |
place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
781 |
involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1" |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
782 |
accordingly. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
783 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
784 |
* Theory Nat: definition of <= and < on natural numbers no longer |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
785 |
depend on well-founded relations. INCOMPATIBILITY. Definitions |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
786 |
le_def and less_def have disappeared. Consider lemmas not_less |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
787 |
[symmetric, where ?'a = nat] and less_eq [symmetric] instead. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
788 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
789 |
* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
790 |
(whose purpose mainly is for various fold_set functionals) have been |
26874 | 791 |
abandoned in favor of the existing algebraic classes |
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
792 |
ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult, |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
793 |
lower_semilattice (resp. upper_semilattice) and linorder. |
26139 | 794 |
INCOMPATIBILITY. |
26041
c2e15e65165f
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
haftmann
parents:
26013
diff
changeset
|
795 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
796 |
* Theory Transitive_Closure: induct and cases rules now declare proper |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
797 |
case_names ("base" and "step"). INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
798 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
799 |
* Theorem Inductive.lfp_ordinal_induct generalized to complete |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
800 |
lattices. The form set-specific version is available as |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
801 |
Inductive.lfp_ordinal_induct_set. |
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
26006
diff
changeset
|
802 |
|
26874 | 803 |
* Renamed theorems "power.simps" to "power_int.simps". |
27067 | 804 |
INCOMPATIBILITY. |
25961 | 805 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
806 |
* Class semiring_div provides basic abstract properties of semirings |
25942 | 807 |
with division and modulo operations. Subsumes former class dvd_mod. |
808 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
809 |
* Merged theories IntDef, Numeral and IntArith into unified theory |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
810 |
Int. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
811 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
812 |
* Theory Library/Code_Index: type "index" now represents natural |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
813 |
numbers rather than integers. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
814 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
815 |
* New class "uminus" with operation "uminus" (split of from class |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
816 |
"minus" which now only has operation "minus", binary). |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
817 |
INCOMPATIBILITY. |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
818 |
|
25522 | 819 |
* Constants "card", "internal_split", "option_map" now with authentic |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
820 |
syntax. INCOMPATIBILITY. |
25522 | 821 |
|
822 |
* Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
|
823 |
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
|
824 |
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
|
825 |
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
|
826 |
Sup_set_def, le_def, less_def, option_map_def now with object |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
827 |
equality. INCOMPATIBILITY. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
828 |
|
25705 | 829 |
* Records. Removed K_record, and replaced it by pure lambda term |
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
830 |
%x. c. The simplifier setup is now more robust against eta expansion. |
25705 | 831 |
INCOMPATIBILITY: in cases explicitly referring to K_record. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
832 |
|
27067 | 833 |
* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
834 |
||
835 |
* Library/ListVector: new theory of arithmetic vector operations. |
|
836 |
||
837 |
* Library/Order_Relation: new theory of various orderings as sets of |
|
838 |
pairs. Defines preorders, partial orders, linear orders and |
|
839 |
well-orders on sets and on types. |
|
26877 | 840 |
|
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
841 |
|
26197 | 842 |
*** ZF *** |
843 |
||
26874 | 844 |
* Renamed some theories to allow to loading both ZF and HOL in the |
845 |
same session: |
|
846 |
||
847 |
Datatype -> Datatype_ZF |
|
848 |
Inductive -> Inductive_ZF |
|
849 |
Int -> Int_ZF |
|
850 |
IntDiv -> IntDiv_ZF |
|
851 |
Nat -> Nat_ZF |
|
852 |
List -> List_ZF |
|
853 |
Main -> Main_ZF |
|
854 |
||
855 |
INCOMPATIBILITY: ZF theories that import individual theories below |
|
856 |
Main might need to be adapted. Regular theory Main is still |
|
857 |
available, as trivial extension of Main_ZF. |
|
26197 | 858 |
|
859 |
||
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
860 |
*** ML *** |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
861 |
|
27067 | 862 |
* ML within Isar: antiquotation @{const name} or @{const |
863 |
name(typargs)} produces statically-checked Const term. |
|
864 |
||
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
865 |
* Functor NamedThmsFun: data is available to the user as dynamic fact |
26724
ff6ff3a9010e
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
wenzelm
parents:
26718
diff
changeset
|
866 |
(of the same name). Removed obsolete print command. |
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
867 |
|
27067 | 868 |
* Removed obsolete "use_legacy_bindings" function. |
26188 | 869 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
870 |
* The ``print mode'' is now a thread-local value derived from a global |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
871 |
template (the former print_mode reference), thus access becomes |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
872 |
non-critical. The global print_mode reference is for session |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
873 |
management only; user-code should use print_mode_value, |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
874 |
print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
875 |
|
26874 | 876 |
* Functions system/system_out provide a robust way to invoke external |
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
877 |
shell commands, with propagation of interrupts (requires Poly/ML |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
878 |
5.2.1). Do not use OS.Process.system etc. from the basis library! |
26222
edf6473ac9e9
* system/system_out provides a robust way to invoke external shell
wenzelm
parents:
26218
diff
changeset
|
879 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
880 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
881 |
*** System *** |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
882 |
|
25971 | 883 |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- |
884 |
in accordance with Proof General 3.7, which prefers GNU emacs. |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
885 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
886 |
* isatool tty runs Isabelle process with plain tty interaction; |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
887 |
optional line editor may be specified via ISABELLE_LINE_EDITOR |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
888 |
setting, the default settings attempt to locate "ledit" and "rlwrap". |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
889 |
|
25651 | 890 |
* isatool browser now works with Cygwin as well, using general |
891 |
"javapath" function defined in Isabelle process environment. |
|
892 |
||
27067 | 893 |
* YXML notation provides a simple and efficient alternative to |
894 |
standard XML transfer syntax. See src/Pure/General/yxml.ML and |
|
895 |
isatool yxml as described in the Isabelle system manual. |
|
25651 | 896 |
|
25652 | 897 |
* JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes) |
25651 | 898 |
provides general wrapper for managing an Isabelle process in a robust |
899 |
fashion, with ``cooked'' output from stdin/stderr. |
|
900 |
||
25855 | 901 |
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), |
902 |
based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). |
|
903 |
||
27067 | 904 |
* Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented |
905 |
way of changing the user's settings is via |
|
906 |
ISABELLE_HOME_USER/etc/settings, which is a fully featured bash |
|
907 |
script. |
|
908 |
||
909 |
* Multithreading.max_threads := 0 refers to the number of actual CPU |
|
910 |
cores of the underlying machine, which is a good starting point for |
|
911 |
optimal performance tuning. The corresponding usedir option -M allows |
|
912 |
"max" as an alias for "0". WARNING: does not work on certain versions |
|
913 |
of Mac OS (with Poly/ML 5.1). |
|
914 |
||
915 |
* isabelle-process: non-ML sessions are run with "nice", to reduce the |
|
916 |
adverse effect of Isabelle flooding interactive front-ends (notably |
|
917 |
ProofGeneral / XEmacs). |
|
918 |
||
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
919 |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
920 |
|
25429 | 921 |
New in Isabelle2007 (November 2007) |
922 |
----------------------------------- |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
923 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
924 |
*** General *** |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
925 |
|
22826 | 926 |
* More uniform information about legacy features, notably a |
927 |
warning/error of "Legacy feature: ...", depending on the state of the |
|
23367 | 928 |
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: |
929 |
legacy features will disappear eventually. |
|
22826 | 930 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
931 |
* Theory syntax: the header format ``theory A = B + C:'' has been |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
932 |
discontinued in favour of ``theory A imports B C begin''. Use isatool |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
933 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
934 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
935 |
* Theory syntax: the old non-Isar theory file format has been |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
936 |
discontinued altogether. Note that ML proof scripts may still be used |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
937 |
with Isar theories; migration is usually quite simple with the ML |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
938 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
939 |
|
22871 | 940 |
* Theory syntax: some popular names (e.g. 'class', 'declaration', |
941 |
'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
|
942 |
quotes. |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
943 |
|
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
944 |
* Theory loader: be more serious about observing the static theory |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
945 |
header specifications (including optional directories), but not the |
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
946 |
accidental file locations of previously successful loads. The strict |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
947 |
update policy of former update_thy is now already performed by |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
948 |
use_thy, so the former has been removed; use_thys updates several |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
949 |
theories simultaneously, just as 'imports' within a theory header |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
950 |
specification, but without merging the results. Potential |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
951 |
INCOMPATIBILITY: may need to refine theory headers and commands |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
952 |
ROOT.ML which depend on load order. |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
953 |
|
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
954 |
* Theory loader: optional support for content-based file |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
955 |
identification, instead of the traditional scheme of full physical |
23889 | 956 |
path plus date stamp; configured by the ISABELLE_FILE_IDENT setting |
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
957 |
(cf. the system manual). The new scheme allows to work with |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
958 |
non-finished theories in persistent session images, such that source |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
959 |
files may be moved later on without requiring reloads. |
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
960 |
|
24187
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
961 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
962 |
file (with the same base name as the theory) are considered a legacy |
24800 | 963 |
feature, which will disappear eventually. Even now, the theory loader |
964 |
no longer maintains dependencies on such files. |
|
965 |
||
966 |
* Syntax: the scope for resolving ambiguities via type-inference is |
|
967 |
now limited to individual terms, instead of whole simultaneous |
|
24234
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
968 |
specifications as before. This greatly reduces the complexity of the |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
969 |
syntax module and improves flexibility by separating parsing and |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
970 |
type-checking. INCOMPATIBILITY: additional type-constraints (explicit |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
971 |
'fixes' etc.) are required in rare situations. |
4714e04fb8e9
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;
wenzelm
parents:
24213
diff
changeset
|
972 |
|
25034 | 973 |
* Syntax: constants introduced by new-style packages ('definition', |
974 |
'abbreviation' etc.) are passed through the syntax module in |
|
975 |
``authentic mode''. This means that associated mixfix annotations |
|
976 |
really stick to such constants, independently of potential name space |
|
977 |
ambiguities introduced later on. INCOMPATIBILITY: constants in parse |
|
978 |
trees are represented slightly differently, may need to adapt syntax |
|
979 |
translations accordingly. Use CONST marker in 'translations' and |
|
980 |
@{const_syntax} antiquotation in 'parse_translation' etc. |
|
981 |
||
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
982 |
* Legacy goal package: reduced interface to the bare minimum required |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
983 |
to keep existing proof scripts running. Most other user-level |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
984 |
functions are now part of the OldGoals structure, which is *not* open |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
985 |
by default (consider isatool expandshort before open OldGoals). |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
986 |
Removed top_sg, prin, printyp, pprint_term/typ altogether, because |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
987 |
these tend to cause confusion about the actual goal (!) context being |
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
988 |
used here, which is not necessarily the same as the_context(). |
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
989 |
|
23379
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
990 |
* Command 'find_theorems': supports "*" wild-card in "name:" |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
991 |
criterion; "with_dups" option. Certain ProofGeneral versions might |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
992 |
support a specific search form (see ProofGeneral/CHANGES). |
22965 | 993 |
|
20370 | 994 |
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 |
995 |
by default, which means that "prems" (and also "fixed variables") are |
|
996 |
suppressed from proof state output. Note that the ProofGeneral |
|
997 |
settings mechanism allows to change and save options persistently, but |
|
998 |
older versions of Isabelle will fail to start up if a negative prems |
|
999 |
limit is imposed. |
|
1000 |
||
21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1001 |
* Local theory targets may be specified by non-nested blocks of |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1002 |
``context/locale/class ... begin'' followed by ``end''. The body may |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1003 |
contain definitions, theorems etc., including any derived mechanism |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1004 |
that has been implemented on top of these primitives. This concept |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1005 |
generalizes the existing ``theorem (in ...)'' towards more versatility |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1006 |
and scalability. |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1007 |
|
21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
1008 |
* Proof General interface: proper undo of final 'end' command; |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
1009 |
discontinued Isabelle/classic mode (ML proof scripts). |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
1010 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
1011 |
|
17865 | 1012 |
*** Document preparation *** |
1013 |
||
21717 | 1014 |
* Added antiquotation @{theory name} which prints the given name, |
1015 |
after checking that it refers to a valid ancestor theory in the |
|
1016 |
current context. |
|
21339 | 1017 |
|
17869 | 1018 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
1019 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 1020 |
|
21717 | 1021 |
* Added antiquotation @{abbrev "c args"} which prints the abbreviation |
1022 |
"c args == rhs" given in the current context. (Any number of |
|
21735 | 1023 |
arguments may be given on the LHS.) |
21717 | 1024 |
|
1025 |
||
17779 | 1026 |
*** Pure *** |
1027 |
||
24800 | 1028 |
* The 'class' package offers a combination of axclass and locale to |
25129 | 1029 |
achieve Haskell-like type classes in Isabelle. Definitions and |
1030 |
theorems within a class context produce both relative results (with |
|
1031 |
implicit parameters according to the locale context), and polymorphic |
|
1032 |
constants with qualified polymorphism (according to the class |
|
1033 |
context). Within the body context of a 'class' target, a separate |
|
1034 |
syntax layer ("user space type system") takes care of converting |
|
1035 |
between global polymorphic consts and internal locale representation. |
|
25177 | 1036 |
See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). |
25184 | 1037 |
"isatool doc classes" provides a tutorial. |
20807 | 1038 |
|
25199 | 1039 |
* Generic code generator framework allows to generate executable |
24800 | 1040 |
code for ML and Haskell (including Isabelle classes). A short usage |
1041 |
sketch: |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1042 |
|
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1043 |
internal compilation: |
25199 | 1044 |
export_code <list of constants (term syntax)> in SML |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1045 |
writing SML code to a file: |
25199 | 1046 |
export_code <list of constants (term syntax)> in SML <filename> |
22735 | 1047 |
writing OCaml code to a file: |
25199 | 1048 |
export_code <list of constants (term syntax)> in OCaml <filename> |
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1049 |
writing Haskell code to a bunch of files: |
25199 | 1050 |
export_code <list of constants (term syntax)> in Haskell <filename> |
1051 |
||
1052 |
evaluating closed propositions to True/False using code generation: |
|
25184 | 1053 |
method ``eval'' |
1054 |
||
1055 |
Reasonable default setup of framework in HOL. |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1056 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1057 |
Theorem attributs for selecting and transforming function equations theorems: |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1058 |
|
22845 | 1059 |
[code fun]: select a theorem as function equation for a specific constant |
1060 |
[code fun del]: deselect a theorem as function equation for a specific constant |
|
1061 |
[code inline]: select an equation theorem for unfolding (inlining) in place |
|
1062 |
[code inline del]: deselect an equation theorem for unfolding (inlining) in place |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1063 |
|
22735 | 1064 |
User-defined serializations (target in {SML, OCaml, Haskell}): |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1065 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1066 |
code_const <and-list of constants (term syntax)> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1067 |
{(target) <and-list of const target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1068 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1069 |
code_type <and-list of type constructors> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1070 |
{(target) <and-list of type target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1071 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1072 |
code_instance <and-list of instances> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1073 |
{(target)}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1074 |
where instance ::= <type constructor> :: <class> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1075 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1076 |
code_class <and_list of classes> |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1077 |
{(target) <and-list of class target syntax>}+ |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1078 |
where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}? |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1079 |
|
25199 | 1080 |
code_instance and code_class only are effective to target Haskell. |
22735 | 1081 |
|
25177 | 1082 |
For example usage see src/HOL/ex/Codegenerator.thy and |
1083 |
src/HOL/ex/Codegenerator_Pretty.thy. A separate tutorial on code |
|
24800 | 1084 |
generation from Isabelle/HOL theories is available via "isatool doc |
1085 |
codegen". |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1086 |
|
25129 | 1087 |
* Code generator: consts in 'consts_code' Isar commands are now |
1088 |
referred to by usual term syntax (including optional type |
|
1089 |
annotations). |
|
1090 |
||
19254 | 1091 |
* Command 'no_translations' removes translation rules from theory |
1092 |
syntax. |
|
1093 |
||
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
1094 |
* Overloaded definitions are now actually checked for acyclic |
19714 | 1095 |
dependencies. The overloading scheme is slightly more general than |
1096 |
that of Haskell98, although Isabelle does not demand an exact |
|
1097 |
correspondence to type class and instance declarations. |
|
1098 |
INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more |
|
1099 |
exotic versions of overloading -- at the discretion of the user! |
|
19711 | 1100 |
|
1101 |
Polymorphic constants are represented via type arguments, i.e. the |
|
1102 |
instantiation that matches an instance against the most general |
|
1103 |
declaration given in the signature. For example, with the declaration |
|
1104 |
c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented |
|
1105 |
as c(nat). Overloading is essentially simultaneous structural |
|
1106 |
recursion over such type arguments. Incomplete specification patterns |
|
19714 | 1107 |
impose global constraints on all occurrences, e.g. c('a * 'a) on the |
19715 | 1108 |
LHS means that more general c('a * 'b) will be disallowed on any RHS. |
19714 | 1109 |
Command 'print_theory' outputs the normalized system of recursive |
1110 |
equations, see section "definitions". |
|
19625
285771cec083
* Pure: overloaded definitions are now actually checked for acyclic dependencies;
wenzelm
parents:
19587
diff
changeset
|
1111 |
|
24086 | 1112 |
* Configuration options are maintained within the theory or proof |
1113 |
context (with name and type bool/int/string), providing a very simple |
|
1114 |
interface to a poor-man's version of general context data. Tools may |
|
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1115 |
declare options in ML (e.g. using Attrib.config_int) and then refer to |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1116 |
these values using Config.get etc. Users may change options via an |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1117 |
associated attribute of the same name. This form of context |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1118 |
declaration works particularly well with commands 'declare' or |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1119 |
'using', for example ``declare [[foo = 42]]''. Thus it has become |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1120 |
very easy to avoid global references, which would not observe Isar |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1121 |
toplevel undo/redo and fail to work with multithreading. |
24086 | 1122 |
|
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1123 |
Various global ML references of Pure and HOL have been turned into |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1124 |
configuration options: |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1125 |
|
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1126 |
Unify.search_bound unify_search_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1127 |
Unify.trace_bound unify_trace_bound |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1128 |
Unify.trace_simp unify_trace_simp |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1129 |
Unify.trace_types unify_trace_types |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1130 |
Simplifier.simp_depth_limit simp_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1131 |
Blast.depth_limit blast_depth_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1132 |
DatatypeProp.dtK datatype_distinctness_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1133 |
fast_arith_neq_limit fast_arith_neq_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1134 |
fast_arith_split_limit fast_arith_split_limit |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1135 |
|
24086 | 1136 |
* Named collections of theorems may be easily installed as context |
24800 | 1137 |
data using the functor NamedThmsFun (see also |
24086 | 1138 |
src/Pure/Tools/named_thms.ML). The user may add or delete facts via |
24110
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1139 |
attributes; there is also a toplevel print command. This facility is |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1140 |
just a common case of general context data, which is the preferred way |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1141 |
for anything more complex than just a list of facts in canonical |
4ab3084e311c
tuned config options: eliminated separate attribute "option";
wenzelm
parents:
24086
diff
changeset
|
1142 |
order. |
24086 | 1143 |
|
24032 | 1144 |
* Isar: command 'declaration' augments a local theory by generic |
1145 |
declaration functions written in ML. This enables arbitrary content |
|
1146 |
being added to the context, depending on a morphism that tells the |
|
1147 |
difference of the original declaration context wrt. the application |
|
1148 |
context encountered later on. |
|
1149 |
||
1150 |
* Isar: proper interfaces for simplification procedures. Command |
|
1151 |
'simproc_setup' declares named simprocs (with match patterns, and body |
|
1152 |
text in ML). Attribute "simproc" adds/deletes simprocs in the current |
|
1153 |
context. ML antiquotation @{simproc name} retrieves named simprocs. |
|
1154 |
||
1155 |
* Isar: an extra pair of brackets around attribute declarations |
|
1156 |
abbreviates a theorem reference involving an internal dummy fact, |
|
1157 |
which will be ignored later --- only the effect of the attribute on |
|
1158 |
the background context will persist. This form of in-place |
|
1159 |
declarations is particularly useful with commands like 'declare' and |
|
1160 |
'using', for example ``have A using [[simproc a]] by simp''. |
|
1161 |
||
23369
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1162 |
* Isar: method "assumption" (and implicit closing of subproofs) now |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1163 |
takes simple non-atomic goal assumptions into account: after applying |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1164 |
an assumption as a rule the resulting subgoals are solved by atomic |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1165 |
assumption steps. This is particularly useful to finish 'obtain' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1166 |
goals, such as "!!x. (!!x. P x ==> thesis) ==> P x ==> thesis", |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1167 |
without referring to the original premise "!!x. P x ==> thesis" in the |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1168 |
Isar proof context. POTENTIAL INCOMPATIBILITY: method "assumption" is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1169 |
more permissive. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1170 |
|
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1171 |
* Isar: implicit use of prems from the Isar proof context is |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1172 |
considered a legacy feature. Common applications like ``have A .'' |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1173 |
may be replaced by ``have A by fact'' or ``note `A`''. In general, |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1174 |
referencing facts explicitly here improves readability and |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1175 |
maintainability of proof texts. |
227c51012cdb
* Isar: method "assumption" (implicit closing of subproofs) takes non-atomic goal assumptions into account;
wenzelm
parents:
23367
diff
changeset
|
1176 |
|
17865 | 1177 |
* Isar: improper proof element 'guess' is like 'obtain', but derives |
1178 |
the obtained context from the course of reasoning! For example: |
|
1179 |
||
1180 |
assume "EX x y. A x & B y" -- "any previous fact" |
|
1181 |
then guess x and y by clarify |
|
1182 |
||
1183 |
This technique is potentially adventurous, depending on the facts and |
|
1184 |
proof tools being involved here. |
|
1185 |
||
18020 | 1186 |
* Isar: known facts from the proof context may be specified as literal |
1187 |
propositions, using ASCII back-quote syntax. This works wherever |
|
1188 |
named facts used to be allowed so far, in proof commands, proof |
|
1189 |
methods, attributes etc. Literal facts are retrieved from the context |
|
1190 |
according to unification of type and term parameters. For example, |
|
1191 |
provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known |
|
1192 |
theorems in the current context, then these are valid literal facts: |
|
1193 |
`A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc. |
|
1194 |
||
1195 |
There is also a proof method "fact" which does the same composition |
|
18044 | 1196 |
for explicit goal states, e.g. the following proof texts coincide with |
1197 |
certain special cases of literal facts: |
|
18020 | 1198 |
|
1199 |
have "A" by fact == note `A` |
|
1200 |
have "A ==> B" by fact == note `A ==> B` |
|
1201 |
have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` |
|
1202 |
have "P a ==> Q a" by fact == note `P a ==> Q a` |
|
1203 |
||
20118
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1204 |
* Isar: ":" (colon) is no longer a symbolic identifier character in |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1205 |
outer syntax. Thus symbolic identifiers may be used without |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1206 |
additional white space in declarations like this: ``assume *: A''. |
0c1ec587a5a8
* Isar: ":" (colon) is no longer a symbolic identifier character;
wenzelm
parents:
20090
diff
changeset
|
1207 |
|
20013 | 1208 |
* Isar: 'print_facts' prints all local facts of the current context, |
1209 |
both named and unnamed ones. |
|
1210 |
||
18308 | 1211 |
* Isar: 'def' now admits simultaneous definitions, e.g.: |
1212 |
||
1213 |
def x == "t" and y == "u" |
|
1214 |
||
18540 | 1215 |
* Isar: added command 'unfolding', which is structurally similar to |
1216 |
'using', but affects both the goal state and facts by unfolding given |
|
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1217 |
rewrite rules. Thus many occurrences of the 'unfold' method or |
18540 | 1218 |
'unfolded' attribute may be replaced by first-class proof text. |
1219 |
||
18815
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1220 |
* Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1221 |
and command 'unfolding' now all support object-level equalities |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1222 |
(potentially conditional). The underlying notion of rewrite rule is |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1223 |
analogous to the 'rule_format' attribute, but *not* that of the |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1224 |
Simplifier (which is usually more generous). |
cb778c0ce1b5
Pure/Isar: (un)folded, (un)fold, unfolding support
wenzelm
parents:
18738
diff
changeset
|
1225 |
|
24238 | 1226 |
* Isar: the new attribute [rotated n] (default n = 1) rotates the |
1227 |
premises of a theorem by n. Useful in conjunction with drule. |
|
1228 |
||
19220 | 1229 |
* Isar: the goal restriction operator [N] (default N = 1) evaluates a |
1230 |
method expression within a sandbox consisting of the first N |
|
19240 | 1231 |
sub-goals, which need to exist. For example, ``simp_all [3]'' |
1232 |
simplifies the first three sub-goals, while (rule foo, simp_all)[] |
|
1233 |
simplifies all new goals that emerge from applying rule foo to the |
|
1234 |
originally first one. |
|
19220 | 1235 |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1236 |
* Isar: schematic goals are no longer restricted to higher-order |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1237 |
patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1238 |
expected. |
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1239 |
|
18901 | 1240 |
* Isar: the conclusion of a long theorem statement is now either |
1241 |
'shows' (a simultaneous conjunction, as before), or 'obtains' |
|
1242 |
(essentially a disjunction of cases with local parameters and |
|
1243 |
assumptions). The latter allows to express general elimination rules |
|
18910 | 1244 |
adequately; in this notation common elimination rules look like this: |
18901 | 1245 |
|
1246 |
lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
|
1247 |
assumes "EX x. P x" |
|
1248 |
obtains x where "P x" |
|
1249 |
||
1250 |
lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" |
|
1251 |
assumes "A & B" |
|
1252 |
obtains A and B |
|
1253 |
||
1254 |
lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" |
|
1255 |
assumes "A | B" |
|
1256 |
obtains |
|
1257 |
A |
|
1258 |
| B |
|
1259 |
||
18910 | 1260 |
The subsequent classical rules even refer to the formal "thesis" |
18901 | 1261 |
explicitly: |
1262 |
||
1263 |
lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
|
1264 |
obtains "~ thesis" |
|
1265 |
||
18910 | 1266 |
lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" |
1267 |
obtains "thesis ==> something" |
|
18901 | 1268 |
|
1269 |
The actual proof of an 'obtains' statement is analogous to that of the |
|
18910 | 1270 |
Isar proof element 'obtain', only that there may be several cases. |
1271 |
Optional case names may be specified in parentheses; these will be |
|
1272 |
available both in the present proof and as annotations in the |
|
1273 |
resulting rule, for later use with the 'cases' method (cf. attribute |
|
1274 |
case_names). |
|
18901 | 1275 |
|
21447
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1276 |
* Isar: the assumptions of a long theorem statement are available as |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1277 |
"assms" fact in the proof context. This is more appropriate than the |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1278 |
(historical) "prems", which refers to all assumptions of the current |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1279 |
context, including those from the target locale, proof body etc. |
379f130843f7
* Isar: the assumptions of a long theorem statement are available as assms;
wenzelm
parents:
21406
diff
changeset
|
1280 |
|
19263 | 1281 |
* Isar: 'print_statement' prints theorems from the current theory or |
1282 |
proof context in long statement form, according to the syntax of a |
|
1283 |
top-level lemma. |
|
1284 |
||
18901 | 1285 |
* Isar: 'obtain' takes an optional case name for the local context |
1286 |
introduction rule (default "that"). |
|
1287 |
||
19587 | 1288 |
* Isar: removed obsolete 'concl is' patterns. INCOMPATIBILITY, use |
1289 |
explicit (is "_ ==> ?foo") in the rare cases where this still happens |
|
1290 |
to occur. |
|
1291 |
||
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1292 |
* Pure: syntax "CONST name" produces a fully internalized constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1293 |
according to the current context. This is particularly useful for |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1294 |
syntax translations that should refer to internal constant |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1295 |
representations independently of name spaces. |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1296 |
|
21537
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1297 |
* Pure: syntax constant for foo (binder "FOO ") is called "foo_binder" |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1298 |
instead of "FOO ". This allows multiple binder declarations to coexist |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1299 |
in the same context. INCOMPATIBILITY. |
45b3a85ee548
* Pure: syntax constant for foo (binder) is called foo_binder;
wenzelm
parents:
21471
diff
changeset
|
1300 |
|
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1301 |
* Isar/locales: 'notation' provides a robust interface to the 'syntax' |
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1302 |
primitive that also works in a locale context (both for constants and |
24950 | 1303 |
fixed variables). Type declaration and internal syntactic representation |
1304 |
of given constants retrieved from the context. Likewise, the |
|
1305 |
'no_notation' command allows to remove given syntax annotations from the |
|
1306 |
current context. |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1307 |
|
19665 | 1308 |
* Isar/locales: new derived specification elements 'axiomatization', |
1309 |
'definition', 'abbreviation', which support type-inference, admit |
|
19083 | 1310 |
object-level specifications (equality, equivalence). See also the |
1311 |
isar-ref manual. Examples: |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1312 |
|
19665 | 1313 |
axiomatization |
21595 | 1314 |
eq (infix "===" 50) where |
1315 |
eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y" |
|
1316 |
||
1317 |
definition "f x y = x + y + 1" |
|
1318 |
definition g where "g x = f x x" |
|
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1319 |
|
19363 | 1320 |
abbreviation |
21595 | 1321 |
neq (infix "=!=" 50) where |
19363 | 1322 |
"x =!= y == ~ (x === y)" |
19081
085b5badb8de
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
wenzelm
parents:
19034
diff
changeset
|
1323 |
|
19083 | 1324 |
These specifications may be also used in a locale context. Then the |
1325 |
constants being introduced depend on certain fixed parameters, and the |
|
1326 |
constant name is qualified by the locale base name. An internal |
|
1327 |
abbreviation takes care for convenient input and output, making the |
|
19088 | 1328 |
parameters implicit and using the original short name. See also |
25177 | 1329 |
src/HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic |
19083 | 1330 |
entities from a monomorphic theory. |
1331 |
||
1332 |
Presently, abbreviations are only available 'in' a target locale, but |
|
19363 | 1333 |
not inherited by general import expressions. Also note that |
1334 |
'abbreviation' may be used as a type-safe replacement for 'syntax' + |
|
24735
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1335 |
'translations' in common applications. The "no_abbrevs" print mode |
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1336 |
prevents folding of abbreviations in term output. |
19084 | 1337 |
|
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1338 |
Concrete syntax is attached to specified constants in internal form, |
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1339 |
independently of name spaces. The parse tree representation is |
21209
dbb8decc36bc
'const_syntax' command: allow fixed variables, renamed to 'notation';
wenzelm
parents:
21200
diff
changeset
|
1340 |
slightly different -- use 'notation' instead of raw 'syntax', and |
19682
c8c301eb965a
* Pure: syntax 'CONST name' produces a fully internalized constant;
wenzelm
parents:
19665
diff
changeset
|
1341 |
'translations' with explicit "CONST" markup to accommodate this. |
19665 | 1342 |
|
24800 | 1343 |
* Pure/Isar: unified syntax for new-style specification mechanisms |
1344 |
(e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits |
|
1345 |
full type inference and dummy patterns ("_"). For example: |
|
24735
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1346 |
|
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1347 |
definition "K x _ = x" |
3a55ee2cae70
* Pure/Isar: unified specification syntax admits type inference and dummy patterns;
wenzelm
parents:
24706
diff
changeset
|
1348 |
|
24738 | 1349 |
inductive conj for A B |
1350 |
where "A ==> B ==> conj A B" |
|
1351 |
||
21735 | 1352 |
* Pure: command 'print_abbrevs' prints all constant abbreviations of |
1353 |
the current context. Print mode "no_abbrevs" prevents inversion of |
|
1354 |
abbreviations on output. |
|
1355 |
||
24800 | 1356 |
* Isar/locales: improved parameter handling: use of locales "var" and |
1357 |
"struct" no longer necessary; - parameter renamings are no longer |
|
1358 |
required to be injective. For example, this allows to define |
|
1359 |
endomorphisms as locale endom = homom mult mult h. |
|
19783 | 1360 |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1361 |
* Isar/locales: changed the way locales with predicates are defined. |
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1362 |
Instead of accumulating the specification, the imported expression is |
22126 | 1363 |
now an interpretation. INCOMPATIBILITY: different normal form of |
1364 |
locale expressions. In particular, in interpretations of locales with |
|
1365 |
predicates, goals repesenting already interpreted fragments are not |
|
1366 |
removed automatically. Use methods `intro_locales' and |
|
1367 |
`unfold_locales'; see below. |
|
1368 |
||
1369 |
* Isar/locales: new methods `intro_locales' and `unfold_locales' |
|
1370 |
provide backward reasoning on locales predicates. The methods are |
|
1371 |
aware of interpretations and discharge corresponding goals. |
|
1372 |
`intro_locales' is less aggressive then `unfold_locales' and does not |
|
1373 |
unfold predicates to assumptions. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1374 |
|
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1375 |
* Isar/locales: the order in which locale fragments are accumulated |
22126 | 1376 |
has changed. This enables to override declarations from fragments due |
1377 |
to interpretations -- for example, unwanted simp rules. |
|
19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19895
diff
changeset
|
1378 |
|
23920 | 1379 |
* Isar/locales: interpretation in theories and proof contexts has been |
1380 |
extended. One may now specify (and prove) equations, which are |
|
1381 |
unfolded in interpreted theorems. This is useful for replacing |
|
1382 |
defined concepts (constants depending on locale parameters) by |
|
1383 |
concepts already existing in the target context. Example: |
|
1384 |
||
1385 |
interpretation partial_order ["op <= :: [int, int] => bool"] |
|
1386 |
where "partial_order.less (op <=) (x::int) y = (x < y)" |
|
1387 |
||
24800 | 1388 |
Typically, the constant `partial_order.less' is created by a |
1389 |
definition specification element in the context of locale |
|
1390 |
partial_order. |
|