author  wenzelm 
Sat, 18 Mar 2000 19:16:56 +0100  
changeset 8518  daaedc7b56a9 
parent 8487  5f3b0e02ec15 
child 8534  fdbabfbc3829 
permissions  rwrr 
7986  1 

5363  2 
Isabelle NEWS  history userrelevant changes 
3 
============================================== 

2553  4 

8015  5 
New in this Isabelle version 
6 
 

7 

8014  8 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
9 

10 
* HOL: the constant for f``x is now "image" rather than "op ``". 

11 

8518  12 
* HOL: exhaust_tac on datatypes superceded by new generic case_tac; 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

13 

8518  14 
* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

15 

8014  16 

8487  17 
*** Document preparation *** 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

18 

a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

19 
* isatool mkdir provides easy setup of Isabelle session directories, 
8518  20 
including proper document sources; 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

21 

a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

22 
* generated LaTeX sources are now deleted after successful run 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

23 
(isatool document c); may retain a copy somewhere else via D option 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

24 
of isatool usedir; 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

25 

8518  26 
* oldstyle theories now produce (crude) LaTeX output as well; 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

27 

a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

28 

8184  29 
*** Isar *** 
30 

8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

31 
* Pure now provides its own version of intro/elim/dest attributes; 
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

32 
useful for building new logics, but beware of confusion with the 
8518  33 
Provers/classical ones; 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

34 

8518  35 
* Pure: new 'obtain' language element supports generalized elimination 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

36 
proofs; 
8184  37 

8487  38 
* Pure: scalable support for caseanalysis type proofs: new 'case' 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

39 
language element refers to local contexts symbolically, as produced by 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

40 
certain proof methods; internally, case names are attached to theorems 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

41 
as "tags"; 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

42 

8487  43 
* Provers: splitter support (via 'split' attribute and 'simp' method 
44 
modifier); 'simp' method: 'only:' modifier removes loopers as well 

45 
(including splits); 

46 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

47 
* HOL: new proof method 'cases' and improved version of 'induct' now 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

48 
support named cases; major packages (inductive, datatype, primrec, 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

49 
recdef) support case names and properly name parameters; 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

50 

d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

51 
* HOL: removed 'case_split' thm binding, should use 'cases' proof 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

52 
method anyway; 
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

53 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

54 
* names of theorems etc. may be natural numbers as well; 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

55 

8518  56 
* Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??; 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

57 

8487  58 
* 'pr' command: optional goals_limit argument; 
59 

60 
* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit 

8518  61 
additional print modes to be specified; e.g. "pr(latex)" will print 
62 
proof state according to the Isabelle LaTeX style; 

8487  63 

8184  64 

8014  65 
*** HOL *** 
66 

8518  67 
* HOL/Algebra: new theory of rings and univariate polynomials, by 
68 
Clemens Ballarin; 

8014  69 

8271
7602b57ba028
HOL/record: fixed selectupdate simplification procedure to handle
wenzelm
parents:
8203
diff
changeset

70 
* HOL/record: fixed selectupdate simplification procedure to handle 
8283
0a319c5746eb
* Pure now provides its own version of intro/elim/dest attributes;
wenzelm
parents:
8271
diff
changeset

71 
extended records as well; admit "r" as field name; 
8271
7602b57ba028
HOL/record: fixed selectupdate simplification procedure to handle
wenzelm
parents:
8203
diff
changeset

72 

8392  73 
* HOL/ex: new theory Factorization proving the Fundamental Theorem of 
74 
Arithmetic, by Thomas M Rasmussen; 

8007  75 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

76 
* new version of "case_tac" subsumes both boolean case split and 
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

77 
"exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer 
8518  78 
exists, may define val exhaust_tac = case_tac for adhoc portability; 
8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

79 

8412  80 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

81 
*** General *** 
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

82 

a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

83 
* compression of ML heaps images may now be controlled via c option 
8518  84 
of isabelle and isatool usedir (currently only observed by Poly/ML); 
8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

85 

8518  86 
* ML: new combinators >> and >>> for incremental transformations 
87 
with secondary results (e.g. certain theory extensions): 

8440
d66f0f14b1ca
* HOL: exhaust_tac on datatypes superceded by new case_tac;
wenzelm
parents:
8425
diff
changeset

88 

8358
a57d72b5d272
* isatool mkdir provides easy setup of Isabelle session directories,
wenzelm
parents:
8283
diff
changeset

89 

8015  90 

7986  91 
New in Isabelle99 (October 1999) 
92 
 

4649  93 

5931  94 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
95 

6922  96 
* HOL: The THEN and ELSE parts of conditional expressions (if P then x else y) 
97 
are no longer simplified. (This allows the simplifier to unfold recursive 

98 
functional programs.) To restore the old behaviour, declare 

7215  99 

100 
Delcongs [if_weak_cong]; 

6922  101 

6269  102 
* HOL: Removed the obsolete syntax "Compl A"; use A for set 
103 
complement; 

5931  104 

6269  105 
* HOL: the predicate "inj" is now defined by translation to "inj_on"; 
6174  106 

7847  107 
* HOL/datatype: mutual_induct_tac no longer exists  
108 
use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"] 

109 

6386
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

110 
* HOL/typedef: fixed type inference for representing set; type 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

111 
arguments now have to occur explicitly on the rhs as type constraints; 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

112 

6269  113 
* ZF: The con_defs part of an inductive definition may no longer refer 
114 
to constants declared in the same theory; 

6057  115 

6269  116 
* HOL, ZF: the function mk_cases, generated by the inductive 
117 
definition package, has lost an argument. To simplify its result, it 

118 
uses the default simpset instead of a supplied list of theorems. 

6141  119 

7215  120 
* HOL/List: the constructors of type list are now Nil and Cons; 
121 

7619  122 
* Simplifier: the type of the infix ML functions 
123 
setSSolver addSSolver setSolver addSolver 

