author | wenzelm |
Sat, 30 May 2009 15:53:19 +0200 | |
changeset 31306 | a74ee84288a0 |
parent 31304 | 00a9c674cf40 |
child 31308 | 3fd52453ae81 |
permissions | -rw-r--r-- |
5363 | 1 |
Isabelle NEWS -- history user-relevant changes |
2 |
============================================== |
|
2553 | 3 |
|
30904 | 4 |
New in this Isabelle version |
5 |
---------------------------- |
|
6 |
||
30951
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
7 |
*** Pure *** |
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
8 |
|
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
9 |
* On instantiation of classes, remaining undefined class parameters are |
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
10 |
formally declared. INCOMPATIBILITY. |
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
11 |
|
a6e26a248f03
formal declaration of undefined parameters after class instantiation
haftmann
parents:
30949
diff
changeset
|
12 |
|
30930 | 13 |
*** HOL *** |
14 |
||
30955 | 15 |
* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1; |
30930 | 16 |
theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and |
17 |
div_mult_mult2 have been generalized to class semiring_div, subsuming former |
|
18 |
theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2. |
|
19 |
div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. |
|
20 |
||
30971 | 21 |
* Power operations on relations and functions are now one dedicate constant compow with |
22 |
infix syntax "^^". Power operations on multiplicative monoids retains syntax "^" |
|
31001 | 23 |
and is now defined generic in class power. INCOMPATIBILITY. |
30964 | 24 |
|
25 |
* ML antiquotation @{code_datatype} inserts definition of a datatype generated |
|
26 |
by the code generator; see Predicate.thy for an example. |
|
30904 | 27 |
|
30949 | 28 |
|
31304 | 29 |
*** ML *** |
30 |
||
31306
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
31 |
* Eliminated old Attrib.add_attributes, Method.add_methods and related |
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
32 |
cominators for "args". INCOMPATIBILITY, need to use simplified |
a74ee84288a0
eliminated old Attrib.add_attributes (and Attrib.syntax);
wenzelm
parents:
31304
diff
changeset
|
33 |
Attrib/Method.setup introduced in Isabelle2009. |
31304 | 34 |
|
35 |
||
36 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
37 |
New in Isabelle2009 (April 2009) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
38 |
-------------------------------- |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
39 |
|
27599 | 40 |
*** General *** |
41 |
||
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
42 |
* 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
|
43 |
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
|
44 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
45 |
- 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
|
46 |
"isatool." |
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
47 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
48 |
- 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
|
49 |
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
|
50 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
51 |
- 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
|
52 |
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
|
53 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
|
28915
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
58 |
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
|
59 |
the interface was uninstalled or changed otherwise. Individual |
0642cbb60c98
removed obsolete isabelle-interface executable and ISABELLE_INTERFACE setting;
wenzelm
parents:
28914
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
|
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
28475
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
|
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
68 |
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
69 |
old ~/isabelle, which was slightly non-standard and apt to cause |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
70 |
surprises on case-insensitive file-systems (such as Mac OS). |
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
71 |
|
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
72 |
INCOMPATIBILITY, need to move existing ~/isabelle/etc, |
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
73 |
~/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
|
74 |
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
|
75 |
ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
76 |
Isabelle distribution, in order to use the new ~/.isabelle uniformly. |
28914
f993cbffc42a
default for ISABELLE_HOME_USER is now ~/.isabelle instead of ~/isabelle;
wenzelm
parents:
28856
diff
changeset
|
77 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
78 |
* Proofs of fully specified statements are run in parallel on |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
79 |
multi-core systems. A speedup factor of 2.5 to 3.2 can be expected on |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
80 |
a regular 4-core machine, if the initial heap space is made reasonably |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
81 |
large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
82 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
83 |
* The main reference manuals ("isar-ref", "implementation", and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
84 |
"system") have been updated and extended. Formally checked references |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
85 |
as hyperlinks are now available uniformly. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
86 |
|
30163
faf95eb3f375
* New prover for coherent logic (see src/Tools/coherent.ML).
wenzelm
parents:
30106
diff
changeset
|
87 |
|
27599 | 88 |
*** Pure *** |
89 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
90 |
* Complete re-implementation of locales. INCOMPATIBILITY in several |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
91 |
respects. The most important changes are listed below. See the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
92 |
Tutorial on Locales ("locales" manual) for details. |
29253 | 93 |
|
94 |
- In locale expressions, instantiation replaces renaming. Parameters |
|
95 |
must be declared in a for clause. To aid compatibility with previous |
|
96 |
parameter inheritance, in locale declarations, parameters that are not |
|
97 |
'touched' (instantiation position "_" or omitted) are implicitly added |
|
98 |
with their syntax at the beginning of the for clause. |
|
99 |
||
100 |
- Syntax from abbreviations and definitions in locales is available in |
|
101 |
locale expressions and context elements. The latter is particularly |
|
102 |
useful in locale declarations. |
|
103 |
||
104 |
- More flexible mechanisms to qualify names generated by locale |
|
105 |
expressions. Qualifiers (prefixes) may be specified in locale |
|
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
106 |
expressions, and can be marked as mandatory (syntax: "name!:") or |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
107 |
optional (syntax "name?:"). The default depends for plain "name:" |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
108 |
depends on the situation where a locale expression is used: in |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
109 |
commands 'locale' and 'sublocale' prefixes are optional, in |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
110 |
'interpretation' and 'interpret' prefixes are mandatory. The old |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
111 |
implicit qualifiers derived from the parameter names of a locale are |
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
112 |
no longer generated. |
30106 | 113 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
114 |
- Command "sublocale l < e" replaces "interpretation l < e". The |
30106 | 115 |
instantiation clause in "interpretation" and "interpret" (square |
116 |
brackets) is no longer available. Use locale expressions. |
|
29253 | 117 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
118 |
- When converting proof scripts, mandatory qualifiers in |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
119 |
'interpretation' and 'interpret' should be retained by default, even |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
120 |
if this is an INCOMPATIBILITY compared to former behavior. In the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
121 |
worst case, use the "name?:" form for non-mandatory ones. Qualifiers |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
122 |
in locale expressions range over a single locale instance only. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
123 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
124 |
- Dropped locale element "includes". This is a major INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
125 |
In existing theorem specifications replace the includes element by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
126 |
respective context elements of the included locale, omitting those |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
127 |
that are already present in the theorem specification. Multiple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
128 |
assume elements of a locale should be replaced by a single one |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
129 |
involving the locale predicate. In the proof body, declarations (most |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
130 |
notably theorems) may be regained by interpreting the respective |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
131 |
locales in the proof context as required (command "interpret"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
132 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
133 |
If using "includes" in replacement of a target solely because the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
134 |
parameter types in the theorem are not as general as in the target, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
135 |
consider declaring a new locale with additional type constraints on |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
136 |
the parameters (context element "constrains"). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
137 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
138 |
- Discontinued "locale (open)". INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
139 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
140 |
- Locale interpretation commands no longer attempt to simplify goal. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
141 |
INCOMPATIBILITY: in rare situations the generated goal differs. Use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
142 |
methods intro_locales and unfold_locales to clarify. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
143 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
144 |
- Locale interpretation commands no longer accept interpretation |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
145 |
attributes. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
146 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
147 |
* Class declaration: so-called "base sort" must not be given in import |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
148 |
list any longer, but is inferred from the specification. Particularly |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
149 |
in HOL, write |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
150 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
151 |
class foo = ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
152 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
153 |
instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
154 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
155 |
class foo = type + ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
156 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
157 |
* Class target: global versions of theorems stemming do not carry a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
158 |
parameter prefix any longer. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
159 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
160 |
* Class 'instance' command no longer accepts attached definitions. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
161 |
INCOMPATIBILITY, use proper 'instantiation' target instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
162 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
163 |
* Recovered hiding of consts, which was accidentally broken in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
164 |
Isabelle2007. Potential INCOMPATIBILITY, ``hide const c'' really |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
165 |
makes c inaccessible; consider using ``hide (open) const c'' instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
166 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
167 |
* Slightly more coherent Pure syntax, with updated documentation in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
168 |
isar-ref manual. Removed locales meta_term_syntax and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
169 |
meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
170 |
INCOMPATIBILITY in rare situations. Note that &&& should not be used |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
171 |
directly in regular applications. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
172 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
173 |
* There is a new syntactic category "float_const" for signed decimal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
174 |
fractions (e.g. 123.45 or -123.45). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
175 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
176 |
* Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
177 |
interface with 'setup' command instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
178 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
179 |
* Command 'local_setup' is similar to 'setup', but operates on a local |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
180 |
theory context. |
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
181 |
|
28114 | 182 |
* The 'axiomatization' command now only works within a global theory |
183 |
context. INCOMPATIBILITY. |
|
184 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
185 |
* Goal-directed proof now enforces strict proof irrelevance wrt. sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
186 |
hypotheses. Sorts required in the course of reasoning need to be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
187 |
covered by the constraints in the initial statement, completed by the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
188 |
type instance information of the background theory. Non-trivial sort |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
189 |
hypotheses, which rarely occur in practice, may be specified via |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
190 |
vacuous propositions of the form SORT_CONSTRAINT('a::c). For example: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
191 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
192 |
lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
193 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
194 |
The result contains an implicit sort hypotheses as before -- |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
195 |
SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
196 |
normalization. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
197 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
198 |
* Generalized Isar history, with support for linear undo, direct state |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
199 |
addressing etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
200 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
201 |
* Changed defaults for unify configuration options: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
202 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
203 |
unify_trace_bound = 50 (formerly 25) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
204 |
unify_search_bound = 60 (formerly 30) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
205 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
206 |
* Different bookkeeping for code equations (INCOMPATIBILITY): |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
207 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
208 |
a) On theory merge, the last set of code equations for a particular |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
209 |
constant is taken (in accordance with the policy applied by other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
210 |
parts of the code generator framework). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
211 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
212 |
b) Code equations stemming from explicit declarations (e.g. code |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
213 |
attribute) gain priority over default code equations stemming |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
214 |
from definition, primrec, fun etc. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
215 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
216 |
* Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
217 |
|
30965 | 218 |
* Unified theorem tables for both code generators. Thus [code |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
219 |
func] has disappeared and only [code] remains. INCOMPATIBILITY. |
30577 | 220 |
|
221 |
* Command 'find_consts' searches for constants based on type and name |
|
222 |
patterns, e.g. |
|
29883 | 223 |
|
224 |
find_consts "_ => bool" |
|
225 |
||
30106 | 226 |
By default, matching is against subtypes, but it may be restricted to |
30728
f0aeca99b5d9
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
30706
diff
changeset
|
227 |
the whole type. Searching by name is possible. Multiple queries are |
30106 | 228 |
conjunctive and queries may be negated by prefixing them with a |
229 |
hyphen: |
|
29883 | 230 |
|
231 |
find_consts strict: "_ => bool" name: "Int" -"int => int" |
|
29861
3c348f5873f3
updated NEWS etc with "solves" criterion and auto_solves
kleing
parents:
29823
diff
changeset
|
232 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
233 |
* New 'find_theorems' criterion "solves" matches theorems that |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
234 |
directly solve the current goal (modulo higher-order unification). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
235 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
236 |
* Auto solve feature for main theorem statements: whenever a new goal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
237 |
is stated, "find_theorems solves" is called; any theorems that could |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
238 |
solve the lemma directly are listed as part of the goal state. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
239 |
Cf. associated options in Proof General Isabelle settings menu, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
240 |
enabled by default, with reasonable timeout for pathological cases of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
241 |
higher-order unification. |
30415
9501af91c4a3
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
webertj
parents:
30399
diff
changeset
|
242 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
243 |
|
27381 | 244 |
*** Document preparation *** |
245 |
||
246 |
* Antiquotation @{lemma} now imitates a regular terminal proof, |
|
27392 | 247 |
demanding keyword 'by' and supporting the full method expression |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
248 |
syntax just like the Isar command 'by'. |
27381 | 249 |
|
250 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
251 |
*** HOL *** |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
252 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
253 |
* Integrated main parts of former image HOL-Complex with HOL. Entry |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
254 |
points Main and Complex_Main remain as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
255 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
256 |
* Logic image HOL-Plain provides a minimal HOL with the most important |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
257 |
tools available (inductive, datatype, primrec, ...). This facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
258 |
experimentation and tool development. Note that user applications |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
259 |
(and library theories) should never refer to anything below theory |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
260 |
Main, as before. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
261 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
262 |
* Logic image HOL-Main stops at theory Main, and thus facilitates |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
263 |
experimentation due to shorter build times. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
264 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
265 |
* Logic image HOL-NSA contains theories of nonstandard analysis which |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
266 |
were previously part of former HOL-Complex. Entry point Hyperreal |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
267 |
remains valid, but theories formerly using Complex_Main should now use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
268 |
new entry point Hypercomplex. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
269 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
270 |
* Generic ATP manager for Sledgehammer, based on ML threads instead of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
271 |
Posix processes. Avoids potentially expensive forking of the ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
272 |
process. New thread-based implementation also works on non-Unix |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
273 |
platforms (Cygwin). Provers are no longer hardwired, but defined |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
274 |
within the theory via plain ML wrapper functions. Basic Sledgehammer |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
275 |
commands are covered in the isar-ref manual. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
276 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
277 |
* Wrapper scripts for remote SystemOnTPTP service allows to use |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
278 |
sledgehammer without local ATP installation (Vampire etc.). Other |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
279 |
provers may be included via suitable ML wrappers, see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
280 |
src/HOL/ATP_Linkup.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
281 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
282 |
* ATP selection (E/Vampire/Spass) is now via Proof General's settings |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
283 |
menu. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
284 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
285 |
* The metis method no longer fails because the theorem is too trivial |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
286 |
(contains the empty clause). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
287 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
288 |
* The metis method now fails in the usual manner, rather than raising |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
289 |
an exception, if it determines that it cannot prove the theorem. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
290 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
291 |
* Method "coherent" implements a prover for coherent logic (see also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
292 |
src/Tools/coherent.ML). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
293 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
294 |
* Constants "undefined" and "default" replace "arbitrary". Usually |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
295 |
"undefined" is the right choice to replace "arbitrary", though |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
296 |
logically there is no difference. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
297 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
298 |
* Command "value" now integrates different evaluation mechanisms. The |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
299 |
result of the first successful evaluation mechanism is printed. In |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
300 |
square brackets a particular named evaluation mechanisms may be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
301 |
specified (currently, [SML], [code] or [nbe]). See further |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
302 |
src/HOL/ex/Eval_Examples.thy. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
303 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
304 |
* Normalization by evaluation now allows non-leftlinear equations. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
305 |
Declare with attribute [code nbe]. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
306 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
307 |
* Methods "case_tac" and "induct_tac" now refer to the very same rules |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
308 |
as the structured Isar versions "cases" and "induct", cf. the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
309 |
corresponding "cases" and "induct" attributes. Mutual induction rules |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
310 |
are now presented as a list of individual projections |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
311 |
(e.g. foo_bar.inducts for types foo and bar); the old format with |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
312 |
explicit HOL conjunction is no longer supported. INCOMPATIBILITY, in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
313 |
rare situations a different rule is selected --- notably nested tuple |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
314 |
elimination instead of former prod.exhaust: use explicit (case_tac t |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
315 |
rule: prod.exhaust) here. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
316 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
317 |
* Attributes "cases", "induct", "coinduct" support "del" option. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
318 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
319 |
* Removed fact "case_split_thm", which duplicates "case_split". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
320 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
321 |
* The option datatype has been moved to a new theory Option. Renamed |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
322 |
option_map to Option.map, and o2s to Option.set, INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
323 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
324 |
* New predicate "strict_mono" classifies strict functions on partial |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
325 |
orders. With strict functions on linear orders, reasoning about |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
326 |
(in)equalities is facilitated by theorems "strict_mono_eq", |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
327 |
"strict_mono_less_eq" and "strict_mono_less". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
328 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
329 |
* Some set operations are now proper qualified constants with |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
330 |
authentic syntax. INCOMPATIBILITY: |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
331 |
|
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
332 |
op Int ~> Set.Int |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
333 |
op Un ~> Set.Un |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
334 |
INTER ~> Set.INTER |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
335 |
UNION ~> Set.UNION |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
336 |
Inter ~> Set.Inter |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
337 |
Union ~> Set.Union |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
338 |
{} ~> Set.empty |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
339 |
UNIV ~> Set.UNIV |
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
30085
diff
changeset
|
340 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
341 |
* Class complete_lattice with operations Inf, Sup, INFI, SUPR now in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
342 |
theory Set. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
343 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
344 |
* Auxiliary class "itself" has disappeared -- classes without any |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
345 |
parameter are treated as expected by the 'class' command. |
29797 | 346 |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
347 |
* Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
348 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
349 |
* Common decision procedures (Cooper, MIR, Ferrack, Approximation, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
350 |
Dense_Linear_Order) are now in directory HOL/Decision_Procs. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
351 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
352 |
* Theory src/HOL/Decision_Procs/Approximation provides the new proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
353 |
method "approximation". It proves formulas on real values by using |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
354 |
interval arithmetic. In the formulas are also the transcendental |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
355 |
functions sin, cos, tan, atan, ln, exp and the constant pi are |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
356 |
allowed. For examples see |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
357 |
src/HOL/Descision_Procs/ex/Approximation_Ex.thy. |
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
358 |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29810
diff
changeset
|
359 |
* Theory "Reflection" now resides in HOL/Library. |
29650 | 360 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
361 |
* Entry point to Word library now simply named "Word". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
362 |
INCOMPATIBILITY. |
29628 | 363 |
|
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
364 |
* Made source layout more coherent with logical distribution |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
365 |
structure: |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
366 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
367 |
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
|
368 |
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
|
369 |
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
|
370 |
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
|
371 |
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
|
372 |
src/HOL/Library/Univ_Poly.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
373 |
src/HOL/Real/ContNotDenum.thy ~> src/HOL/Library/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
374 |
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
|
375 |
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
|
376 |
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
|
377 |
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
|
378 |
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
|
379 |
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
|
380 |
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
|
381 |
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
|
382 |
src/HOL/Complex/Complex.thy ~> src/HOL/ |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
383 |
src/HOL/Complex/FrechetDeriv.thy ~> src/HOL/Library/ |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
384 |
src/HOL/Complex/Fundamental_Theorem_Algebra.thy ~> src/HOL/Library/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
385 |
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
|
386 |
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
|
387 |
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
|
388 |
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
|
389 |
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
|
390 |
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
|
391 |
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
|
392 |
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
|
393 |
src/HOL/Hyperreal/Series.thy ~> src/HOL/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
394 |
src/HOL/Hyperreal/SEQ.thy ~> src/HOL/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
395 |
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
|
396 |
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
|
397 |
src/HOL/Real/Float ~> src/HOL/Library/ |
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
398 |
src/HOL/Real/HahnBanach ~> src/HOL/HahnBanach |
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29182
diff
changeset
|
399 |
src/HOL/Real/RealVector.thy ~> src/HOL/ |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
400 |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28915
diff
changeset
|
401 |
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
|
402 |
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
|
403 |
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
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
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
|
410 |
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
|
411 |
|
29398 | 412 |
src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL |
413 |
src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL |
|
414 |
src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL |
|
415 |
src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL |
|
416 |
src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL |
|
417 |
src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL |
|
418 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
419 |
* If methods "eval" and "evaluation" encounter a structured proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
420 |
state with !!/==>, only the conclusion is evaluated to True (if |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
421 |
possible), avoiding strange error messages. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
422 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
423 |
* Method "sizechange" automates termination proofs using (a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
424 |
modification of) the size-change principle. Requires SAT solver. See |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
425 |
src/HOL/ex/Termination.thy for examples. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
426 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
427 |
* Simplifier: simproc for let expressions now unfolds if bound |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
428 |
variable occurs at most once in let expression body. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
429 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
430 |
* Method "arith": Linear arithmetic now ignores all inequalities when |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
431 |
fast_arith_neq_limit is exceeded, instead of giving up entirely. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
432 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
433 |
* New attribute "arith" for facts that should always be used |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
434 |
automatically by arithmetic. It is intended to be used locally in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
435 |
proofs, e.g. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
436 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
437 |
assumes [arith]: "x > 0" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
438 |
|
30706 | 439 |
Global usage is discouraged because of possible performance impact. |
440 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
441 |
* New classes "top" and "bot" with corresponding operations "top" and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
442 |
"bot" in theory Orderings; instantiation of class "complete_lattice" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
443 |
requires instantiation of classes "top" and "bot". INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
444 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
445 |
* Changed definition lemma "less_fun_def" in order to provide an |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
446 |
instance for preorders on functions; use lemma "less_le" instead. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
447 |
INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
448 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
449 |
* Theory Orderings: class "wellorder" moved here, with explicit |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
450 |
induction rule "less_induct" as assumption. For instantiation of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
451 |
"wellorder" by means of predicate "wf", use rule wf_wellorderI. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
452 |
INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
453 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
454 |
* Theory Orderings: added class "preorder" as superclass of "order". |
27793 | 455 |
INCOMPATIBILITY: Instantiation proofs for order, linorder |
456 |
etc. slightly changed. Some theorems named order_class.* now named |
|
457 |
preorder_class.*. |
|
458 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
459 |
* Theory Relation: renamed "refl" to "refl_on", "reflexive" to "refl, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
460 |
"diag" to "Id_on". |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
461 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
462 |
* Theory Finite_Set: added a new fold combinator of type |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
463 |
|
28855 | 464 |
('a => 'b => 'b) => 'b => 'a set => 'b |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
465 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
466 |
Occasionally this is more convenient than the old fold combinator |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
467 |
which is now defined in terms of the new one and renamed to |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
468 |
fold_image. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
469 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
470 |
* Theories Ring_and_Field and OrderedGroup: The lemmas "group_simps" |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
471 |
and "ring_simps" have been replaced by "algebra_simps" (which can be |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
472 |
extended with further lemmas!). At the moment both still exist but |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
473 |
the former will disappear at some point. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
474 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
475 |
* Theory Power: Lemma power_Suc is now declared as a simp rule in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
476 |
class recpower. Type-specific simp rules for various recpower types |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
477 |
have been removed. INCOMPATIBILITY, rename old lemmas as follows: |
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
478 |
|
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
479 |
rat_power_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
480 |
rat_power_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
481 |
realpow_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
482 |
realpow_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
483 |
complexpow_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
484 |
complexpow_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
485 |
power_poly_0 -> power_0 |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
486 |
power_poly_Suc -> power_Suc |
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30250
diff
changeset
|
487 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
488 |
* Theories Ring_and_Field and Divides: Definition of "op dvd" has been |
27793 | 489 |
moved to separate class dvd in Ring_and_Field; a couple of lemmas on |
490 |
dvd has been generalized to class comm_semiring_1. Likewise a bunch |
|
491 |
of lemmas from Divides has been generalized from nat to class |
|
492 |
semiring_div. INCOMPATIBILITY. This involves the following theorem |
|
493 |
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
|
494 |
|
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
495 |
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
|
496 |
zero_dvd_iff ~> dvd_0_left_iff |
28559 | 497 |
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
|
498 |
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
|
499 |
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
|
500 |
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
|
501 |
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
|
502 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
503 |
* Theory IntDiv: removed many lemmas that are instances of class-based |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
504 |
generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
505 |
rename old lemmas as follows: |
30044 | 506 |
|
507 |
dvd_diff -> nat_dvd_diff |
|
508 |
dvd_zminus_iff -> dvd_minus_iff |
|
30224 | 509 |
mod_add1_eq -> mod_add_eq |
510 |
mod_mult1_eq -> mod_mult_right_eq |
|
511 |
mod_mult1_eq' -> mod_mult_left_eq |
|
512 |
mod_mult_distrib_mod -> mod_mult_eq |
|
30044 | 513 |
nat_mod_add_left_eq -> mod_add_left_eq |
514 |
nat_mod_add_right_eq -> mod_add_right_eq |
|
515 |
nat_mod_div_trivial -> mod_div_trivial |
|
516 |
nat_mod_mod_trivial -> mod_mod_trivial |
|
517 |
zdiv_zadd_self1 -> div_add_self1 |
|
518 |
zdiv_zadd_self2 -> div_add_self2 |
|
30181 | 519 |
zdiv_zmult_self1 -> div_mult_self2_is_id |
30044 | 520 |
zdiv_zmult_self2 -> div_mult_self1_is_id |
521 |
zdvd_triv_left -> dvd_triv_left |
|
522 |
zdvd_triv_right -> dvd_triv_right |
|
523 |
zdvd_zmult_cancel_disj -> dvd_mult_cancel_left |
|
30085 | 524 |
zmod_eq0_zdvd_iff -> dvd_eq_mod_eq_0[symmetric] |
30044 | 525 |
zmod_zadd_left_eq -> mod_add_left_eq |
526 |
zmod_zadd_right_eq -> mod_add_right_eq |
|
527 |
zmod_zadd_self1 -> mod_add_self1 |
|
528 |
zmod_zadd_self2 -> mod_add_self2 |
|
30224 | 529 |
zmod_zadd1_eq -> mod_add_eq |
30044 | 530 |
zmod_zdiff1_eq -> mod_diff_eq |
531 |
zmod_zdvd_zmod -> mod_mod_cancel |
|
532 |
zmod_zmod_cancel -> mod_mod_cancel |
|
533 |
zmod_zmult_self1 -> mod_mult_self2_is_0 |
|
534 |
zmod_zmult_self2 -> mod_mult_self1_is_0 |
|
535 |
zmod_1 -> mod_by_1 |
|
536 |
zdiv_1 -> div_by_1 |
|
537 |
zdvd_abs1 -> abs_dvd_iff |
|
538 |
zdvd_abs2 -> dvd_abs_iff |
|
539 |
zdvd_refl -> dvd_refl |
|
540 |
zdvd_trans -> dvd_trans |
|
541 |
zdvd_zadd -> dvd_add |
|
542 |
zdvd_zdiff -> dvd_diff |
|
543 |
zdvd_zminus_iff -> dvd_minus_iff |
|
544 |
zdvd_zminus2_iff -> minus_dvd_iff |
|
545 |
zdvd_zmultD -> dvd_mult_right |
|
546 |
zdvd_zmultD2 -> dvd_mult_left |
|
547 |
zdvd_zmult_mono -> mult_dvd_mono |
|
548 |
zdvd_0_right -> dvd_0_right |
|
549 |
zdvd_0_left -> dvd_0_left_iff |
|
550 |
zdvd_1_left -> one_dvd |
|
551 |
zminus_dvd_iff -> minus_dvd_iff |
|
552 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
553 |
* Theory Rational: 'Fract k 0' now equals '0'. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
554 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
555 |
* The real numbers offer decimal input syntax: 12.34 is translated |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
556 |
into 1234/10^2. This translation is not reversed upon output. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
557 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
558 |
* Theory Library/Polynomial defines an abstract type 'a poly of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
559 |
univariate polynomials with coefficients of type 'a. In addition to |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
560 |
the standard ring operations, it also supports div and mod. Code |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
561 |
generation is also supported, using list-style constructors. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
562 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
563 |
* Theory Library/Inner_Product defines a class of real_inner for real |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
564 |
inner product spaces, with an overloaded operation inner :: 'a => 'a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
565 |
=> real. Class real_inner is a subclass of real_normed_vector from |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
566 |
theory RealVector. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
567 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
568 |
* Theory Library/Product_Vector provides instances for the product |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
569 |
type 'a * 'b of several classes from RealVector and Inner_Product. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
570 |
Definitions of addition, subtraction, scalar multiplication, norms, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
571 |
and inner products are included. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
572 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
573 |
* Theory Library/Bit defines the field "bit" of integers modulo 2. In |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
574 |
addition to the field operations, numerals and case syntax are also |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
575 |
supported. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
576 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
577 |
* Theory Library/Diagonalize provides constructive version of Cantor's |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
578 |
first diagonalization argument. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
579 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
580 |
* Theory Library/GCD: Curried operations gcd, lcm (for nat) and zgcd, |
27599 | 581 |
zlcm (for int); carried together from various gcd/lcm developements in |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
582 |
the HOL Distribution. Constants zgcd and zlcm replace former igcd and |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
583 |
ilcm; corresponding theorems renamed accordingly. INCOMPATIBILITY, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
584 |
may recover tupled syntax as follows: |
27556 | 585 |
|
586 |
hide (open) const gcd |
|
587 |
abbreviation gcd where |
|
588 |
"gcd == (%(a, b). GCD.gcd a b)" |
|
589 |
notation (output) |
|
590 |
GCD.gcd ("gcd '(_, _')") |
|
591 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
592 |
The same works for lcm, zgcd, zlcm. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
593 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
594 |
* Theory Library/Nat_Infinity: added addition, numeral syntax and more |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
595 |
instantiations for algebraic structures. Removed some duplicate |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
596 |
theorems. Changes in simp rules. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
597 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
598 |
* ML antiquotation @{code} takes a constant as argument and generates |
27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27599
diff
changeset
|
599 |
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
|
600 |
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
|
601 |
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
|
602 |
simultaneously. Provides a generic and safe interface for |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
603 |
instrumentalizing code generation. See |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
604 |
src/HOL/Decision_Procs/Ferrack.thy for a more ambitious application. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
605 |
In future you ought to refrain from ad-hoc compiling generated SML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
606 |
code on the ML toplevel. Note that (for technical reasons) @{code} |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
607 |
cannot refer to constants for which user-defined serializations are |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
608 |
set. Refer to the corresponding ML counterpart directly in that |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
609 |
cases. |
27122 | 610 |
|
611 |
* Command 'rep_datatype': instead of theorem names the command now |
|
612 |
takes a list of terms denoting the constructors of the type to be |
|
613 |
represented as datatype. The characteristic theorems have to be |
|
614 |
proven. INCOMPATIBILITY. Also observe that the following theorems |
|
615 |
have disappeared in favour of existing ones: |
|
616 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
617 |
unit_induct ~> unit.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
618 |
prod_induct ~> prod.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
619 |
sum_induct ~> sum.induct |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
620 |
Suc_Suc_eq ~> nat.inject |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
621 |
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
|
622 |
|
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
623 |
|
27696 | 624 |
*** HOL-Algebra *** |
625 |
||
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
626 |
* New locales for orders and lattices where the equivalence relation |
30106 | 627 |
is not restricted to equality. INCOMPATIBILITY: all order and lattice |
628 |
locales use a record structure with field eq for the equivalence. |
|
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
629 |
|
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
27704
diff
changeset
|
630 |
* 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
|
631 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
632 |
* Units_l_inv and Units_r_inv are now simp rules by default. |
27696 | 633 |
INCOMPATIBILITY. Simplifier proof that require deletion of l_inv |
634 |
and/or r_inv will now also require deletion of these lemmas. |
|
635 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
636 |
* Renamed the following theorems, INCOMPATIBILITY: |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
637 |
|
27696 | 638 |
UpperD ~> Upper_memD |
639 |
LowerD ~> Lower_memD |
|
640 |
least_carrier ~> least_closed |
|
641 |
greatest_carrier ~> greatest_closed |
|
642 |
greatest_Lower_above ~> greatest_Lower_below |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
643 |
one_zero ~> carrier_one_zero |
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
644 |
one_not_zero ~> carrier_one_not_zero (collision with assumption) |
27696 | 645 |
|
27793 | 646 |
|
30849 | 647 |
*** HOL-Nominal *** |
648 |
||
30855 | 649 |
* Nominal datatypes can now contain type-variables. |
650 |
||
651 |
* Commands 'nominal_inductive' and 'equivariance' work with local |
|
652 |
theory targets. |
|
653 |
||
654 |
* Nominal primrec can now works with local theory targets and its |
|
655 |
specification syntax now conforms to the general format as seen in |
|
656 |
'inductive' etc. |
|
657 |
||
658 |
* Method "perm_simp" honours the standard simplifier attributes |
|
659 |
(no_asm), (no_asm_use) etc. |
|
660 |
||
661 |
* The new predicate #* is defined like freshness, except that on the |
|
662 |
left hand side can be a set or list of atoms. |
|
663 |
||
664 |
* Experimental command 'nominal_inductive2' derives strong induction |
|
665 |
principles for inductive definitions. In contrast to |
|
666 |
'nominal_inductive', which can only deal with a fixed number of |
|
667 |
binders, it can deal with arbitrary expressions standing for sets of |
|
668 |
atoms to be avoided. The only inductive definition we have at the |
|
669 |
moment that needs this generalisation is the typing rule for Lets in |
|
670 |
the algorithm W: |
|
671 |
||
672 |
Gamma |- t1 : T1 (x,close Gamma T1)::Gamma |- t2 : T2 x#Gamma |
|
673 |
----------------------------------------------------------------- |
|
674 |
Gamma |- Let x be t1 in t2 : T2 |
|
675 |
||
676 |
In this rule one wants to avoid all the binders that are introduced by |
|
677 |
"close Gamma T1". We are looking for other examples where this |
|
678 |
feature might be useful. Please let us know. |
|
30849 | 679 |
|
680 |
||
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
681 |
*** HOLCF *** |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
682 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
683 |
* Reimplemented the simplification procedure for proving continuity |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
684 |
subgoals. The new simproc is extensible; users can declare additional |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
685 |
continuity introduction rules with the attribute [cont2cont]. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
686 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
687 |
* The continuity simproc now uses a different introduction rule for |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
688 |
solving continuity subgoals on terms with lambda abstractions. In |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
689 |
some rare cases the new simproc may fail to solve subgoals that the |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
690 |
old one could solve, and "simp add: cont2cont_LAM" may be necessary. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
691 |
Potential INCOMPATIBILITY. |
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
692 |
|
30847 | 693 |
* Command 'fixrec': specification syntax now conforms to the general |
30855 | 694 |
format as seen in 'inductive' etc. See src/HOLCF/ex/Fixrec_ex.thy for |
695 |
examples. INCOMPATIBILITY. |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
696 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
697 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
698 |
*** ZF *** |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
699 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
700 |
* Proof of Zorn's Lemma for partial orders. |
30176
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
701 |
|
78610979b3c6
add news for HOLCF; fixed some typos and inaccuracies
huffman
parents:
30163
diff
changeset
|
702 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
703 |
*** ML *** |
28088
723735f2d73a
* Name bindings in higher specification mechanisms;
wenzelm
parents:
28085
diff
changeset
|
704 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
705 |
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
706 |
Poly/ML 5.2.1 or later. Important note: the TimeLimit facility |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
707 |
depends on multithreading, so timouts will not work before Poly/ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
708 |
5.2.1! |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
709 |
|
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
710 |
* High-level support for concurrent ML programming, see |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
711 |
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
|
712 |
particularly convenient to organize independent functional |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
713 |
computations. The concept of "synchronized variables" provides a |
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
714 |
higher-order interface for components with shared state, avoiding the |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
715 |
delicate details of mutexes and condition variables. (Requires |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
716 |
Poly/ML 5.2.1 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
717 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
718 |
* ML bindings produced via Isar commands are stored within the Isar |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
719 |
context (theory or proof). Consequently, commands like 'use' and 'ML' |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
720 |
become thread-safe and work with undo as expected (concerning |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
721 |
top-level bindings, not side-effects on global references). |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
722 |
INCOMPATIBILITY, need to provide proper Isar context when invoking the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
723 |
compiler at runtime; really global bindings need to be given outside a |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
724 |
theory. (Requires Poly/ML 5.2 or later.) |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
725 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
726 |
* Command 'ML_prf' is analogous to 'ML' but works within a proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
727 |
context. Top-level ML bindings are stored within the proof context in |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
728 |
a purely sequential fashion, disregarding the nested proof structure. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
729 |
ML bindings introduced by 'ML_prf' are discarded at the end of the |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
730 |
proof. (Requires Poly/ML 5.2 or later.) |
29161
9903e84a9c9c
* Proofs of are run in parallel on multi-core systems;
wenzelm
parents:
29145
diff
changeset
|
731 |
|
30530 | 732 |
* Simplified ML attribute and method setup, cf. functions Attrib.setup |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
733 |
and Method.setup, as well as Isar commands 'attribute_setup' and |
30547 | 734 |
'method_setup'. INCOMPATIBILITY for 'method_setup', need to simplify |
735 |
existing code accordingly, or use plain 'setup' together with old |
|
736 |
Method.add_method. |
|
30530 | 737 |
|
28294 | 738 |
* Simplified ML oracle interface Thm.add_oracle promotes 'a -> cterm |
739 |
to 'a -> thm, while results are always tagged with an authentic oracle |
|
740 |
name. The Isar command 'oracle' is now polymorphic, no argument type |
|
741 |
is specified. INCOMPATIBILITY, need to simplify existing oracle code |
|
742 |
accordingly. Note that extra performance may be gained by producing |
|
743 |
the cterm carefully, avoiding slow Thm.cterm_of. |
|
744 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
745 |
* Simplified interface for defining document antiquotations via |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
746 |
ThyOutput.antiquotation, ThyOutput.output, and optionally |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
747 |
ThyOutput.maybe_pretty_source. INCOMPATIBILITY, need to simplify user |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
748 |
antiquotations accordingly, see src/Pure/Thy/thy_output.ML for common |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
749 |
examples. |
28099
fb16a07d6580
* Generic Toplevel.add_hook interface allows to analyze the result of
wenzelm
parents:
28089
diff
changeset
|
750 |
|
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
751 |
* More systematic treatment of long names, abstract name bindings, and |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
752 |
name space operations. Basic operations on qualified names have been |
30399 | 753 |
move from structure NameSpace to Long_Name, e.g. Long_Name.base_name, |
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
754 |
Long_Name.append. Old type bstring has been mostly replaced by |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
755 |
abstract type binding (see structure Binding), which supports precise |
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
756 |
qualification by packages and local theory targets, as well as proper |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
757 |
tracking of source positions. INCOMPATIBILITY, need to wrap old |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
758 |
bstring values into Binding.name, or better pass through abstract |
30399 | 759 |
bindings everywhere. See further src/Pure/General/long_name.ML, |
30395
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
760 |
src/Pure/General/binding.ML and src/Pure/General/name_space.ML |
f3103bd2b167
* More systematic treatment of long names, abstract name bindings, and name space operations.
wenzelm
parents:
30326
diff
changeset
|
761 |
|
28089
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
762 |
* Result facts (from PureThy.note_thms, ProofContext.note_thms, |
66ae1926482a
* Result facts now refer to the *full* internal name;
wenzelm
parents:
28088
diff
changeset
|
763 |
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
|
764 |
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
|
765 |
|
27287 | 766 |
* Disposed old type and term read functions (Sign.read_def_typ, |
767 |
Sign.read_typ, Sign.read_def_terms, Sign.read_term, |
|
768 |
Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should |
|
769 |
use regular Syntax.read_typ, Syntax.read_term, Syntax.read_typ_global, |
|
27269 | 770 |
Syntax.read_term_global etc.; see also OldGoals.read_term as last |
771 |
resort for legacy applications. |
|
772 |
||
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
773 |
* Disposed old declarations, tactics, tactic combinators that refer to |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
774 |
the simpset or claset of an implicit theory (such as Addsimps, |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
775 |
Simp_tac, SIMPSET). INCOMPATIBILITY, should use @{simpset} etc. in |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
776 |
embedded ML text, or local_simpset_of with a proper context passed as |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
777 |
explicit runtime argument. |
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
30577
diff
changeset
|
778 |
|
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
779 |
* Rules and tactics that read instantiations (read_instantiate, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
780 |
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
781 |
context, which is required for parsing and type-checking. Moreover, |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
782 |
the variables are specified as plain indexnames, not string encodings |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
783 |
thereof. INCOMPATIBILITY. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
784 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
785 |
* Generic Toplevel.add_hook interface allows to analyze the result of |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
786 |
transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
787 |
for theorem dependency output of transactions resulting in a new |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
788 |
theory state. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
789 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
790 |
* ML antiquotations: block-structured compilation context indicated by |
27391 | 791 |
\<lbrace> ... \<rbrace>; additional antiquotation forms: |
792 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
793 |
@{binding name} - basic name binding |
27519
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
794 |
@{let ?pat = term} - term abbreviation (HO matching) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
795 |
@{note name = fact} - fact abbreviation |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
796 |
@{thm fact} - singleton fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
797 |
@{thms fact} - general fact (with attributes) |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
798 |
@{lemma prop by method} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
799 |
@{lemma prop by meth1 meth2} - singleton goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
800 |
@{lemma prop1 ... propN by method} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
801 |
@{lemma prop1 ... propN by meth1 meth2} - general goal |
59b54d80d2ae
slightly improved @{lemma} (both for latex and ML);
wenzelm
parents:
27485
diff
changeset
|
802 |
@{lemma (open) ...} - open derivation |
27380 | 803 |
|
27246
df85326af57c
* Rules and tactics that read instantiations now demand a proper context;
wenzelm
parents:
27200
diff
changeset
|
804 |
|
27979 | 805 |
*** System *** |
806 |
||
28248 | 807 |
* The Isabelle "emacs" tool provides a specific interface to invoke |
808 |
Proof General / Emacs, with more explicit failure if that is not |
|
809 |
installed (the old isabelle-interface script silently falls back on |
|
810 |
isabelle-process). The PROOFGENERAL_HOME setting determines the |
|
811 |
installation location of the Proof General distribution. |
|
812 |
||
27979 | 813 |
* Isabelle/lib/classes/Pure.jar provides basic support to integrate |
814 |
the Isabelle process into a JVM/Scala application. See |
|
815 |
Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java |
|
816 |
process wrapper has been discontinued.) |
|
817 |
||
30845
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
818 |
* Added homegrown Isabelle font with unicode layout, see lib/fonts. |
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
819 |
|
9a887484de53
misc cleanup and rearrangements for Isabelle2009 release;
wenzelm
parents:
30741
diff
changeset
|
820 |
* Various status messages (with exact source position information) are |
27979 | 821 |
emitted, if proper markup print mode is enabled. This allows |
822 |
user-interface components to provide detailed feedback on internal |
|
823 |
prover operations. |
|
824 |
||
825 |
||
27143 | 826 |
|
27008 | 827 |
New in Isabelle2008 (June 2008) |
828 |
------------------------------- |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
829 |
|
25522 | 830 |
*** General *** |
831 |
||
27061 | 832 |
* The Isabelle/Isar Reference Manual (isar-ref) has been reorganized |
833 |
and updated, with formally checked references as hyperlinks. |
|
834 |
||
25994 | 835 |
* Theory loader: use_thy (and similar operations) no longer set the |
836 |
implicit ML context, which was occasionally hard to predict and in |
|
837 |
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which |
|
838 |
provides a proper context already. |
|
839 |
||
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
840 |
* Theory loader: old-style ML proof scripts being *attached* to a thy |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
841 |
file are no longer supported. INCOMPATIBILITY, regular 'uses' and |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
842 |
'use' within a theory file will do the job. |
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
26315
diff
changeset
|
843 |
|
26650 | 844 |
* Name space merge now observes canonical order, i.e. the second space |
845 |
is inserted into the first one, while existing entries in the first |
|
26659 | 846 |
space take precedence. INCOMPATIBILITY in rare situations, may try to |
26650 | 847 |
swap theory imports. |
848 |
||
27067 | 849 |
* Syntax: symbol \<chi> is now considered a letter. Potential |
850 |
INCOMPATIBILITY in identifier syntax etc. |
|
851 |
||
852 |
* Outer syntax: string tokens no longer admit escaped white space, |
|
853 |
which was an accidental (undocumented) feature. INCOMPATIBILITY, use |
|
854 |
white space without escapes. |
|
855 |
||
856 |
* Outer syntax: string tokens may contain arbitrary character codes |
|
857 |
specified via 3 decimal digits (as in SML). E.g. "foo\095bar" for |
|
858 |
"foo_bar". |
|
859 |
||
25522 | 860 |
|
25502 | 861 |
*** Pure *** |
862 |
||
26718 | 863 |
* Context-dependent token translations. Default setup reverts locally |
864 |
fixed variables, and adds hilite markup for undeclared frees. |
|
865 |
||
26681 | 866 |
* Unused theorems can be found using the new command 'unused_thms'. |
867 |
There are three ways of invoking it: |
|
868 |
||
869 |
(1) unused_thms |
|
870 |
Only finds unused theorems in the current theory. |
|
871 |
||
872 |
(2) unused_thms thy_1 ... thy_n - |
|
873 |
Finds unused theorems in the current theory and all of its ancestors, |
|
874 |
excluding the theories thy_1 ... thy_n and all of their ancestors. |
|
875 |
||
876 |
(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m |
|
877 |
Finds unused theorems in the theories thy'_1 ... thy'_m and all of |
|
878 |
their ancestors, excluding the theories thy_1 ... thy_n and all of |
|
879 |
their ancestors. |
|
880 |
||
26718 | 881 |
In order to increase the readability of the list produced by |
882 |
unused_thms, theorems that have been created by a particular instance |
|
26874 | 883 |
of a theory command such as 'inductive' or 'function' are considered |
884 |
to belong to the same "group", meaning that if at least one theorem in |
|
26718 | 885 |
this group is used, the other theorems in the same group are no longer |
886 |
reported as unused. Moreover, if all theorems in the group are |
|
887 |
unused, only one theorem in the group is displayed. |
|
888 |
||
889 |
Note that proof objects have to be switched on in order for |
|
890 |
unused_thms to work properly (i.e. !proofs must be >= 1, which is |
|
26874 | 891 |
usually the case when using Proof General with the default settings). |
26681 | 892 |
|
26650 | 893 |
* Authentic naming of facts disallows ad-hoc overwriting of previous |
894 |
theorems within the same name space. INCOMPATIBILITY, need to remove |
|
895 |
duplicate fact bindings, or even accidental fact duplications. Note |
|
896 |
that tools may maintain dynamically scoped facts systematically, using |
|
897 |
PureThy.add_thms_dynamic. |
|
898 |
||
26660 | 899 |
* Command 'hide' now allows to hide from "fact" name space as well. |
900 |
||
26496
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
901 |
* Eliminated destructive theorem database, simpset, claset, and |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
902 |
clasimpset. Potential INCOMPATIBILITY, really need to observe linear |
49ae9456eba9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26495
diff
changeset
|
903 |
update of theories within ML code. |
26479 | 904 |
|
26955
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
905 |
* 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
|
906 |
INCOMPATIBILITY, object-logics depending on former Pure require |
ebbaa935eae0
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
wenzelm
parents:
26925
diff
changeset
|
907 |
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
|
908 |
depending on former CPure need to refer to Pure. |
26650 | 909 |
|
26495 | 910 |
* Commands 'use' and 'ML' are now purely functional, operating on |
26479 | 911 |
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML' |
912 |
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'. |
|
913 |
INCOMPATIBILITY. |
|
914 |
||
26874 | 915 |
* Command 'setup': discontinued implicit version with ML reference. |
26434 | 916 |
|
25970
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
917 |
* Instantiation target allows for simultaneous specification of class |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
918 |
instance operations together with an instantiation proof. |
9053fd546501
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;
wenzelm
parents:
25961
diff
changeset
|
919 |
Type-checking phase allows to refer to class operations uniformly. |
27067 | 920 |
See src/HOL/Complex/Complex.thy for an Isar example and |
921 |
src/HOL/Library/Eval.thy for an ML example. |
|
25502 | 922 |
|
26201
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
923 |
* Indexing of literal facts: be more serious about including only |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
924 |
facts from the visible specification/proof context, but not the |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
925 |
background context (locale etc.). Affects `prop` notation and method |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
926 |
"fact". INCOMPATIBILITY: need to name facts explicitly in rare |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
927 |
situations. |
d3363a854708
indexing literal facts: exclude background context;
wenzelm
parents:
26197
diff
changeset
|
928 |
|
26925
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
929 |
* Method "cases", "induct", "coinduct": removed obsolete/undocumented |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
930 |
"(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
|
931 |
proof text. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
932 |
|
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
933 |
* Isar statements: removed obsolete case "rule_context". |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
934 |
INCOMPATIBILITY, better use explicit fixes/assumes. |
ce964f0df281
* Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
wenzelm
parents:
26920
diff
changeset
|
935 |
|
26874 | 936 |
* Locale proofs: default proof step now includes 'unfold_locales'; |
937 |
hence 'proof' without argument may be used to unfold locale |
|
938 |
predicates. |
|
26765 | 939 |
|
940 |
||
26762 | 941 |
*** Document preparation *** |
942 |
||
26914 | 943 |
* Simplified pdfsetup.sty: color/hyperref is used unconditionally for |
944 |
both pdf and dvi (hyperlinks usually work in xdvi as well); removed |
|
945 |
obsolete thumbpdf setup (contemporary PDF viewers do this on the |
|
946 |
spot); renamed link color from "darkblue" to "linkcolor" (default |
|
26920 | 947 |
value unchanged, can be redefined via \definecolor); no longer sets |
948 |
"a4paper" option (unnecessary or even intrusive). |
|
26914 | 949 |
|
27008 | 950 |
* Antiquotation @{lemma A method} proves proposition A by the given |
951 |
method (either a method name or a method name plus (optional) method |
|
952 |
arguments in parentheses) and prints A just like @{prop A}. |
|
26762 | 953 |
|
954 |
||
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
955 |
*** HOL *** |
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
956 |
|
27067 | 957 |
* New primrec package. Specification syntax conforms in style to |
958 |
definition/function/.... No separate induction rule is provided. The |
|
959 |
"primrec" command distinguishes old-style and new-style specifications |
|
960 |
by syntax. The former primrec package is now named OldPrimrecPackage. |
|
961 |
When adjusting theories, beware: constants stemming from new-style |
|
962 |
primrec specifications have authentic syntax. |
|
963 |
||
964 |
* Metis prover is now an order of magnitude faster, and also works |
|
965 |
with multithreading. |
|
966 |
||
967 |
* Metis: the maximum number of clauses that can be produced from a |
|
968 |
theorem is now given by the attribute max_clauses. Theorems that |
|
969 |
exceed this number are ignored, with a warning printed. |
|
970 |
||
971 |
* Sledgehammer no longer produces structured proofs by default. To |
|
972 |
enable, declare [[sledgehammer_full = true]]. Attributes |
|
973 |
reconstruction_modulus, reconstruction_sorts renamed |
|
974 |
sledgehammer_modulus, sledgehammer_sorts. INCOMPATIBILITY. |
|
975 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
27067
diff
changeset
|
976 |
* Method "induct_scheme" derives user-specified induction rules |
27067 | 977 |
from well-founded induction and completeness of patterns. This factors |
978 |
out some operations that are done internally by the function package |
|
979 |
and makes them available separately. See |
|
980 |
src/HOL/ex/Induction_Scheme.thy for examples. |
|
981 |
||
982 |
* More flexible generation of measure functions for termination |
|
983 |
proofs: Measure functions can be declared by proving a rule of the |
|
984 |
form "is_measure f" and giving it the [measure_function] attribute. |
|
985 |
The "is_measure" predicate is logically meaningless (always true), and |
|
986 |
just guides the heuristic. To find suitable measure functions, the |
|
987 |
termination prover sets up the goal "is_measure ?f" of the appropriate |
|
988 |
type and generates all solutions by prolog-style backwards proof using |
|
989 |
the declared rules. |
|
990 |
||
991 |
This setup also deals with rules like |
|
992 |
||
993 |
"is_measure f ==> is_measure (list_size f)" |
|
994 |
||
995 |
which accommodates nested datatypes that recurse through lists. |
|
996 |
Similar rules are predeclared for products and option types. |
|
997 |
||
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
998 |
* 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
|
999 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1000 |
INCOMPATIBILITIES: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1001 |
|
27008 | 1002 |
- Definitions of overloaded constants on sets have to be replaced by |
1003 |
definitions on => and bool. |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1004 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1005 |
- Some definitions of overloaded operators on sets can now be proved |
27008 | 1006 |
using the definitions of the operators on => and bool. Therefore, |
1007 |
the following theorems have been renamed: |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1008 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1009 |
subset_def -> subset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1010 |
psubset_def -> psubset_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1011 |
set_diff_def -> set_diff_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1012 |
Compl_def -> Compl_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1013 |
Sup_set_def -> Sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1014 |
Inf_set_def -> Inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1015 |
sup_set_def -> sup_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1016 |
inf_set_def -> inf_set_eq |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1017 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1018 |
- 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
|
1019 |
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
|
1020 |
the unknowns in the rule is a set. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1021 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1022 |
- Higher order unification and forward proofs: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1023 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1024 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1025 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1026 |
then have "EX S. P S" .. |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1027 |
|
27008 | 1028 |
no longer works (due to the incompleteness of the HO unification |
1029 |
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
|
1030 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1031 |
have "EX S. P S" |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1032 |
proof |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1033 |
show "P S" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1034 |
qed |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1035 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1036 |
- Calculational reasoning with subst (or similar rules): |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1037 |
The proof pattern |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1038 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1039 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1040 |
also have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1041 |
finally have "P T" . |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1042 |
|
27008 | 1043 |
no longer works (for similar reasons as the previous example) and |
1044 |
must be replaced by something like |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1045 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1046 |
have "P (S::'a set)" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1047 |
moreover have "S = T" <...> |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1048 |
ultimately have "P T" by simp |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1049 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1050 |
- Tactics or packages written in ML code: |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1051 |
Code performing pattern matching on types via |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1052 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1053 |
Type ("set", [T]) => ... |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1054 |
|
27008 | 1055 |
must be rewritten. Moreover, functions like strip_type or |
1056 |
binder_types no longer return the right value when applied to a |
|
1057 |
type of the form |
|
26964
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1058 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1059 |
T1 => ... => Tn => U => bool |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1060 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1061 |
rather than |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1062 |
|
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1063 |
T1 => ... => Tn => U set |
df1f238a05f7
Added entry explaining incompatibilities introduced by replacing sets by predicates.
berghofe
parents:
26955
diff
changeset
|
1064 |
|
26874 | 1065 |
* Merged theories Wellfounded_Recursion, Accessible_Part and |
27067 | 1066 |
Wellfounded_Relations to theory Wellfounded. |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26724
diff
changeset
|
1067 |
|
26513 | 1068 |
* Explicit class "eq" for executable equality. INCOMPATIBILITY. |
1069 |
||
26874 | 1070 |
* Class finite no longer treats UNIV as class parameter. Use class |
1071 |
enum from theory Library/Enum instead to achieve a similar effect. |
|
26445 | 1072 |
INCOMPATIBILITY. |
1073 |
||
26874 | 1074 |
* Theory List: rule list_induct2 now has explicitly named cases "Nil" |
1075 |
and "Cons". INCOMPATIBILITY. |
|
1076 |
||
26422
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
1077 |
* 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
|
1078 |
Potential INCOMPATIBILITY. |
d5883907c514
HOL (and FOL): renamed variables in rules imp_elim and swap;
wenzelm
parents:
26401
diff
changeset
|
1079 |
|
26874 | 1080 |
* Theory Product_Type: duplicated lemmas split_Pair_apply and |
1081 |
injective_fst_snd removed, use split_eta and prod_eqI instead. |
|
1082 |
Renamed upd_fst to apfst and upd_snd to apsnd. INCOMPATIBILITY. |
|
26355 | 1083 |
|
26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1084 |
* 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
|
1085 |
the same name in theory Orderings: |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1086 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1087 |
less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1088 |
less_linear |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1089 |
le_imp_less_or_eq |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1090 |
le_less_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1091 |
less_le_trans |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1092 |
less_not_sym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1093 |
less_asym |
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1094 |
|
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26333
diff
changeset
|
1095 |
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
|
1096 |
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
|
1097 |
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
|
1098 |
|
26231 | 1099 |
* Library/Option_ord.thy: Canonical order on option type. |
1100 |
||
27008 | 1101 |
* Library/RBT.thy: Red-black trees, an efficient implementation of |
1102 |
finite maps. |
|
26197 | 1103 |
|
26231 | 1104 |
* Library/Countable.thy: Type class for countable types. |
1105 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1106 |
* 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
|
1107 |
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
|
1108 |
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
|
1109 |
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
|
1110 |
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
|
1111 |
accordingly. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1112 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1113 |
* 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
|
1114 |
depend on well-founded relations. INCOMPATIBILITY. Definitions |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1115 |
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
|
1116 |
[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
|
1117 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1118 |
* 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
|
1119 |
(whose purpose mainly is for various fold_set functionals) have been |
26874 | 1120 |
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
|
1121 |
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
|
1122 |
lower_semilattice (resp. upper_semilattice) and linorder. |
26139 | 1123 |
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
|
1124 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1125 |
* 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
|
1126 |
case_names ("base" and "step"). INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1127 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1128 |
* 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
|
1129 |
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
|
1130 |
Inductive.lfp_ordinal_induct_set. |
26013
8764a1f1253b
Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents:
26006
diff
changeset
|
1131 |
|
26874 | 1132 |
* Renamed theorems "power.simps" to "power_int.simps". |
27067 | 1133 |
INCOMPATIBILITY. |
25961 | 1134 |
|
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1135 |
* Class semiring_div provides basic abstract properties of semirings |
25942 | 1136 |
with division and modulo operations. Subsumes former class dvd_mod. |
1137 |
||
26180
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1138 |
* 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
|
1139 |
Int. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1140 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1141 |
* 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
|
1142 |
numbers rather than integers. INCOMPATIBILITY. |
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1143 |
|
cc85eaab20f6
Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents:
26139
diff
changeset
|
1144 |
* 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
|
1145 |
"minus" which now only has operation "minus", binary). |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
1146 |
INCOMPATIBILITY. |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
1147 |
|
25522 | 1148 |
* Constants "card", "internal_split", "option_map" now with authentic |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25900
diff
changeset
|
1149 |
syntax. INCOMPATIBILITY. |
25522 | 1150 |
|
1151 |
* Definitions subset_def, psubset_def, set_diff_def, Compl_def, |
|
1152 |
le_bool_def, less_bool_def, le_fun_def, less_fun_def, inf_bool_def, |
|
1153 |
sup_bool_def, Inf_bool_def, Sup_bool_def, inf_fun_def, sup_fun_def, |
|
1154 |
Inf_fun_def, Sup_fun_def, inf_set_def, sup_set_def, Inf_set_def, |
|
1155 |
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
|
1156 |
equality. INCOMPATIBILITY. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
1157 |
|
25705 | 1158 |
* 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
|
1159 |
%x. c. The simplifier setup is now more robust against eta expansion. |
25705 | 1160 |
INCOMPATIBILITY: in cases explicitly referring to K_record. |
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
1161 |
|
27067 | 1162 |
* Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}. |
1163 |
||
1164 |
* Library/ListVector: new theory of arithmetic vector operations. |
|
1165 |
||
1166 |
* Library/Order_Relation: new theory of various orderings as sets of |
|
1167 |
pairs. Defines preorders, partial orders, linear orders and |
|
1168 |
well-orders on sets and on types. |
|
26877 | 1169 |
|
25726
9728f319ffc6
* Metis prover an order of magnitude faster, works with multithreading.
wenzelm
parents:
25712
diff
changeset
|
1170 |
|
26197 | 1171 |
*** ZF *** |
1172 |
||
26874 | 1173 |
* Renamed some theories to allow to loading both ZF and HOL in the |
1174 |
same session: |
|
1175 |
||
1176 |
Datatype -> Datatype_ZF |
|
1177 |
Inductive -> Inductive_ZF |
|
1178 |
Int -> Int_ZF |
|
1179 |
IntDiv -> IntDiv_ZF |
|
1180 |
Nat -> Nat_ZF |
|
1181 |
List -> List_ZF |
|
1182 |
Main -> Main_ZF |
|
1183 |
||
1184 |
INCOMPATIBILITY: ZF theories that import individual theories below |
|
1185 |
Main might need to be adapted. Regular theory Main is still |
|
1186 |
available, as trivial extension of Main_ZF. |
|
26197 | 1187 |
|
1188 |
||
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
1189 |
*** ML *** |
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
1190 |
|
27067 | 1191 |
* ML within Isar: antiquotation @{const name} or @{const |
1192 |
name(typargs)} produces statically-checked Const term. |
|
1193 |
||
26401
e7a94081dce7
Functor NamedThmsFun: data is available to the user as dynamic fact;
wenzelm
parents:
26387
diff
changeset
|
1194 |
* 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
|
1195 |
(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
|
1196 |
|
27067 | 1197 |
* Removed obsolete "use_legacy_bindings" function. |
26188 | 1198 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
1199 |
* 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
|
1200 |
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
|
1201 |
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
|
1202 |
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
|
1203 |
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
|
1204 |
|
26874 | 1205 |
* 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
|
1206 |
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
|
1207 |
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
|
1208 |
|
25737
84c92fc48e36
``print mode'' is now a thread-local value derived from a global template;
wenzelm
parents:
25726
diff
changeset
|
1209 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
1210 |
*** System *** |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
1211 |
|
25971 | 1212 |
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- |
1213 |
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
|
1214 |
|
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
1215 |
* isatool tty runs Isabelle process with plain tty interaction; |
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
1216 |
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
|
1217 |
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
|
1218 |
|
25651 | 1219 |
* isatool browser now works with Cygwin as well, using general |
1220 |
"javapath" function defined in Isabelle process environment. |
|
1221 |
||
27067 | 1222 |
* YXML notation provides a simple and efficient alternative to |
1223 |
standard XML transfer syntax. See src/Pure/General/yxml.ML and |
|
1224 |
isatool yxml as described in the Isabelle system manual. |
|
25651 | 1225 |
|
25652 | 1226 |
* JVM class isabelle.IsabelleProcess (located in Isabelle/lib/classes) |
25651 | 1227 |
provides general wrapper for managing an Isabelle process in a robust |
1228 |
fashion, with ``cooked'' output from stdin/stderr. |
|
1229 |
||
25855 | 1230 |
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), |
1231 |
based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). |
|
1232 |
||
27067 | 1233 |
* Removed obsolete THIS_IS_ISABELLE_BUILD feature. NB: the documented |
1234 |
way of changing the user's settings is via |
|
1235 |
ISABELLE_HOME_USER/etc/settings, which is a fully featured bash |
|
1236 |
script. |
|
1237 |
||
1238 |
* Multithreading.max_threads := 0 refers to the number of actual CPU |
|
1239 |
cores of the underlying machine, which is a good starting point for |
|
1240 |
optimal performance tuning. The corresponding usedir option -M allows |
|
1241 |
"max" as an alias for "0". WARNING: does not work on certain versions |
|
1242 |
of Mac OS (with Poly/ML 5.1). |
|
1243 |
||
1244 |
* isabelle-process: non-ML sessions are run with "nice", to reduce the |
|
1245 |
adverse effect of Isabelle flooding interactive front-ends (notably |
|
1246 |
ProofGeneral / XEmacs). |
|
1247 |
||
25626
3000965b1fdf
* isatool tty runs Isabelle process with plain tty interaction;
wenzelm
parents:
25609
diff
changeset
|
1248 |
|
25464
0ca80ce89001
moved new NEWS from Isabelle2007 to this Isabelle version'';
wenzelm
parents:
25459
diff
changeset
|
1249 |
|
25429 | 1250 |
New in Isabelle2007 (November 2007) |
1251 |
----------------------------------- |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
1252 |
|
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
1253 |
*** General *** |
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
1254 |
|
22826 | 1255 |
* More uniform information about legacy features, notably a |
1256 |
warning/error of "Legacy feature: ...", depending on the state of the |
|
23367 | 1257 |
tolerate_legacy_features flag (default true). FUTURE INCOMPATIBILITY: |
1258 |
legacy features will disappear eventually. |
|
22826 | 1259 |
|
17918
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
1260 |
* 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
|
1261 |
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
|
1262 |
fixheaders to convert existing theory files. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
1263 |
|
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
1264 |
* 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
|
1265 |
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
|
1266 |
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
|
1267 |
function use_legacy_bindings. INCOMPATIBILITY. |
93e26302733e
* Theory syntax: discontinued non-Isar format and old Isar headers;
wenzelm
parents:
17890
diff
changeset
|
1268 |
|
22871 | 1269 |
* Theory syntax: some popular names (e.g. 'class', 'declaration', |
1270 |
'fun', 'help', 'if') are now keywords. INCOMPATIBILITY, use double |
|
1271 |
quotes. |
|
19814
faa698d46686
* Theory syntax: some popular names (e.g. "class", "if") are now keywords.
wenzelm
parents:
19783
diff
changeset
|
1272 |
|
23888
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
1273 |
* 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
|
1274 |
header specifications (including optional directories), but not the |
24172
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1275 |
accidental file locations of previously successful loads. The strict |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1276 |
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
|
1277 |
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
|
1278 |
theories simultaneously, just as 'imports' within a theory header |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1279 |
specification, but without merging the results. Potential |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1280 |
INCOMPATIBILITY: may need to refine theory headers and commands |
06e42cf7df4e
theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents:
24110
diff
changeset
|
1281 |
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
|
1282 |
|
babe337cce2d
* Theory loader: be more serious about observing the static theory header specifications;
wenzelm
parents:
23881
diff
changeset
|
1283 |
* 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
|
1284 |
identification, instead of the traditional scheme of full physical |
23889 | 1285 |
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
|
1286 |
(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
|
1287 |
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
|
1288 |
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
|
1289 |
|
24187
8bdf5ca5871f
* Theory loader: old-style ML proof scripts are considered a legacy feature;
wenzelm
parents:
24172
diff
changeset
|
1290 |
* 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
|
1291 |
file (with the same base name as the theory) are considered a legacy |
24800 | 1292 |
feature, which will disappear eventually. Even now, the theory loader |
1293 |
no longer maintains dependencies on such files. |
|
1294 |
||
1295 |
* Syntax: the scope for resolving ambiguities via type-inference is |
|
1296 |
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
|
1297 |
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
|
1298 |
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
|
1299 |
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
|
1300 |
'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
|
1301 |
|
25034 | 1302 |
* Syntax: constants introduced by new-style packages ('definition', |
1303 |
'abbreviation' etc.) are passed through the syntax module in |
|
1304 |
``authentic mode''. This means that associated mixfix annotations |
|
1305 |
really stick to such constants, independently of potential name space |
|
1306 |
ambiguities introduced later on. INCOMPATIBILITY: constants in parse |
|
1307 |
trees are represented slightly differently, may need to adapt syntax |
|
1308 |
translations accordingly. Use CONST marker in 'translations' and |
|
1309 |
@{const_syntax} antiquotation in 'parse_translation' etc. |
|
1310 |
||
17981
2602be0d99ae
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
wenzelm
parents:
17918
diff
changeset
|
1311 |
* 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
|
1312 |
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
|
1313 |
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
|
1314 |
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
|
1315 |
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
|
1316 |
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
|
1317 |
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
|
1318 |
|
23379
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
1319 |
* Command 'find_theorems': supports "*" wild-card in "name:" |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
1320 |
criterion; "with_dups" option. Certain ProofGeneral versions might |
d0e3f790bd73
updated 'find_theorems' -- moved ProofGeneral specifics to ProofGeneral/CHANGES;
wenzelm
parents:
23377
diff
changeset
|
1321 |
support a specific search form (see ProofGeneral/CHANGES). |
22965 | 1322 |
|
20370 | 1323 |
* The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1 |
1324 |
by default, which means that "prems" (and also "fixed variables") are |
|
1325 |
suppressed from proof state output. Note that the ProofGeneral |
|
1326 |
settings mechanism allows to change and save options persistently, but |
|
1327 |
older versions of Isabelle will fail to start up if a negative prems |
|
1328 |
limit is imposed. |
|
1329 |
||
21308
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1330 |
* 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
|
1331 |
``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
|
1332 |
contain definitions, theorems etc., including any derived mechanism |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1333 |
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
|
1334 |
generalizes the existing ``theorem (in ...)'' towards more versatility |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1335 |
and scalability. |
73883a528b26
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
wenzelm
parents:
21265
diff
changeset
|
1336 |
|
21960
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
1337 |
* 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
|
1338 |
discontinued Isabelle/classic mode (ML proof scripts). |
0574f192b78a
* Proof General: proper undo of final 'end'; discontinued Isabelle/classic;
wenzelm
parents:
21896
diff
changeset
|
1339 |
|
17754
58a306d9f736
* Command 'find_theorems': support * wildcard in name: criterion.
wenzelm
parents:
17725
diff
changeset
|
1340 |
|
17865 | 1341 |
*** Document preparation *** |
1342 |
||
21717 | 1343 |
* Added antiquotation @{theory name} which prints the given name, |
1344 |
after checking that it refers to a valid ancestor theory in the |
|
1345 |
current context. |
|
21339 | 1346 |
|
17869 | 1347 |
* Added antiquotations @{ML_type text} and @{ML_struct text} which |
1348 |
check the given source text as ML type/structure, printing verbatim. |
|
17865 | 1349 |
|
21717 | 1350 |
* Added antiquotation @{abbrev "c args"} which prints the abbreviation |
1351 |
"c args == rhs" given in the current context. (Any number of |
|
21735 | 1352 |
arguments may be given on the LHS.) |
21717 | 1353 |
|
1354 |
||
17779 | 1355 |
*** Pure *** |
1356 |
||
24800 | 1357 |
* The 'class' package offers a combination of axclass and locale to |
25129 | 1358 |
achieve Haskell-like type classes in Isabelle. Definitions and |
1359 |
theorems within a class context produce both relative results (with |
|
1360 |
implicit parameters according to the locale context), and polymorphic |
|
1361 |
constants with qualified polymorphism (according to the class |
|
1362 |
context). Within the body context of a 'class' target, a separate |
|
1363 |
syntax layer ("user space type system") takes care of converting |
|
1364 |
between global polymorphic consts and internal locale representation. |
|
25177 | 1365 |
See src/HOL/ex/Classpackage.thy for examples (as well as main HOL). |
25184 | 1366 |
"isatool doc classes" provides a tutorial. |
20807 | 1367 |
|
25199 | 1368 |
* Generic code generator framework allows to generate executable |
24800 | 1369 |
code for ML and Haskell (including Isabelle classes). A short usage |
1370 |
sketch: |
|
20188
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1371 |
|
8b22026445af
added notes on class_package.ML and codegen_package.ML
haftmann
parents:
20169
diff
changeset
|
1372 |
internal compilation: |
25199 | 1373 |
export_code <list of constants (term syntax)> in SML |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1374 |
writing SML code to a file: |
25199 | 1375 |
export_code <list of constants (term syntax)> in SML <filename> |
22735 | 1376 |
writing OCaml code to a file: |
25199 | 1377 |
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
|
1378 |
writing Haskell code to a bunch of files: |
25199 | 1379 |
export_code <list of constants (term syntax)> in Haskell <filename> |
1380 |
||
1381 |
evaluating closed propositions to True/False using code generation: |
|
25184 | 1382 |
method ``eval'' |
1383 |
||
1384 |
Reasonable default setup of framework in HOL. |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1385 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1386 |
Theorem attributs for selecting and transforming function equations theorems: |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20375
diff
changeset
|
1387 |
|
22845 | 1388 |
[code fun]: select a theorem as function equation for a specific constant |
1389 |
[code fun del]: deselect a theorem as function equation for a specific constant |
|
1390 |
[code inline]: select an equation theorem for unfolding (inlining) in place |
|
1391 |
[code inline del]: deselect an equation theorem for unfolding (inlining) in place |
|
20453 |