author | haftmann |
Mon, 17 Nov 2008 17:00:21 +0100 | |
changeset 28819 | daca685d7bb7 |
parent 28741 | 1b257449f804 |
child 28855 | 5d21a3e7303c |
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 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
18 |
- The "Isabelle" alias for "isabelle-interface" has been removed. |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
19 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
24 |
Also note that user interfaces are now better wrapped as regular |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
25 |
Isabelle tools instead of using the special isabelle-interface wrapper |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
26 |
(which can be confusing if the interface is uninstalled or changed |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
27 |
otherwise). See "isabelle tty" and "isabelle emacs" for contemporary |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
28 |
examples. |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
29 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
|
28252 | 34 |
* The Isabelle System Manual (system) has been updated, with formally |
35 |
checked references as hyperlinks. |
|
36 |
||
27599 | 37 |
* Generalized Isar history, with support for linear undo, direct state |
38 |
addressing etc. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
39 |
|
27191 | 40 |
* Recovered hiding of consts, which was accidentally broken in |
41 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
|
42 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
|
43 |
||
27599 | 44 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
45 |
interface instead. |
|
46 |
||
47 |
||
48 |
*** Pure *** |
|
49 |
||
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
50 |
* 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
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
hypotheses, which rarely occur in practice, may be specified via |
28633 | 55 |
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
|
56 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
57 |
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
|
58 |
|
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
59 |
The result contains an implicit sort hypotheses as before -- |
28631 | 60 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
61 |
normalization. |
|
28629
c5a915b45390
goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses;
wenzelm
parents:
28606
diff
changeset
|
62 |
|
28178
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
63 |
* Changed defaults for unify configuration options: |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
64 |
|
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
65 |
unify_trace_bound = 50 (formerly 25) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
66 |
unify_search_bound = 60 (formerly 30) |
e56b8b044bef
* Changed defaults for unify configuration options;
wenzelm
parents:
28143
diff
changeset
|
67 |
|
28143 | 68 |
* Different bookkeeping for code equations: |
69 |
a) On theory merge, the last set of code equations for a particular constant |
|
70 |
is taken (in accordance with the policy applied by other parts of the |
|
71 |
code generator framework). |
|
72 |
b) Code equations stemming from explicit declarations (e.g. code attribute) |
|
73 |
gain priority over default code equations stemming from definition, primrec, |
|
74 |
fun etc. |
|
75 |
INCOMPATIBILITY. |
|
76 |
||
28058 | 77 |
* Global versions of theorems stemming from classes do not carry |
78 |
a parameter prefix any longer. INCOMPATIBILITY. |
|
79 |
||
28710 | 80 |
* Dropped locale element "includes". This is a major INCOMPATIBILITY. |
81 |
In existing theorem specifications replace the includes element by the |
|
82 |
respective context elements of the included locale, omitting those that |
|
83 |
are already present in the theorem specification. Multiple assume |
|
84 |
elements of a locale should be replaced by a single one involving the |
|
85 |
locale predicate. In the proof body, declarations (most notably |
|
86 |
theorems) may be regained by interpreting the respective locales in the |
|
87 |
proof context as required (command "interpret"). |
|
88 |
If using "includes" in replacement of a target solely because the |
|
89 |
parameter types in the theorem are not as general as in the target, |
|
90 |
consider declaring a new locale with additional type constraints on the |
|
91 |
parameters (context element "constrains"). |
|
92 |
||
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
93 |
* Dropped "locale (open)". INCOMPATBILITY. |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
94 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
95 |
* Interpretation commands no longer attempt to simplify goal. |
27761
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
96 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
b95e9ba0ca1d
Interpretation command (theory/proof context) no longer simplifies goal.
ballarin
parents:
27717
diff
changeset
|
97 |
methods intro_locales and unfold_locales to clarify. |
27681 | 98 |
|
28085
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
99 |
* Interpretation commands no longer accept interpretation attributes. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
100 |
INCOMPATBILITY. |
914183e229e9
Interpretation commands no longer accept interpretation attributes.
ballarin
parents:
28067
diff
changeset
|
101 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
102 |
* Command 'instance': attached definitions no longer accepted. |
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
103 |
INCOMPATIBILITY, use proper 'instantiation' target. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
104 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
105 |
* 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
|
106 |
|
28114 | 107 |
* The 'axiomatization' command now only works within a global theory |
108 |
context. INCOMPATIBILITY. |
|
109 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
110 |
|
27381 | 111 |
*** Document preparation *** |
112 |
||
113 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 114 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
115 |
syntax just like the Isar command 'by'. |
27381 | 116 |
|
117 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
118 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
119 |
|
28741 | 120 |
* If methods "eval" and "evaluation" encounter a structured proof state |
121 |
with !!/==>, only the conclusion is evaluated to True (if possible), |
|
122 |
avoiding strange error messages. |
|
123 |
||
124 |
* Simplifier: simproc for let expressions now unfolds if bound variable |
|
125 |
occurs at most one time in let expression body. INCOMPATIBILITY. |
|
126 |
||
28685 | 127 |
* New classes "top" and "bot" with corresponding operations "top" and "bot" |
128 |
in theory Orderings; instantiation of class "complete_lattice" requires |
|
129 |
instantiation of classes "top" and "bot". INCOMPATIBILITY. |
|
130 |
||
131 |
* Changed definition lemma "less_fun_def" in order to provide an instance |
|
132 |
for preorders on functions; use lemma "less_le" instead. INCOMPATIBILITY. |
|
133 |
||
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
134 |
* Unified theorem tables for both code code generators. Thus |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
135 |
[code func] has disappeared and only [code] remains. INCOMPATIBILITY. |
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
136 |
|
28685 | 137 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
138 |
"undefined" is the right choice to replace "arbitrary", though logically |
|
139 |
there is no difference. INCOMPATIBILITY. |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
140 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
141 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
28605 | 142 |
Posix processes. Avoids potentially expensive forking of the ML |
143 |
process. New thread-based implementation also works on non-Unix |
|
144 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
|
28606 | 145 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
146 |
commands are covered in the isar-ref manual |
|
28604
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
147 |
|
f36496b73227
generic ATP manager based on threads (by Fabian Immler);
wenzelm
parents:
28563
diff
changeset
|
148 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
28475 | 149 |
sledgehammer without local ATP installation (Vampire etc.). See also |
150 |
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
|
151 |
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
|
152 |
also src/HOL/ATP_Linkup.thy. |
28474
d0b8b0a1fca5
Vampire wrapper script for remote SystemOnTPTP service (by Fabian Immler);
wenzelm
parents:
28350
diff
changeset
|
153 |
|
28350 | 154 |
* Normalization by evaluation now allows non-leftlinear equations. |
155 |
Declare with attribute [code nbe]. |
|
156 |
||
157 |
* Command "value" now integrates different evaluation |
|
28248 | 158 |
mechanisms. The result of the first successful evaluation mechanism |
159 |
is printed. In square brackets a particular named evaluation |
|
160 |
mechanisms may be specified (currently, [SML], [code] or [nbe]). See |
|
161 |
further src/HOL/ex/Eval_Examples.thy. |
|
28227 | 162 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
163 |
* HOL/Orderings: class "wellorder" moved here, with explicit induction |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
164 |
rule "less_induct" as assumption. For instantiation of "wellorder" by |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
165 |
means of predicate "wf", use rule wf_wellorderI. INCOMPATIBILITY. |
27823 | 166 |
|
27793 | 167 |
* HOL/Orderings: added class "preorder" as superclass of "order". |
168 |
INCOMPATIBILITY: Instantiation proofs for order, linorder |
|
169 |
etc. slightly changed. Some theorems named order_class.* now named |
|
170 |
preorder_class.*. |
|
171 |
||
172 |
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been |
|
173 |
moved to separate class dvd in Ring_and_Field; a couple of lemmas on |
|
174 |
dvd has been generalized to class comm_semiring_1. Likewise a bunch |
|
175 |
of lemmas from Divides has been generalized from nat to class |
|
176 |
semiring_div. INCOMPATIBILITY. This involves the following theorem |
|
177 |
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
|
178 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
179 |
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
|
180 |
zero_dvd_iff ~> dvd_0_left_iff |
28559 | 181 |
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
|
182 |
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
|
183 |
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
|
184 |
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
|
185 |
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
|
186 |
|
27599 | 187 |
* HOL/Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
188 |
zlcm (for int); carried together from various gcd/lcm developements in |
|
189 |
the HOL Distribution. zgcd and zlcm replace former igcd and ilcm; |
|
190 |
corresponding theorems renamed accordingly. INCOMPATIBILY. To |
|
191 |
recover tupled syntax, use syntax declarations like: |
|
27556 | 192 |
|
193 |
hide (open) const gcd |
|
194 |
abbreviation gcd where |
|
195 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
196 |
notation (output) |
|
197 |
GCD.gcd ("gcd '(_, _')") |
|
198 |
||
199 |
(analogously for lcm, zgcd, zlcm). |
|
200 |
||
201 |
* HOL/Real/Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
|
27551 | 202 |
|
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
203 |
* 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
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
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
|
213 |
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
|
214 |
directly in that cases. |
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
215 |
|
27424 | 216 |
* Integrated image HOL-Complex with HOL. Entry points Main.thy and |
217 |
Complex_Main.thy remain as they are. |
|
218 |
||
27599 | 219 |
* New image HOL-Plain provides a minimal HOL with the most important |
220 |
tools available (inductive, datatype, primrec, ...). By convention |
|
221 |
the corresponding theory Plain should be ancestor of every further |
|
222 |
(library) theory. Some library theories now have ancestor Plain |
|
223 |
(instead of Main), thus theory Main occasionally has to be imported |
|
224 |
explicitly. |
|
27421 | 225 |
|
28248 | 226 |
* The metis method now fails in the usual manner, rather than raising |
227 |
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
|
228 |
|
28700
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
229 |
* 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
|
230 |
(contains the empty clause). |
fb92b1d1b285
The metis method no longer fails because the theorem is too trivial
paulson
parents:
28685
diff
changeset
|
231 |
|
27324
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
232 |
* 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
|
233 |
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
|
234 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
235 |
are now presented as a list of individual projections |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
236 |
(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
|
237 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
904acdaf4299
induct_tac: mutual rules work as for method "induct";
wenzelm
parents:
27305
diff
changeset
|
238 |
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
|
239 |
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
|
240 |
rule: prod.exhaust) here. |
27122 | 241 |
|
27141
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
242 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9bfcdb1905e1
* Attributes cases, induct, coinduct support del option.
wenzelm
parents:
27122
diff
changeset
|
243 |
|
27122 | 244 |
* Removed fact "case_split_thm", which duplicates "case_split". |
245 |
||
246 |
* Command 'rep_datatype': instead of theorem names the command now |
|
247 |
takes a list of terms denoting the constructors of the type to be |
|
248 |
represented as datatype. The characteristic theorems have to be |
|
249 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
250 |
have disappeared in favour of existing ones: |
|
251 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
252 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
253 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
254 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
255 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
256 |
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
|
257 |
|
27122 | 258 |
* Library/Nat_Infinity: added addition, numeral syntax and more |
259 |
instantiations for algebraic structures. Removed some duplicate |
|
260 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
261 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
262 |
* ATP selection (E/Vampire/Spass) is now via Proof General's settings |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
263 |
menu. |
28067 | 264 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
265 |
|
27696 | 266 |
*** HOL-Algebra *** |
267 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
268 |
* 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
|
269 |
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
|
270 |
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
|
271 |
equivalence. |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
272 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
273 |
* 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
|
274 |
|
27696 | 275 |
* Units_l_inv and Units_r_inv are now simprules by default. |
276 |
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
|
277 |
and/or r_inv will now also require deletion of these lemmas. |
|
278 |
||
279 |
* Renamed the following theorems. INCOMPATIBILITY. |
|
280 |
UpperD ~> Upper_memD |
|
281 |
LowerD ~> Lower_memD |
|
282 |
least_carrier ~> least_closed |
|
283 |
greatest_carrier ~> greatest_closed |
|
284 |
greatest_Lower_above ~> greatest_Lower_below |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
285 |
one_zero ~> carrier_one_zero |
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
286 |
one_not_zero ~> carrier_one_not_zero (collision with assumption) |
27696 | 287 |
|
27793 | 288 |
|
27485 | 289 |
*** HOL-NSA *** |
290 |
||
291 |
* Created new image HOL-NSA, containing theories of nonstandard |
|
292 |
analysis which were previously part of HOL-Complex. Entry point |
|
293 |
Hyperreal.thy remains valid, but theories formerly using |
|
294 |
Complex_Main.thy should now use new entry point Hypercomplex.thy. |
|
295 |
||
296 |
||
27704 | 297 |
*** ZF *** |
298 |
||
299 |
* Proof of Zorn's Lemma for partial orders. |
|
300 |
||
301 |
||
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
302 |
*** ML *** |
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
303 |
|
28294 | 304 |
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
305 |
to 'a -> thm, while results are always tagged with an authentic oracle |
|
306 |
name. The Isar command 'oracle' is now polymorphic, no argument type |
|
307 |
is specified. INCOMPATIBILITY, need to simplify existing oracle code |
|
308 |
accordingly. Note that extra performance may be gained by producing |
|
309 |
the cterm carefully, avoiding slow Thm.cterm_of. |
|
310 |
||
28282
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
311 |
* 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
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
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
|
316 |
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
|
317 |
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
|
318 |
|
44664ffc9725
* ML bindings produced via Isar commands are stored within the Isar context.
wenzelm
parents:
28254
diff
changeset
|
319 |
* 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
|
320 |
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
|
321 |
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
|
322 |
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
|
323 |
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
|
324 |
|
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
325 |
* 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
|
326 |
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
|
327 |
for theorem dependency output of transactions resulting in a new |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28099
diff
changeset
|
328 |
theory state. |
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
329 |
|
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
330 |
* Name bindings in higher specification mechanisms (notably |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
331 |
LocalTheory.define, LocalTheory.note, and derived packages) are now |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
332 |
formalized as type Name.binding, replacing old bstring. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
333 |
INCOMPATIBILITY, need to wrap strings via Name.binding function, see |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
334 |
also Name.name_of. Packages should pass name bindings given by the |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
335 |
user to underlying specification mechanisms; this enables precise |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
336 |
tracking of source positions, for example. |
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
337 |
|
28089
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
338 |
* Result facts (from PureThy.note_thms, ProofContext.note_thms, |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
342 |
* 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
|
343 |
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
|
344 |
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
|
345 |
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
|
346 |
thereof. INCOMPATIBILITY. |
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
347 |
|
27287 | 348 |
* Disposed old type and term read functions (Sign.read_def_typ, |
349 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
350 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
351 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 352 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
353 |
resort for legacy applications. |
|
354 |
||
27380 | 355 |
* Antiquotations: block-structured compilation context indicated by |
27391 | 356 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
357 |
||
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
358 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
359 |
@{note name = fact} - fact abbreviation |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
360 |
@{thm fact} - singleton fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
361 |
@{thms fact} - general fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
362 |
@{lemma prop by method} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
363 |
@{lemma prop by meth1 meth2} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
364 |
@{lemma prop1 ... propN by method} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
365 |
@{lemma prop1 ... propN by meth1 meth2} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
366 |
@{lemma (open) ...} - open derivation |
27380 | 367 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
368 |
|
27979 | 369 |
*** System *** |
370 |
||
28676
78688a5fafc2
multithreading support only for polyml-5.2.1 or later;
wenzelm
parents:
28633
diff
changeset
|
371 |
* 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
|
372 |
Poly/ML 5.2.1 or later. |
28254
d67ba23e0277
multithreading for Poly/ML 5.1 is no longer supported;
wenzelm
parents:
28252
diff
changeset
|
373 |
|
28248 | 374 |
* The Isabelle "emacs" tool provides a specific interface to invoke |
375 |
Proof General / Emacs, with more explicit failure if that is not |
|
376 |
installed (the old isabelle-interface script silently falls back on |
|
377 |
isabelle-process). The PROOFGENERAL_HOME setting determines the |
|
378 |
installation location of the Proof General distribution. |
|
379 |
||
27979 | 380 |
* Isabelle/lib/classes/Pure.jar provides basic support to integrate |
381 |
the Isabelle process into a JVM/Scala application. See |
|
382 |
Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java |
|
383 |
process wrapper has been discontinued.) |
|
384 |
||
385 |
* Status messages (with exact source position information) are |
|
386 |
emitted, if proper markup print mode is enabled. This allows |
|
387 |
user-interface components to provide detailed feedback on internal |
|
388 |
prover operations. |
|
389 |
||
390 |
* Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. |
|
391 |
||
392 |
||
27143 | 393 |
|
27008 | 394 |
New in Isabelle2008 (June 2008) |
395 |
------------------------------- |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
396 |
|
25522 | 397 |
*** General *** |
398 |
||
27061 | 399 |
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized |
400 |
and updated, with formally checked references as hyperlinks. |
|
401 |
||
25994 | 402 |
* Theory loader: use_thy (and similar operations) no longer set the |
403 |
implicit ML context, which was occasionally hard to predict and in |
|
404 |
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
|
405 |
provides a proper context already. |
|
406 |
||
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
407 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
408 |
file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
409 |
'use' within a theory file will do the job. |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
410 |
|
26650 | 411 |
* Name space merge now observes canonical order, i.e. the second space |
412 |
is inserted into the first one, while existing entries in the first |
|
26659 | 413 |
space take precedence. INCOMPATIBILITY in rare situations, may try to |
26650 | 414 |
swap theory imports. |
415 |
||
27067 | 416 |
* Syntax: symbol \<chi> is now considered a letter. Potential |
417 |
INCOMPATIBILITY in identifier syntax etc. |
|
418 |
||
419 |
* Outer syntax: string tokens no longer admit escaped white space, |
|
420 |
which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
421 |
white space without escapes. |
|
422 |
||
423 |
* Outer syntax: string tokens may contain arbitrary character codes |
|
424 |
specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
|
425 |
"foo_bar". |
|
426 |
||
25522 | 427 |
|
25502 | 428 |
*** Pure *** |
429 |
||
26718 | 430 |
* Context-dependent token translations. Default setup reverts locally |
431 |
fixed variables, and adds hilite markup for undeclared frees. |
|
432 |
||
26681 | 433 |
* Unused theorems can be found using the new command 'unused_thms'. |
434 |
There are three ways of invoking it: |
|
435 |
||
436 |
(1) unused_thms |
|
437 |
Only finds unused theorems in the current theory. |
|
438 |
||
439 |
(2) unused_thms thy_1 ... thy_n - |
|
440 |
Finds unused theorems in the current theory and all of its ancestors, |
|
441 |
excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
442 |
||
443 |
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
444 |
Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
445 |
their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
446 |
their ancestors. |
|
447 |
||
26718 | 448 |
In order to increase the readability of the list produced by |
449 |
unused_thms, theorems that have been created by a particular instance |
|
26874 | 450 |
of a theory command such as 'inductive' or 'function' are considered |
451 |
to belong to the same "group", meaning that if at least one theorem in |
|
26718 | 452 |
this group is used, the other theorems in the same group are no longer |
453 |
reported as unused. Moreover, if all theorems in the group are |
|
454 |
unused, only one theorem in the group is displayed. |
|
455 |
||
456 |
Note that proof objects have to be switched on in order for |
|
457 |
unused_thms to work properly (i.e. !proofs must be >= 1, which is |
|
26874 | 458 |
usually the case when using Proof General with the default settings). |
26681 | 459 |
|
26650 | 460 |
* Authentic naming of facts disallows ad-hoc overwriting of previous |
461 |
theorems within the same name space. INCOMPATIBILITY, need to remove |
|
462 |
duplicate fact bindings, or even accidental fact duplications. Note |
|
463 |
that tools may maintain dynamically scoped facts systematically, using |
|
464 |
PureThy.add_thms_dynamic. |
|
465 |
||
26660 | 466 |
* Command 'hide' now allows to hide from "fact" name space as well. |
467 |
||
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
468 |
* Eliminated destructive theorem database, simpset, claset, and |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
469 |
clasimpset. Potential INCOMPATIBILITY, really need to observe linear |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
470 |
update of theories within ML code. |
26479 | 471 |
|
26955
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
472 |
* 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
|
473 |
INCOMPATIBILITY, object-logics depending on former Pure require |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
474 |
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
|
475 |
depending on former CPure need to refer to Pure. |
26650 | 476 |
|
26495 | 477 |
* Commands 'use' and 'ML' are now purely functional, operating on |
26479 | 478 |
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML' |
479 |
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'. |
|
480 |
INCOMPATIBILITY. |
|
481 |
||
26874 | 482 |
* Command 'setup': discontinued implicit version with ML reference. |
26434 | 483 |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
484 |
* Instantiation target allows for simultaneous specification of class |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
485 |
instance operations together with an instantiation proof. |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
486 |
Type-checking phase allows to refer to class operations uniformly. |
27067 | 487 |
See src/HOL/Complex/Complex.thy for an Isar example and |
488 |
src/HOL/Library/Eval.thy for an ML example. |
|
25502 | 489 |
|
26201
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
490 |
* Indexing of literal facts: be more serious about including only |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
491 |
facts from the visible specification/proof context, but not the |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
492 |
background context (locale etc.). Affects `prop` notation and method |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
493 |
"fact". INCOMPATIBILITY: need to name facts explicitly in rare |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
494 |
situations. |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
495 |
|
26925
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
496 |
* Method "cases", "induct", "coinduct": removed obsolete/undocumented |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
497 |
"(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
|
498 |
proof text. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
499 |
|
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
500 |
* Isar statements: removed obsolete case "rule_context". |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
501 |
INCOMPATIBILITY, better use explicit fixes/assumes. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
502 |
|
26874 | 503 |
* Locale proofs: default proof step now includes 'unfold_locales'; |
504 |
hence 'proof' without argument may be used to unfold locale |
|
505 |
predicates. |
|
26765 | 506 |
|
507 |
||
26762 | 508 |
*** Document preparation *** |
509 |
||
26914 | 510 |
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for |
511 |
both pdf and dvi (hyperlinks usually work in xdvi as well); removed |
|
512 |
obsolete thumbpdf setup (contemporary PDF viewers do this on the |
|
513 |
spot); renamed link color from "darkblue" to "linkcolor" (default |
|
26920 | 514 |
value unchanged, can be redefined via \definecolor); no longer sets |
515 |
"a4paper" option (unnecessary or even intrusive). |
|
26914 | 516 |
|
27008 | 517 |
* Antiquotation @{lemma A method} proves proposition A by the given |
518 |
method (either a method name or a method name plus (optional) method |
|