124 
is now simpset * solver > simpset where `solver' is a new abstract type 

125 
for packaging solvers. A solver is created via 

126 
mk_solver: string > (thm list > int > tactic) > solver 

127 
where the string argument is only a comment. 

6057  128 

7647
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

129 

6069  130 
*** Proof tools *** 
131 

6343  132 
* Provers/Arith/fast_lin_arith.ML contains a functor for creating a 
133 
decision procedure for linear arithmetic. Currently it is used for 

7593  134 
types `nat', `int', and `real' in HOL (see below); it can, should and 
135 
will be instantiated for other types and logics as well. 

6069  136 

7324  137 
* The simplifier now accepts rewrite rules with flexible heads, eg 
138 
hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y 

139 
They are applied like any rule with a nonpattern lhs, i.e. by firstorder 

140 
matching. 

6069  141 

7593  142 

6014  143 
*** General *** 
144 

7986  145 
* New Isabelle/Isar subsystem provides an alternative to traditional 
7215  146 
tactical theorem proving; together with the ProofGeneral/isar user 
147 
interface it offers an interactive environment for developing human 

148 
readable proof documents (Isar == Intelligible semiautomated 

7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

149 
reasoning); for further information see isatool doc isarref, 
7986  150 
src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/ 
7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

151 

8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

152 
* improved presentation of theories: better HTML markup (including 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

153 
colors), graph views in several sizes; isatool usedir now provides a 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

154 
proper interface for user theories (via P option); actual document 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

155 
preparation based on (PDF)LaTeX is available as well (for newstyle 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

156 
theories only); see isatool doc system for more information; 
7215  157 

7252  158 
* native support for Proof General, both for classic Isabelle and 
7986  159 
Isabelle/Isar; 
7215  160 

7791  161 
* ML function thm_deps visualizes dependencies of theorems and lemmas, 
162 
using the graph browser tool; 

163 

6751  164 
* Isabelle manuals now also available as PDF; 
165 

6449  166 
* theory loader rewritten from scratch (may not be fully 
167 
bugcompatible); old loadpath variable has been replaced by show_path, 

6671  168 
add_path, del_path, reset_path functions; new operations such as 
7593  169 
update_thy, touch_thy, remove_thy, use/update_thy_only (see also 
170 
isatool doc ref); 

6449  171 

7215  172 
* improved isatool install: option k creates KDE application icon, 
173 
option p DIR installs standalone binaries; 

174 

175 
* added ML_PLATFORM setting (useful for crossplatform installations); 

176 
more robust handling of platform specific ML images for SML/NJ; 

177 

7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

178 
* the settings environment is now statically scoped, i.e. it is never 
7986  179 
created again in subprocesses invoked from isabelle, isatool, or 
7886
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

180 
Isabelle; 
8fa551e22e52
the settings environment is now statically scoped;
wenzelm
parents:
7863
diff
changeset

181 

7215  182 
* path element specification '~~' refers to '$ISABELLE_HOME'; 
183 

6343  184 
* in locales, the "assumes" and "defines" parts may be omitted if 
185 
empty; 

5973  186 

6269  187 
* new print_mode "xsymbols" for extended symbol support (e.g. genuine 
188 
long arrows); 

6259
488bdc1bd11a
path element specification '~~' refers to '$ISABELLE_HOME';
wenzelm
parents:
6174
diff
changeset

189 

6343  190 
* new print_mode "HTML"; 
191 

192 
* new flag show_tags controls display of tags of theorems (which are 

193 
basically just comments that may be attached by some tools); 

194 

6461  195 
* Isamode 2.6 requires patch to accomodate change of Isabelle font 
196 
mode and goal output format: 

197 

198 
diff r Isamode2.6/elisp/isaload.el Isamode/elisp/isaload.el 

199 
244c244 

200 
< (list (isagetenv "ISABELLE") "msymbols" logicname) 

201 
 

6533  202 
> (list (isagetenv "ISABELLE") "misabelle_font" "msymbols" logicname) 
6461  203 
diff r Isabelle2.6/elisp/isaproofstate.el Isamode/elisp/isaproofstate.el 
204 
181c181 

205 
< (defconst proofstateproofstartregexp "^Level [09]+$" 

206 
 

207 
> (defconst proofstateproofstartregexp "^Level [09]+" 

208 

7450  209 
* function bind_thms stores lists of theorems (cf. bind_thm); 
210 

7593  211 
* new shorthand tactics ftac, eatac, datac, fatac; 
212 

213 
* qed (and friends) now accept "" as result name; in that case the 

7986  214 
theorem is not stored, but proper checks and presentation of the 
215 
result still apply; 

7593  216 

7805
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

217 
* theorem database now also indexes constants "Trueprop", "all", 
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

218 
"==>", "=="; thus thms_containing, findI etc. may retrieve more rules; 
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7791
diff
changeset

219 

6028  220 

6057  221 
*** HOL *** 
222 

7215  223 
** HOL arithmetic ** 
224 

6343  225 
* There are now decision procedures for linear arithmetic over nat and 
226 
int: 

6131  227 

6343  228 
1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', 
229 
`+', `', `Suc', `min', `max' and numerical constants; other subterms 

230 
are treated as atomic; subformulae not involving type `nat' or `int' 

231 
are ignored; quantified subformulae are ignored unless they are 

232 
positive universal or negative existential. The tactic has to be 

233 
invoked by hand and can be a little bit slow. In particular, the 

234 
running time is exponential in the number of occurrences of `min' and 

235 
`max', and `' on `nat'. 

6131  236 

6343  237 
2. fast_arith_tac is a cutdown version of arith_tac: it only takes 
238 
(negated) (in)equalities among the premises and the conclusion into 

239 
account (i.e. no compound formulae) and does not know about `min' and 

240 
`max', and `' on `nat'. It is fast and is used automatically by the 

241 
simplifier. 

6131  242 

6343  243 
NB: At the moment, these decision procedures do not cope with mixed 
244 
nat/int formulae where the two parts interact, such as `m < n ==> 

245 
int(m) < int(n)'. 

6028  246 

7215  247 
* HOL/Numeral provides a generic theory of numerals (encoded 
7313  248 
efficiently as bit strings); setup for types nat/int/real is in place; 
7215  249 
INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than 
250 
int, existing theories and proof scripts may require a few additional 

251 
type constraints; 

252 

253 
* integer division and remainder can now be performed on constant 

254 
arguments; 

7157  255 

7215  256 
* many properties of integer multiplication, division and remainder 
257 
are now available; 

6922  258 

7287  259 
* An interface to the Stanford Validity Checker (SVC) is available through the 
260 
tactic svc_tac. Propositional tautologies and theorems of linear arithmetic 

261 
are proved automatically. SVC must be installed separately, and its results 

262 
must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any 

263 
invocation of the underlying oracle). For SVC see 

7444  264 
http://verify.stanford.edu/SVC 
6922  265 

7125  266 
* IsaMakefile: the HOLReal target now builds an actual image; 
267 

7215  268 

269 
** HOL misc ** 

270 

7595
5f5d575ddac3
* HOL/Real/HahnBanach: the HahnBanach theorem for real vector spaces
wenzelm
parents:
7593
diff
changeset

271 
* HOL/Real/HahnBanach: the HahnBanach theorem for real vector spaces 
5f5d575ddac3
* HOL/Real/HahnBanach: the HahnBanach theorem for real vector spaces
wenzelm
parents:
7593
diff
changeset

272 
(in Isabelle/Isar)  by Gertrud Bauer; 
5f5d575ddac3
* HOL/Real/HahnBanach: the HahnBanach theorem for real vector spaces
wenzelm
parents:
7593
diff
changeset

273 

7691  274 
* HOL/BCV: generic model of bytecode verification, i.e. dataflow 
275 
analysis for assembly languages with subtypes; 

276 

6278  277 
* HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization 
278 
 avoids syntactic ambiguities and treats state, transition, and 

279 
temporal levels more uniformly; introduces INCOMPATIBILITIES due to 

280 
changed syntax and (many) tactics; 

281 

7791  282 
* HOL/inductive: Now also handles more general introduction rules such 
283 
as "ALL y. (y, x) : r > y : acc r ==> x : acc r"; monotonicity 

284 
theorems are now maintained within the theory (maintained via the 

285 
"mono" attribute); 

7780
099742c562aa
Documented changes to HOL/inductive and function thm_deps.
berghofe
parents:
7691
diff
changeset

286 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

287 
* HOL/datatype: Now also handles arbitrarily branching datatypes 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

288 
(using function types) such as 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

289 

36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

290 
datatype 'a tree = Atom 'a  Branch "nat => 'a tree" 
7047
d103b875ef1d
Datatype package now handles arbitrarily branching datatypes.
berghofe
parents:
6925
diff
changeset

291 

7326  292 
* HOL/record: record_simproc (part of the default simpset) takes care 
293 
of selectors applied to updated records; record_split_tac is no longer 

7327  294 
part of the default claset; update_defs may now be removed from the 
295 
simpset in many cases; COMPATIBILITY: old behavior achieved by 

7326  296 

297 
claset_ref () := claset() addSWrapper record_split_wrapper; 

298 
Delsimprocs [record_simproc] 

299 

6386
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

300 
* HOL/typedef: fixed type inference for representing set; type 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

301 
arguments now have to occur explicitly on the rhs as type constraints; 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

302 

7287  303 
* HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem 
304 
names rather than an ML expression; 

305 

306 
* HOL/defer_recdef (TFL): like recdef but the wellfounded relation can be 

307 
supplied later. Program schemes can be defined, such as 

308 
"While B C s = (if B s then While B C (C s) else s)" 

309 
where the wellfounded relation can be chosen after B and C have been given. 

6563  310 

7215  311 
* HOL/List: the constructors of type list are now Nil and Cons; 
312 
INCOMPATIBILITY: while [] and infix # syntax is still there, of 

313 
course, ML tools referring to List.list.op # etc. have to be adapted; 

314 

7238
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

315 
* HOL_quantifiers flag superseded by "HOL" print mode, which is 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

316 
disabled by default; run isabelle with option m HOL to get back to 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

317 
the original Gordon/HOLstyle output; 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

318 

36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

319 
* HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P, 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

320 
ALL x<=y. P, EX x<y. P, EX x<=y. P; 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

321 

36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

322 
* HOL basic syntax simplified (more orthogonal): all variants of 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

323 
All/Ex now support plain / symbolic / HOL notation; plain syntax for 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

324 
Eps operator is provided as well: "SOME x. P[x]"; 
36e58620ffc8
replaced HOL_quantifiers flag by "HOL" print mode;
wenzelm
parents:
7216
diff
changeset

325 

7320  326 
* HOL/Sum.thy: sum_case has been moved to HOL/Datatype; 
7261  327 

7280  328 
* HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made 
329 
thus available for user theories; 

330 

7300
8439bf404c28
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
wenzelm
parents:
7287
diff
changeset

331 
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with 
8439bf404c28
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
wenzelm
parents:
7287
diff
changeset

332 
HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the 
8439bf404c28
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
wenzelm
parents:
7287
diff
changeset

333 
time; 
8439bf404c28
* HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
wenzelm
parents:
7287
diff
changeset

334 

7986  335 
* HOL: new tactic smp_tac: int > int > tactic, which applies spec 
336 
several times and then mp; 

7492  337 

7215  338 

7113  339 
*** LK *** 
340 

7215  341 
* the notation <<...>> is now available as a notation for sequences of 
342 
formulas; 

7113  343 

344 
* the simplifier is now installed 

345 

346 
* the axiom system has been generalized (thanks to Soren Heilmann) 

347 

348 
* the classical reasoner now has a default rule database 

349 

350 

6064  351 
*** ZF *** 
352 

353 
* new primrec section allows primitive recursive functions to be given 

6269  354 
directly (as in HOL) over datatypes and the natural numbers; 
6064  355 

6269  356 
* new tactics induct_tac and exhaust_tac for induction (or case 
357 
analysis) over datatypes and the natural numbers; 

6064  358 

359 
* the datatype declaration of type T now defines the recursor T_rec; 

360 

6141  361 
* simplification automatically does freeness reasoning for datatype 
6269  362 
constructors; 
6141  363 

6269  364 
* automatic typeinference, with AddTCs command to insert new 
365 
typechecking rules; 

6155  366 

6269  367 
* datatype introduction rules are now added as Safe Introduction rules 
368 
to the claset; 

6155  369 

6269  370 
* the syntax "if P then x else y" is now available in addition to 
371 
if(P,x,y); 

372 

6069  373 

6343  374 
*** Internal programming interfaces *** 
375 

7919
35c18affc1d8
tuned simplifier trace output; new flag debug_simp
wenzelm
parents:
7886
diff
changeset

376 
* tuned simplifier trace output; new flag debug_simp; 
35c18affc1d8
tuned simplifier trace output; new flag debug_simp
wenzelm
parents:
7886
diff
changeset

377 

7420
cba45c114f3b
structures Vartab / Termtab (instances of TableFun);
wenzelm
parents:
7327
diff
changeset

378 
* structures Vartab / Termtab (instances of TableFun) offer efficient 
cba45c114f3b
structures Vartab / Termtab (instances of TableFun);
wenzelm
parents:
7327
diff
changeset

379 
tables indexed by indexname_ord / term_ord (compatible with aconv); 
cba45c114f3b
structures Vartab / Termtab (instances of TableFun);
wenzelm
parents:
7327
diff
changeset

380 

6386
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

381 
* AxClass.axclass_tac lost the theory argument; 
e9e8af97f48f
HOL/typedef: fixed type inference for representing set;
wenzelm
parents:
6343
diff
changeset

382 

6343  383 
* tuned current_goals_markers semantics: begin / end goal avoids 
384 
printing empty lines; 

385 

386 
* removed prs and prs_fn hook, which was broken because it did not 

387 
include \n in its semantics, forcing writeln to add one 

388 
uncoditionally; replaced prs_fn by writeln_fn; consider std_output: 

389 
string > unit if you really want to output text without newline; 

390 

391 
* Symbol.output subject to print mode; INCOMPATIBILITY: defaults to 

392 
plain output, interface builders may have to enable 'isabelle_font' 

393 
mode to get Isabelle font glyphs as before; 

394 

395 
* refined token_translation interface; INCOMPATIBILITY: output length 

396 
now of type real instead of int; 

397 

7196  398 
* theory loader actions may be traced via new ThyInfo.add_hook 
399 
interface (see src/Pure/Thy/thy_info.ML); example application: keep 

400 
your own database of information attached to *whole* theories  as 

401 
opposed to intratheory data slots offered via TheoryDataFun; 

402 

7647
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

403 
* proper handling of dangling sort hypotheses (at last!); 
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

404 
Thm.strip_shyps and Drule.strip_shyps_warning take care of removing 
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

405 
extra sort hypotheses that can be witnessed from the type signature; 
7986  406 
the force_strip_shyps flag is gone, any remaining shyps are simply 
407 
left in the theorem (with a warning issued by strip_shyps_warning); 

7647
2ceddd91cd0a
proper handling of dangling sort hypotheses (at last!);
wenzelm
parents:
7619
diff
changeset

408 

6343  409 

6064  410 

5781  411 
New in Isabelle981 (October 1998) 
412 
 

413 

5127  414 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
4842  415 

5726  416 
* several changes of automated proof tools; 
5373  417 

5726  418 
* HOL: major changes to the inductive and datatype packages, including 
419 
some minor incompatibilities of theory syntax; 

5214  420 

5726  421 
* HOL: renamed r^1 to 'converse' from 'inverse'; 'inj_onto' is now 
5217  422 
called `inj_on'; 
5160  423 

5275  424 
* HOL: removed duplicate thms in Arith: 
425 
less_imp_add_less should be replaced by trans_less_add1 

426 
le_imp_add_le should be replaced by trans_le_add1 

5160  427 

5726  428 
* HOL: unary minus is now overloaded (new type constraints may be 
429 
required); 

5490  430 

5726  431 
* HOL and ZF: unary minus for integers is now # instead of #~. In 
432 
ZF, expressions such as n#1 must be changed to n# 1, since #1 is 

433 
now taken as an integer constant. 

5541  434 

5726  435 
* Pure: ML function 'theory_of' renamed to 'theory'; 
5397
034ed25535b9
* Pure: ML function 'theory_of' replaced by 'theory';
wenzelm
parents:
5373
diff
changeset

436 

5363  437 

5127  438 
*** Proof tools *** 
4880  439 

5657
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

440 
* Simplifier: 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

441 
1. Asm_full_simp_tac is now more aggressive. 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

442 
1. It will sometimes reorient premises if that increases their power to 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

443 
simplify. 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

444 
2. It does no longer proceed strictly from left to right but may also 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

445 
rotate premises to achieve further simplification. 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

446 
For compatibility reasons there is now Asm_lr_simp_tac which is like the 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

447 
old Asm_full_simp_tac in that it does not rotate premises. 
1a6c9c6a3f8e
2. The simplifier now knows a little bit about natarithmetic.
nipkow
parents:
5651
diff
changeset

448 
2. The simplifier now knows a little bit about natarithmetic. 
4880  449 

5127  450 
* Classical reasoner: wrapper mechanism for the classical reasoner now 
451 
allows for selected deletion of wrappers, by introduction of names for 

452 
wrapper functionals. This implies that addbefore, addSbefore, 

453 
addaltern, and addSaltern now take a pair (name, tactic) as argument, 

454 
and that adding two tactics with the same name overwrites the first 

455 
one (emitting a warning). 

4824  456 
type wrapper = (int > tactic) > (int > tactic) 
4649  457 
setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by 
4824  458 
addWrapper, addSWrapper: claset * (string * wrapper) > claset 
459 
delWrapper, delSWrapper: claset * string > claset 

4649  460 
getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; 
461 

5705
56f2030c46c6
tuned (all proofs are INSTABLE by David's definition of instability);
wenzelm
parents:
5671
diff
changeset

462 
* Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE 
5726  463 
semantics; addbefore now affects only the unsafe part of step_tac 
464 
etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY 

465 
FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac 

466 
by Force_tac; 

5524  467 

5726  468 
* Classical reasoner: setwrapper to setWrapper and compwrapper to 
469 
compWrapper; added safe wrapper (and access functions for it); 

5524  470 

5127  471 
* HOL/split_all_tac is now much faster and fails if there is nothing 
5726  472 
to split. Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order 
473 
and the names of the automatically generated variables have changed. 

474 
split_all_tac has moved within claset() from unsafe wrappers to safe 

475 
wrappers, which means that !!bound variables are split much more 

476 
aggressively, and safe_tac and clarify_tac now split such variables. 

477 
If this splitting is not appropriate, use delSWrapper "split_all_tac". 

478 
Note: the same holds for record_split_tac, which does the job of 

479 
split_all_tac for record fields. 

5127  480 

5726  481 
* HOL/Simplifier: Rewrite rules for case distinctions can now be added 
482 
permanently to the default simpset using Addsplits just like 

483 
Addsimps. They can be removed via Delsplits just like 

484 
Delsimps. Lowercase versions are also available. 

5127  485 

5726  486 
* HOL/Simplifier: The rule split_if is now part of the default 
487 
simpset. This means that the simplifier will eliminate all occurrences 

488 
of ifthenelse in the conclusion of a goal. To prevent this, you can 

489 
either remove split_if completely from the default simpset by 

490 
`Delsplits [split_if]' or remove it in a specific call of the 

491 
simplifier using `... delsplits [split_if]'. You can also add/delete 

492 
other case splitting rules to/from the default simpset: every datatype 

493 
generates suitable rules `split_t_case' and `split_t_case_asm' (where 

494 
t is the name of the datatype). 

5127  495 

5726  496 
* Classical reasoner / Simplifier combination: new force_tac (and 
5127  497 
derivatives Force_tac, force) combines rewriting and classical 
498 
reasoning (and whatever other tools) similarly to auto_tac, but is 

5726  499 
aimed to solve the given subgoal completely. 
5127  500 

501 

502 
*** General *** 

503 

5217  504 
* new toplevel commands `Goal' and `Goalw' that improve upon `goal' 
5127  505 
and `goalw': the theory is no longer needed as an explicit argument  
506 
the current theory context is used; assumptions are no longer returned 

507 
at the MLlevel unless one of them starts with ==> or !!; it is 

5217  508 
recommended to convert to these new commands using isatool fixgoal 
509 
(backup your sources first!); 

4842  510 

5217  511 
* new toplevel commands 'thm' and 'thms' for retrieving theorems from 
5207  512 
the current theory context, and 'theory' to lookup stored theories; 
4806  513 

5722  514 
* new theory section 'locale' for declaring constants, assumptions and 
515 
definitions that have local scope; 

516 

5127  517 
* new theory section 'nonterminals' for purely syntactic types; 
4858  518 

5127  519 
* new theory section 'setup' for generic ML setup functions 
520 
(e.g. package initialization); 

4869  521 

5131  522 
* the distribution now includes Isabelle icons: see 
523 
lib/logo/isabelle{small,tiny}.xpm; 

524 

5363  525 
* isatool install  install binaries with absolute references to 
526 
ISABELLE_HOME/bin; 

527 

5572  528 
* isatool logo  create instances of the Isabelle logo (as EPS); 
529 

5407  530 
* print mode 'emacs' reserved for Isamode; 
531 

5726  532 
* support multiple print (ast) translations per constant name; 
533 

6925
8d4d45ec6a3d
theorems involving oracles are now printed with a suffixed [!];
wenzelm
parents:
6922
diff
changeset

534 
* theorems involving oracles are now printed with a suffixed [!]; 
8d4d45ec6a3d
theorems involving oracles are now printed with a suffixed [!];
wenzelm
parents:
6922
diff
changeset

535 

4711  536 

4661  537 
*** HOL *** 
538 

5710  539 
* there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial'); 
5709  540 

5217  541 
* HOL/inductive package reorganized and improved: now supports mutual 
5267  542 
definitions such as 
5217  543 

544 
inductive EVEN ODD 

545 
intrs 

546 
null "0 : EVEN" 

547 
oddI "n : EVEN ==> Suc n : ODD" 

548 
evenI "n : ODD ==> Suc n : EVEN" 

549 

550 
new theorem list "elims" contains an elimination rule for each of the 

551 
recursive sets; inductive definitions now handle disjunctive premises 

552 
correctly (also ZF); 

5214  553 

5217  554 
INCOMPATIBILITIES: requires Inductive as an ancestor; component 
555 
"mutual_induct" no longer exists  the induction rule is always 

556 
contained in "induct"; 

557 

558 

559 
* HOL/datatype package reimplemented and greatly improved: now 

5267  560 
supports mutually recursive datatypes such as 
5217  561 

562 
datatype 

563 
'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp) 

564 
 SUM ('a aexp) ('a aexp) 

565 
 DIFF ('a aexp) ('a aexp) 

566 
 NUM 'a 

567 
and 

568 
'a bexp = LESS ('a aexp) ('a aexp) 

569 
 AND ('a bexp) ('a bexp) 

570 
 OR ('a bexp) ('a bexp) 

571 

5267  572 
as well as indirectly recursive datatypes such as 
5214  573 

5217  574 
datatype 
575 
('a, 'b) term = Var 'a 

576 
 App 'b ((('a, 'b) term) list) 

5214  577 

5217  578 
The new tactic mutual_induct_tac [<var_1>, ..., <var_n>] i performs 
579 
induction on mutually / indirectly recursive datatypes. 

580 

581 
Primrec equations are now stored in theory and can be accessed via 

582 
<function_name>.simps. 

583 

584 
INCOMPATIBILITIES: 

5214  585 

5217  586 
 Theories using datatypes must now have theory Datatype as an 
587 
ancestor. 

588 
 The specific <typename>.induct_tac no longer exists  use the 

589 
generic induct_tac instead. 

5226  590 
 natE has been renamed to nat.exhaust  use exhaust_tac 
5217  591 
instead of res_inst_tac ... natE. Note that the variable 
5226  592 
names in nat.exhaust differ from the names in natE, this 
5217  593 
may cause some "fragile" proofs to fail. 
594 
 The theorems split_<typename>_case and split_<typename>_case_asm 

595 
have been renamed to <typename>.split and <typename>.split_asm. 

596 
 Since default sorts of type variables are now handled correctly, 

597 
some datatype definitions may have to be annotated with explicit 

598 
sort constraints. 

599 
 Primrec definitions no longer require function name and type 

600 
of recursive argument. 

5214  601 

5217  602 
Consider using isatool fixdatatype to adapt your theories and proof 
603 
scripts to the new package (backup your sources first!). 

604 

605 

5726  606 
* HOL/record package: considerably improved implementation; now 
607 
includes concrete syntax for record types, terms, updates; theorems 

608 
for surjective pairing and splitting !!bound record variables; proof 

609 
support is as follows: 

610 

611 
1) standard conversions (selectors or updates applied to record 

612 
constructor terms) are part of the standard simpset; 

613 

614 
2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are 

615 
made part of standard simpset and claset via addIffs; 

616 

617 
3) a tactic for record field splitting (record_split_tac) is part of 

618 
the standard claset (addSWrapper); 

619 

620 
To get a better idea about these rules you may retrieve them via 

621 
something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is 

622 
the name of your record type. 

623 

624 
The split tactic 3) conceptually simplifies by the following rule: 

625 

626 
"(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))" 

627 

628 
Thus any record variable that is bound by metaall will automatically 

629 
blow up into some record constructor term, consequently the 

630 
simplifications of 1), 2) apply. Thus force_tac, auto_tac etc. shall 

631 
solve record problems automatically. 

632 

5214  633 

5125  634 
* reorganized the main HOL image: HOL/Integ and String loaded by 
635 
default; theory Main includes everything; 

636 

5650  637 
* automatic simplification of integer sums and comparisons, using cancellation; 
638 

5526  639 
* added option_map_eq_Some and not_Some_eq to the default simpset and claset; 
5127  640 

641 
* added disj_not1 = "(~P  Q) = (P > Q)" to the default simpset; 

642 

643 
* many new identities for unions, intersections, set difference, etc.; 

644 

645 
* expand_if, expand_split, expand_sum_case and expand_nat_case are now 

646 
called split_if, split_split, split_sum_case and split_nat_case (to go 

647 
with add/delsplits); 

5125  648 

5127  649 
* HOL/Prod introduces simplification procedure unit_eq_proc rewriting 
650 
(?x::unit) = (); this is made part of the default simpset, which COULD 

651 
MAKE EXISTING PROOFS FAIL under rare circumstances (consider 

5207  652 
'Delsimprocs [unit_eq_proc];' as last resort); also note that 
653 
unit_abs_eta_conv is added in order to counter the effect of 

654 
unit_eq_proc on (%u::unit. f u), replacing it by f rather than by 

655 
%u.f(); 

5125  656 

5217  657 
* HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which 
658 
makes more sense); 

5109  659 

5475  660 
* HOL/Set INCOMPATIBILITY: rule `equals0D' is now a wellformed destruct rule; 
661 
It and 'sym RS equals0D' are now in the default claset, giving automatic 

662 
disjointness reasoning but breaking a few old proofs. 

5267  663 

5217  664 
* HOL/Relation INCOMPATIBILITY: renamed the relational operator r^1 
665 
to 'converse' from 'inverse' (for compatibility with ZF and some 

666 
literature); 

5085
8e5a7942fdea
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
wenzelm
parents:
5077
diff
changeset

667 

5127  668 
* HOL/recdef can now declare nonrecursive functions, with {} supplied as 
669 
the wellfounded relation; 

4838  670 

5490  671 
* HOL/Set INCOMPATIBILITY: the complement of set A is now written A instead of 
672 
Compl A. The "Compl" syntax remains available as input syntax for this 

673 
release ONLY. 

674 

5127  675 
* HOL/Update: new theory of function updates: 
676 
f(a:=b) == %x. if x=a then b else f x 

677 
may also be iterated as in f(a:=b,c:=d,...); 

5077
71043526295f
* HOL/List: new function list_update written xs[i:=v] that updates the ith
nipkow
parents:
5075
diff
changeset

678 

5127  679 
* HOL/Vimage: new theory for inverse image of a function, syntax f``B; 
4899  680 

5282  681 
* HOL/List: 
682 
 new function list_update written xs[i:=v] that updates the ith 

683 
list position. May also be iterated as in xs[i:=a,j:=b,...]. 

5428  684 
 new function `upt' written [i..j(] which generates the list 
685 
[i,i+1,...,j1], i.e. the upper bound is excluded. To include the upper 

686 
bound write [i..j], which is a shorthand for [i..j+1(]. 

5282  687 
 new lexicographic orderings and corresponding wellfoundedness theorems. 
4779  688 

5127  689 
* HOL/Arith: 
690 
 removed 'pred' (predecessor) function; 

691 
 generalized some theorems about n1; 

692 
 many new laws about "div" and "mod"; 

693 
 new laws about greatest common divisors (see theory ex/Primes); 

4766  694 

5127  695 
* HOL/Relation: renamed the relational operator r^1 "converse" 
4842  696 
instead of "inverse"; 
4711  697 

5651  698 
* HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness 
699 
of the multiset ordering; 

700 

5127  701 
* directory HOL/Real: a construction of the reals using Dedekind cuts 
5651  702 
(not included by default); 
4835  703 

5127  704 
* directory HOL/UNITY: Chandy and Misra's UNITY formalism; 
4711  705 

5651  706 
* directory HOL/Hoare: a new version of Hoare logic which permits manysorted 
707 
programs, i.e. different program variables may have different types. 

708 

5142  709 
* calling (stac rew i) now fails if "rew" has no effect on the goal 
710 
[previously, this check worked only if the rewrite rule was unconditional] 

5308  711 
Now rew can involve either definitions or equalities (either == or =). 
5002
7b4c2a153738
* improved the theory data mechanism to support real encapsulation;
wenzelm
parents:
4981
diff
changeset

712 

5363  713 

4879
58656c6a3551
"let" is no longer restricted to FOL terms and allows any logical terms
paulson
parents:
4869
diff
changeset

714 
*** ZF *** 
58656c6a3551
"let" is no longer restricted to FOL terms and allows any logical terms
paulson
parents:
4869
diff
changeset

715 

5332  716 
* theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains 
717 
only the theorems proved on ZF.ML; 

5160  718 

5475  719 
* ZF INCOMPATIBILITY: rule `equals0D' is now a wellformed destruct rule; 
720 
It and 'sym RS equals0D' are now in the default claset, giving automatic 

721 
disjointness reasoning but breaking a few old proofs. 

5267  722 

5160  723 
* ZF/Update: new theory of function updates 
724 
with default rewrite rule f(x:=y) ` z = if(z=x, y, f`z) 

725 
may also be iterated as in f(a:=b,c:=d,...); 

726 

4879
58656c6a3551
"let" is no longer restricted to FOL terms and allows any logical terms
paulson
parents:
4869
diff
changeset

727 
* in let x=t in u(x), neither t nor u(x) has to be an FOL term. 
4649  728 

5142  729 
* calling (stac rew i) now fails if "rew" has no effect on the goal 
730 
[previously, this check worked only if the rewrite rule was unconditional] 

5308  731 
Now rew can involve either definitions or equalities (either == or =). 
5142  732 

5160  733 
* case_tac provided for compatibility with HOL 
734 
(like the old excluded_middle_tac, but with subgoals swapped) 

735 

4842  736 

5127  737 
*** Internal programming interfaces *** 
5002
7b4c2a153738
* improved the theory data mechanism to support real encapsulation;
wenzelm
parents:
4981
diff
changeset

738 

5251  739 
* Pure: several new basic modules made available for general use, see 
740 
also src/Pure/README; 

5207  741 

5008  742 
* improved the theory data mechanism to support encapsulation (data 
743 
kind name replaced by private Object.kind, acting as authorization 

5373  744 
key); new typesafe user interface via functor TheoryDataFun; generic 
745 
print_data function becomes basically useless; 

5002
7b4c2a153738
* improved the theory data mechanism to support real encapsulation;
wenzelm
parents:
4981
diff
changeset

746 

5251  747 
* removed global_names compatibility flag  all theory declarations 
748 
are qualified by default; 

749 

5085
8e5a7942fdea
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
wenzelm
parents:
5077
diff
changeset

750 
* module Pure/Syntax now offers quote / antiquote translation 
8e5a7942fdea
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
wenzelm
parents:
5077
diff
changeset

751 
functions (useful for Hoare logic etc. with implicit dependencies); 
5373  752 
see HOL/ex/Antiquote for an example use; 
5085
8e5a7942fdea
simplification procedure unit_eq_proc rewrites (?x::unit) = ();
wenzelm
parents:
5077
diff
changeset

753 

5127  754 
* Simplifier now offers conversions (asm_)(full_)rewrite: simpset > 
755 
cterm > thm; 

756 

5207  757 
* new tactical CHANGED_GOAL for checking that a tactic modifies a 
758 
subgoal; 

5142  759 

5251  760 
* Display.print_goals function moved to Locale.print_goals; 
761 

5731  762 
* standard print function for goals supports current_goals_markers 
763 
variable for marking begin of proof, end of proof, start of goal; the 

764 
default is ("", "", ""); setting current_goals_markers := ("<proof>", 

765 
"</proof>", "<goal>") causes SGML like tagged proof state printing, 

766 
for example; 

767 

5002
7b4c2a153738
* improved the theory data mechanism to support real encapsulation;
wenzelm
parents:
4981
diff
changeset

768 

7b4c2a153738
* improved the theory data mechanism to support real encapsulation;
wenzelm
parents:
4981
diff
changeset

769 

4410  770 
New in Isabelle98 (January 1998) 
771 
 

772 

773 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 

774 

775 
* changed lexical syntax of terms / types: dots made part of long 

776 
identifiers, e.g. "%x.x" no longer possible, should be "%x. x"; 

777 

778 
* simpset (and claset) reference variable replaced by functions 

779 
simpset / simpset_ref; 

780 

781 
* no longer supports theory aliases (via merge) and nontrivial 

782 
implicit merge of thms' signatures; 

783 

784 
* most internal names of constants changed due to qualified names; 

785 

786 
* changed Pure/Sequence interface (see Pure/seq.ML); 

787 

3454  788 

3715  789 
*** General Changes *** 
790 

4174  791 
* hierachically structured name spaces (for consts, types, axms, thms 
3943  792 
etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of 
4108  793 
old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY: 
794 
isatool fixdots ensures space after dots (e.g. "%x. x"); set 

4174  795 
long_names for fully qualified output names; NOTE: ML programs 
796 
(special tactics, packages etc.) referring to internal names may have 

797 
to be adapted to cope with fully qualified names; in case of severe 

798 
backward campatibility problems try setting 'global_names' at compile 

799 
time to have enrything declared within a flat name space; one may also 

800 
fine tune name declarations in theories via the 'global' and 'local' 

801 
section; 

4108  802 

803 
* reimplemented the implicit simpset and claset using the new anytype 

804 
data filed in signatures; references simpset:simpset ref etc. are 

805 
replaced by functions simpset:unit>simpset and 

806 
simpset_ref:unit>simpset ref; COMPATIBILITY: use isatool fixclasimp 

807 
to patch your ML files accordingly; 

3856  808 

3857  809 
* HTML output now includes theory graph data for display with Java 
810 
applet or isatool browser; data generated automatically via isatool 

3901  811 
usedir (see i option, ISABELLE_USEDIR_OPTIONS); 
3857  812 

3856  813 
* defs may now be conditional; improved rewrite_goals_tac to handle 
814 
conditional equations; 

815 

4174  816 
* defs now admits additional type arguments, using TYPE('a) syntax; 
817 

3901  818 
* theory aliases via merge (e.g. M=A+B+C) no longer supported, always 
819 
creates a new theory node; implicit merge of thms' signatures is 

4112  820 
restricted to 'trivial' ones; COMPATIBILITY: one may have to use 
3901  821 
transfer:theory>thm>thm in (rare) cases; 
822 

3968
ec138de716d9
improved handling of draft signatures / theories; draft thms (and
wenzelm
parents:
3964
diff
changeset

823 
* improved handling of draft signatures / theories; draft thms (and 
ec138de716d9
improved handling of draft signatures / theories; draft thms (and
wenzelm
parents:
3964
diff
changeset

824 
ctyps, cterms) are automatically promoted to real ones; 
ec138de716d9
improved handling of draft signatures / theories; draft thms (and
wenzelm
parents:
3964
diff
changeset

825 

3901  826 
* slightly changed interfaces for oracles: admit many per theory, named 
827 
(e.g. oracle foo = mlfun), additional name argument for invoke_oracle; 

828 

829 
* print_goals: optional output of const types (set show_consts and 

830 
show_types); 

3851
fe9932a7cd46
print_goals: optional output of const types (set show_consts);
wenzelm
parents:
3846
diff
changeset

831 

4388  832 
* improved output of warnings (###) and errors (***); 
3697
c5833dfcc2cc
Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
wenzelm
parents:
3671
diff
changeset

833 

4178
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
4174
diff
changeset

834 
* subgoal_tac displays a warning if the new subgoal has type variables; 
e64ff1c1bc70
subgoal_tac displays a warning if the new subgoal has type variables
paulson
parents:
4174
diff
changeset

835 

3715  836 
* removed old README and Makefiles; 
3697
c5833dfcc2cc
Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
wenzelm
parents:
3671
diff
changeset

837 

3856  838 
* replaced print_goals_ref hook by print_current_goals_fn and result_error_fn; 
3670
9fea3562f8c7
replaced print_goals_ref hook by print_current_goals_fn and
wenzelm
parents:
3658
diff
changeset

839 

3715  840 
* removed obsolete init_pps and init_database; 
841 

842 
* deleted the obsolete tactical STATE, which was declared by 

843 
fun STATE tacfun st = tacfun st st; 

844 

4388  845 
* cd and use now support path variables, e.g. $ISABELLE_HOME, or ~ 
846 
(which abbreviates $HOME); 

4269  847 

848 
* changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY: 

849 
use isatool fixseq to adapt your ML programs (this works for fully 

850 
qualified references to the Sequence structure only!); 

851 

4381  852 
* use_thy no longer requires writable current directory; it always 
853 
reloads .ML *and* .thy file, if either one is out of date; 

4269  854 

3715  855 

856 
*** Classical Reasoner *** 

857 

3744  858 
* Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new 
859 
tactics that use classical reasoning to simplify a subgoal without 

860 
splitting it into several subgoals; 

3715  861 

3719  862 
* Safe_tac: like safe_tac but uses the default claset; 
863 

3715  864 

865 
*** Simplifier *** 

866 

867 
* added simplification meta rules: 

868 
(asm_)(full_)simplify: simpset > thm > thm; 

869 

870 
* simplifier.ML no longer part of Pure  has to be loaded by object 

871 
logics (again); 

872 

873 
* added prems argument to simplification procedures; 

874 

4325  875 
* HOL, FOL, ZF: added infix function `addsplits': 
876 
instead of `<simpset> setloop (split_tac <thms>)' 

877 
you can simply write `<simpset> addsplits <thms>' 

878 

3715  879 

880 
*** Syntax *** 

881 

4174  882 
* TYPE('a) syntax for type reflection terms; 
883 

3985  884 
* no longer handles consts with name ""  declare as 'syntax' instead; 
3856  885 

886 
* pretty printer: changed order of mixfix annotation preference (again!); 

3846  887 

3715  888 
* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; 
889 

890 

891 
*** HOL *** 

892 

5726  893 
* HOL: there is a new splitter `split_asm_tac' that can be used e.g. 
4189  894 
with `addloop' of the simplifier to faciliate case splitting in premises. 
895 

4035  896 
* HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions; 
3985  897 

898 
* HOL/Auth: new protocol proofs including some for the Internet 

4035  899 
protocol TLS; 
3985  900 

4125  901 
* HOL/Map: new theory of `maps' a la VDM; 
3982  902 

4335  903 
* HOL/simplifier: simplification procedures nat_cancel_sums for 
904 
cancelling out common nat summands from =, <, <= (in)equalities, or 

905 
differences; simplification procedures nat_cancel_factor for 

906 
cancelling common factor from =, <, <= (in)equalities over natural 

4373  907 
sums; nat_cancel contains both kinds of procedures, it is installed by 
908 
default in Arith.thy  this COULD MAKE EXISTING PROOFS FAIL; 

4335  909 

3580  910 
* HOL/simplifier: terms of the form 
4325  911 
`? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) 
3580  912 
are rewritten to 
4035  913 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', 
914 
and those of the form 

4325  915 
`! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) > R(x)' (or t=x) 
4035  916 
are rewritten to 
917 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) > R(t)', 

918 

919 
* HOL/datatype 

920 
Each datatype `t' now comes with a theorem `split_t_case' of the form 

3580  921 

4035  922 
P(t_case f1 ... fn x) = 
923 
( (!y1 ... ym1. x = C1 y1 ... ym1 > P(f1 y1 ... ym1)) & 

924 
... 

4189  925 
(!y1 ... ymn. x = Cn y1 ... ymn > P(f1 y1 ... ymn)) 
4035  926 
) 
927 

4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4915
diff
changeset

928 
and a theorem `split_t_case_asm' of the form 
4189  929 

930 
P(t_case f1 ... fn x) = 

931 
~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1))  

932 
... 

933 
(? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn)) 

934 
) 

4930
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4915
diff
changeset

935 
which can be added to a simpset via `addsplits'. The existing theorems 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4915
diff
changeset

936 
expand_list_case and expand_option_case have been renamed to 
89271bc4e7ed
extended addsplits and delsplits to handle also split rules for assumptions
oheimb
parents:
4915
diff
changeset

937 
split_list_case and split_option_case. 
4189  938 

4361  939 
* HOL/Arithmetic: 
940 
 `pred n' is automatically converted to `n1'. 

941 
Users are strongly encouraged not to use `pred' any longer, 

942 
because it will disappear altogether at some point. 

943 
 Users are strongly encouraged to write "0 < n" rather than 

944 
"n ~= 0". Theorems and proof tools have been modified towards this 

945 
`standard'. 

4357  946 

4502  947 
* HOL/Lists: 
948 
the function "set_of_list" has been renamed "set" (and its theorems too); 

949 
the function "nth" now takes its arguments in the reverse order and 

950 
has acquired the infix notation "!" as in "xs!n". 

3570  951 

4154  952 
* HOL/Set: UNIV is now a constant and is no longer translated to Compl{}; 
953 

954 
* HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its 

955 
specialist theorems (like UN1_I) are gone. Similarly for (INT x.B x); 

956 

4575  957 
* HOL/record: extensible records with schematic structural subtyping 
958 
(single inheritance); EXPERIMENTAL version demonstrating the encoding, 

959 
still lacks various theorems and concrete record syntax; 

960 

4125  961 

3715  962 
*** HOLCF *** 
3535  963 

4125  964 
* removed "axioms" and "generated by" sections; 
965 

4123  966 
* replaced "ops" section by extended "consts" section, which is capable of 
4125  967 
handling the continuous function space ">" directly; 
968 

969 
* domain package: 

970 
. proves theorems immediately and stores them in the theory, 

971 
. creates hierachical name space, 

972 
. now uses normal mixfix annotations (instead of cinfix...), 

973 
. minor changes to some names and values (for consistency), 

974 
. e.g. cases > casedist, dists_eq > dist_eqs, [take_lemma] > take_lemmas, 

975 
. separator between mutual domain defs: changed "," to "and", 

976 
. improved handling of sort constraints; now they have to 

977 
appear on the lefthand side of the equations only; 

4123  978 

979 
* fixed LAM <x,y,zs>.b syntax; 

3567  980 

3744  981 
* added extended adm_tac to simplifier in HOLCF  can now discharge 
982 
adm (%x. P (t x)), where P is chainfinite and t continuous; 

3579  983 

984 

3719  985 
*** FOL and ZF *** 
986 

5726  987 
* FOL: there is a new splitter `split_asm_tac' that can be used e.g. 
4189  988 
with `addloop' of the simplifier to faciliate case splitting in premises. 
989 

3744  990 
* qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as 
991 
in HOL, they strip ALL and > from proved theorems; 

992 

3719  993 

3579  994 

3006  995 
New in Isabelle948 (May 1997) 
996 
 

2654  997 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

998 
*** General Changes *** 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

999 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1000 
* new utilities to build / run / maintain Isabelle etc. (in parts 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1001 
still somewhat experimental); old Makefiles etc. still functional; 
2971  1002 

3205  1003 
* new 'Isabelle System Manual'; 
1004 

2825  1005 
* INSTALL text, together with ./configure and ./build scripts; 
2773  1006 

3006  1007 
* reimplemented type inference for greater efficiency, better error 
1008 
messages and clean internal interface; 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1009 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1010 
* prlim command for dealing with lots of subgoals (an easier way of 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1011 
setting goals_limit); 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1012 

3006  1013 

1014 
*** Syntax *** 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1015 

3116  1016 
* supports alternative (named) syntax tables (parser and pretty 
1017 
printer); internal interface is provided by add_modesyntax(_i); 

1018 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1019 
* Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1020 
be used in conjunction with the Isabelle symbol font; uses the 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1021 
"symbols" syntax table; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1022 

2705  1023 
* added token_translation interface (may translate name tokens in 
2756  1024 
arbitrary ways, dependent on their type (free, bound, tfree, ...) and 
3116  1025 
the current print_mode); IMPORTANT: user print translation functions 
1026 
are responsible for marking newly introduced bounds 

1027 
(Syntax.mark_boundT); 

2705  1028 

2730  1029 
* token translations for modes "xterm" and "xterm_color" that display 
3006  1030 
names in bold, underline etc. or colors (which requires a color 
1031 
version of xterm); 

2730  1032 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1033 
* infixes may now be declared with names independent of their syntax; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1034 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1035 
* added typed_print_translation (like print_translation, but may 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1036 
access type of constant); 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1037 

3006  1038 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1039 
*** Classical Reasoner *** 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1040 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1041 
Blast_tac: a new tactic! It is often more powerful than fast_tac, but has 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1042 
some limitations. Blast_tac... 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1043 
+ ignores addss, addbefore, addafter; this restriction is intrinsic 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1044 
+ ignores elimination rules that don't have the correct format 
5726  1045 
(the conclusion MUST be a formula variable) 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1046 
+ ignores types, which can make HOL proofs fail 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1047 
+ rules must not require higherorder unification, e.g. apply_type in ZF 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1048 
[message "Function Var's argument not a bound variable" relates to this] 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1049 
+ its proof strategy is more general but can actually be slower 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1050 

3107  1051 
* substitution with equality assumptions no longer permutes other 
1052 
assumptions; 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1053 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1054 
* minor changes in semantics of addafter (now called addaltern); renamed 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1055 
setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper 
3107  1056 
(and access functions for it); 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1057 

5726  1058 
* improved combination of classical reasoner and simplifier: 
3317  1059 
+ functions for handling clasimpsets 
1060 
+ improvement of addss: now the simplifier is called _after_ the 

1061 
safe steps. 

1062 
+ safe variant of addss called addSss: uses safe simplifications 

5726  1063 
_during_ the safe steps. It is more complete as it allows multiple 
3317  1064 
instantiations of unknowns (e.g. with slow_tac). 
3006  1065 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1066 
*** Simplifier *** 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1067 

3006  1068 
* added interface for simplification procedures (functions that 
1069 
produce *proven* rewrite rules on the fly, depending on current 

1070 
redex); 

1071 

1072 
* ordering on terms as parameter (used for ordered rewriting); 

1073 

3107  1074 
* new functions delcongs, deleqcongs, and Delcongs. richer rep_ss; 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1075 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1076 
* the solver is now split into a safe and an unsafe part. 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1077 
This should be invisible for the normal user, except that the 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1078 
functions setsolver and addsolver have been renamed to setSolver and 
3107  1079 
addSolver; added safe_asm_full_simp_tac; 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1080 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1081 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1082 
*** HOL *** 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1083 

3042  1084 
* a generic induction tactic `induct_tac' which works for all datatypes and 
3107  1085 
also for type `nat'; 
3042  1086 

3316  1087 
* a generic case distinction tactic `exhaust_tac' which works for all 
1088 
datatypes and also for type `nat'; 

1089 

1090 
* each datatype comes with a function `size'; 

1091 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1092 
* patterns in case expressions allow tuple patterns as arguments to 
3107  1093 
constructors, for example `case x of [] => ...  (x,y,z)#ps => ...'; 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1094 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1095 
* primrec now also works with type nat; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1096 

3338  1097 
* recdef: a new declaration form, allows general recursive functions to be 
1098 
defined in theory files. See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify. 

1099 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1100 
* the constant for negation has been renamed from "not" to "Not" to 
3107  1101 
harmonize with FOL, ZF, LK, etc.; 
3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1102 

3107  1103 
* HOL/ex/LFilter theory of a corecursive "filter" functional for 
1104 
infinite lists; 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1105 

3227  1106 
* HOL/Modelcheck demonstrates invocation of model checker oracle; 
1107 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1108 
* HOL/ex/Ring.thy declares cring_simp, which solves equational 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1109 
problems in commutative rings, using axiomatic type classes for + and *; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1110 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1111 
* more examples in HOL/MiniML and HOL/Auth; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1112 

223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1113 
* more default rewrite rules for quantifiers, union/intersection; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1114 

3321  1115 
* a new constant `arbitrary == @x.False'; 
1116 

3107  1117 
* HOLCF/IOA replaces old HOL/IOA; 
1118 

5726  1119 
* HOLCF changes: derived all rules and arities 
1120 
+ axiomatic type classes instead of classes 

2653
f1a6997cdc06
described changes for HOLCFVersion without rules and arities
slotosch
parents:
2649
diff
changeset

1121 
+ typedef instead of faking type definitions 
2747  1122 
+ eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. 
2730  1123 
+ new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po 
2653
f1a6997cdc06
described changes for HOLCFVersion without rules and arities
slotosch
parents:
2649
diff
changeset

1124 
+ eliminated the types void, one, tr 
f1a6997cdc06
described changes for HOLCFVersion without rules and arities
slotosch
parents:
2649
diff
changeset

1125 
+ use unit lift and bool lift (with translations) instead of one and tr 
f1a6997cdc06
described changes for HOLCFVersion without rules and arities
slotosch
parents:
2649
diff
changeset

1126 
+ eliminated blift from Lift3.thy (use Def instead of blift) 
3107  1127 
all eliminated rules are derived as theorems > no visible changes ; 
2649  1128 

3006  1129 

3002
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

1130 
*** ZF *** 
2553  1131 

2865  1132 
* ZF now has Fast_tac, Simp_tac and Auto_tac. Union_iff is a now a default 
1133 
rewrite rule; this may affect some proofs. eq_cs is gone but can be put back 

1134 
as ZF_cs addSIs [equalityI]; 

2553  1135 

2554  1136 

2732  1137 

2553  1138 
New in Isabelle947 (November 96) 
1139 
 

1140 

1141 
* allowing negative levels (as offsets) in prlev and choplev; 

1142 

2554  1143 
* superlinear speedup for large simplifications; 
1144 

1145 
* FOL, ZF and HOL now use miniscoping: rewriting pushes 

1146 
quantifications in as far as possible (COULD MAKE EXISTING PROOFS 

1147 
FAIL); can suppress it using the command Delsimps (ex_simps @ 

1148 
all_simps); De Morgan laws are also now included, by default; 

1149 

1150 
* improved printing of ==> : ~: 

1151 

1152 
* new objectlogic "Sequents" adds linear logic, while replacing LK 

1153 
and Modal (thanks to Sara Kalvala); 

1154 

1155 
* HOL/Auth: correctness proofs for authentication protocols; 

1156 

1157 
* HOL: new auto_tac combines rewriting and classical reasoning (many 

1158 
examples on HOL/Auth); 

1159 

1160 
* HOL: new command AddIffs for declaring theorems of the form P=Q to 

1161 
the rewriter and classical reasoner simultaneously; 

1162 

1163 
* function uresult no longer returns theorems in "standard" format; 

1164 
regain previous version by: val uresult = standard o uresult; 

1165 

1166 

1167 

1168 
New in Isabelle946 

1169 
 

1170 

1171 
* oracles  these establish an interface between Isabelle and trusted 

1172 
external reasoners, which may deliver results as theorems; 

1173 

1174 
* proof objects (in particular record all uses of oracles); 

1175 

1176 
* Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset; 

1177 

1178 
* "constdefs" section in theory files; 

1179 

1180 
* "primrec" section (HOL) no longer requires names; 

1181 

1182 
* internal type "tactic" now simply "thm > thm Sequence.seq"; 

1183 

1184 

1185 

1186 
New in Isabelle945 

1187 
 

1188 

1189 
* reduced space requirements; 

1190 

1191 
* automatic HTML generation from theories; 

1192 

1193 
* theory files no longer require "..." (quotes) around most types; 

1194 

1195 
* new examples, including two proofs of the ChurchRosser theorem; 

1196 

1197 
* noncurried (1994) version of HOL is no longer distributed; 

1198 

2553  1199 

2557  1200 

1201 
New in Isabelle944 

1202 
 

1203 

2747  1204 
* greatly reduced space requirements; 
2557  1205 

1206 
* theory files (.thy) no longer require \...\ escapes at line breaks; 

1207 

5726  1208 
* searchable theorem database (see the section "Retrieving theorems" on 
2557  1209 
page 8 of the Reference Manual); 
1210 

1211 
* new examples, including Grabczewski's monumental case study of the 

1212 
Axiom of Choice; 

1213 

1214 
* The previous version of HOL renamed to Old_HOL; 

1215 

5726  1216 
* The new version of HOL (previously called CHOL) uses a curried syntax 
2557  1217 
for functions. Application looks like f a b instead of f(a,b); 
1218 

1219 
* Mutually recursive inductive definitions finally work in HOL; 

1220 

1221 
* In ZF, patternmatching on tuples is now available in all abstractions and 

1222 
translates to the operator "split"; 

1223 

1224 

1225 

1226 
New in Isabelle943 

1227 
 

1228 

5726  1229 
* new infix operator, addss, allowing the classical reasoner to 
2557  1230 
perform simplification at each step of its search. Example: 
5726  1231 
fast_tac (cs addss ss) 
2557  1232 

5726  1233 
* a new logic, CHOL, the same as HOL, but with a curried syntax 
1234 
for functions. Application looks like f a b instead of f(a,b). Also pairs 

2557  1235 
look like (a,b) instead of <a,b>; 
1236 

1237 
* PLEASE NOTE: CHOL will eventually replace HOL! 

1238 

1239 
* In CHOL, patternmatching on tuples is now available in all abstractions. 

1240 
It translates to the operator "split". A new theory of integers is available; 

1241 

1242 
* In ZF, integer numerals now denote two'scomplement binary integers. 

1243 
Arithmetic operations can be performed by rewriting. See ZF/ex/Bin.ML; 

1244 

5726  1245 
* Many new examples: I/O automata, ChurchRosser theorem, equivalents 
2557  1246 
of the Axiom of Choice; 
1247 

1248 

1249 

1250 
New in Isabelle942 

1251 
 

1252 

5726  1253 
* Significantly faster resolution; 
2557  1254 

1255 
* the different sections in a .thy file can now be mixed and repeated 

1256 
freely; 

1257 

1258 
* Database of theorems for FOL, HOL and ZF. New 

1259 
commands including qed, qed_goal and bind_thm store theorems in the database. 

1260 

1261 
* Simple database queries: return a named theorem (get_thm) or all theorems of 

1262 
a given theory (thms_of), or find out what theory a theorem was proved in 

1263 
(theory_of_thm); 

1264 

1265 
* Bugs fixed in the inductive definition and datatype packages; 

1266 

1267 
* The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs 

1268 
and HOL_dup_cs obsolete; 

1269 

1270 
* Syntactic ambiguities caused by the new treatment of syntax in Isabelle941 

1271 
have been removed; 

1272 

1273 
* Simpler definition of function space in ZF; 

1274 

1275 
* new results about cardinal and ordinal arithmetic in ZF; 

1276 

1277 
* 'subtype' facility in HOL for introducing new types as subsets of existing 

1278 
types; 

1279 

1280 

2553  1281 
$Id$ 