author  wenzelm 
Wed, 28 Jul 1999 19:14:33 +0200  
changeset 7125  df7cf6e85501 
parent 7113  ab79d9fa8d8e 
child 7157  d49318f6c11a 
permissions  rwrr 
6420  1 

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

2553  4 

4981  5 
New in this Isabelle version 
6 
 

4649  7 

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

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

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

13 
Delcongs [if_weak_cong]; 

14 

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

5931  17 

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

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

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

21 
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

22 

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

6057  25 

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

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

6141  29 

6057  30 

6069  31 
*** Proof tools *** 
32 

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

35 
types `nat' and `int' in HOL (see below) but can, should and will be 

36 
instantiated for other types and logics as well. 

6069  37 

38 

6014  39 
*** General *** 
40 

6751  41 
* Isabelle manuals now also available as PDF; 
42 

6671  43 
* improved browser info generation: better HTML markup (including 
44 
colors), graph views in several sizes; isatool usedir now provides a 

45 
proper interface for user theories (via P option); 

46 

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

6671  49 
add_path, del_path, reset_path functions; new operations such as 
50 
update_thy, touch_thy, remove_thy (see also isatool doc ref); 

6449  51 

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

5973  54 

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

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

57 

6343  58 
* new print_mode "HTML"; 
59 

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

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

61 

6343  62 
* new flag show_tags controls display of tags of theorems (which are 
63 
basically just comments that may be attached by some tools); 

64 

6420  65 
* improved isatool install: option k creates KDE application icon, 
66 
option p DIR installs standalone binaries; 

6415  67 

6413  68 
* added ML_PLATFORM setting (useful for crossplatform installations); 
6671  69 
more robust handling of platform specific ML images for SML/NJ; 
6413  70 

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

73 

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

75 
244c244 

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

77 
 

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

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

82 
 

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

84 

6028  85 

6057  86 
*** HOL *** 
87 

6343  88 
* There are now decision procedures for linear arithmetic over nat and 
89 
int: 

6131  90 

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

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

94 
are ignored; quantified subformulae are ignored unless they are 

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

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

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

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

6131  99 

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

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

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

104 
simplifier. 

6131  105 

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

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

6028  109 

6922  110 
* Integer division and remainder can now be performed on constant arguments. 
111 

112 
* Many properties of integer multiplication, division and remainder are now 

113 
available. 

114 

7125  115 
* IsaMakefile: the HOLReal target now builds an actual image; 
116 

6403  117 
* New bounded quantifier syntax (input only): 
118 
! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P 

119 

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

122 
temporal levels more uniformly; introduces INCOMPATIBILITIES due to 

123 
changed syntax and (many) tactics; 

124 

7047
d103b875ef1d
Datatype package now handles arbitrarily branching datatypes.
berghofe
parents:
6925
diff
changeset

125 
* HOL/datatype: Now also handles arbitrarily branching datatypes 
d103b875ef1d
Datatype package now handles arbitrarily branching datatypes.
berghofe
parents:
6925
diff
changeset

126 
(using function types) such as 
d103b875ef1d
Datatype package now handles arbitrarily branching datatypes.
berghofe
parents:
6925
diff
changeset

127 

d103b875ef1d
Datatype package now handles arbitrarily branching datatypes.
berghofe
parents:
6925
diff
changeset

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

129 

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

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

131 
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

132 

6671  133 
* HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects 
134 
comma separated list of theorem names rather than an ML expression; 

6563  135 

6795  136 
* reset HOL_quantifiers by default, i.e. quantifiers are printed as 
137 
ALL/EX rather than !/?; 

138 

6269  139 

7113  140 
*** LK *** 
141 

142 
* the notation <<...>> is now available as a notation for sequences of formulas 

143 

144 
* the simplifier is now installed 

145 

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

147 

148 
* the classical reasoner now has a default rule database 

149 

150 

6064  151 
*** ZF *** 
152 

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

6269  154 
directly (as in HOL) over datatypes and the natural numbers; 
6064  155 

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

6064  158 

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

160 

6141  161 
* simplification automatically does freeness reasoning for datatype 
6269  162 
constructors; 
6141  163 

6269  164 
* automatic typeinference, with AddTCs command to insert new 
165 
typechecking rules; 

6155  166 

6269  167 
* datatype introduction rules are now added as Safe Introduction rules 
168 
to the claset; 

6155  169 

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

172 

6069  173 

6343  174 
*** Internal programming interfaces *** 
175 

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

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

177 

6343  178 
* tuned current_goals_markers semantics: begin / end goal avoids 
179 
printing empty lines; 

180 

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

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

183 
uncoditionally; replaced prs_fn by writeln_fn; consider std_output: 

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

185 

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

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

188 
mode to get Isabelle font glyphs as before; 

189 

190 
* refined token_translation interface; INCOMPATIBILITY: output length 

191 
now of type real instead of int; 

192 

193 

6064  194 

5781  195 
New in Isabelle981 (October 1998) 
196 
 

197 

5127  198 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
4842  199 

5726  200 
* several changes of automated proof tools; 
5373  201 

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

5214  204 

5726  205 
* HOL: renamed r^1 to 'converse' from 'inverse'; 'inj_onto' is now 
5217  206 
called `inj_on'; 
5160  207 

5275  208 
* HOL: removed duplicate thms in Arith: 
209 
less_imp_add_less should be replaced by trans_less_add1 

210 
le_imp_add_le should be replaced by trans_le_add1 

5160  211 

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

5490  214 

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

217 
now taken as an integer constant. 

5541  218 

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

220 

5363  221 

5127  222 
*** Proof tools *** 
4880  223 

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

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

225 
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

226 
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

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

228 
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

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

230 
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

231 
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

232 
2. The simplifier now knows a little bit about natarithmetic. 
4880  233 

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

236 
wrapper functionals. This implies that addbefore, addSbefore, 

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

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

239 
one (emitting a warning). 

4824  240 
type wrapper = (int > tactic) > (int > tactic) 
4649  241 
setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by 
4824  242 
addWrapper, addSWrapper: claset * (string * wrapper) > claset 
243 
delWrapper, delSWrapper: claset * string > claset 

4649  244 
getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; 
245 

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

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

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

250 
by Force_tac; 

5524  251 

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

5524  254 

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

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

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

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

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

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

263 
split_all_tac for record fields. 

5127  264 

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

267 
Addsimps. They can be removed via Delsplits just like 

268 
Delsimps. Lowercase versions are also available. 

5127  269 

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

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

273 
either remove split_if completely from the default simpset by 

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

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

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

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

278 
t is the name of the datatype). 

5127  279 

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

5726  283 
aimed to solve the given subgoal completely. 
5127  284 

285 

286 
*** General *** 

287 

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

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

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

4842  294 

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

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

300 

5127  301 
* new theory section 'nonterminals' for purely syntactic types; 
4858  302 

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

4869  305 

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

308 

5363  309 
* isatool install  install binaries with absolute references to 
310 
ISABELLE_HOME/bin; 

311 

5572  312 
* isatool logo  create instances of the Isabelle logo (as EPS); 
313 

5407  314 
* print mode 'emacs' reserved for Isamode; 
315 

5726  316 
* support multiple print (ast) translations per constant name; 
317 

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

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

319 

4711  320 

4661  321 
*** HOL *** 
322 

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

5217  325 
* HOL/inductive package reorganized and improved: now supports mutual 
5267  326 
definitions such as 
5217  327 

328 
inductive EVEN ODD 

329 
intrs 

330 
null "0 : EVEN" 

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

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

333 

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

335 
recursive sets; inductive definitions now handle disjunctive premises 

336 
correctly (also ZF); 

5214  337 

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

340 
contained in "induct"; 

341 

342 

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

5267  344 
supports mutually recursive datatypes such as 
5217  345 

346 
datatype 

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

348 
 SUM ('a aexp) ('a aexp) 

349 
 DIFF ('a aexp) ('a aexp) 

350 
 NUM 'a 

351 
and 

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

353 
 AND ('a bexp) ('a bexp) 

354 
 OR ('a bexp) ('a bexp) 

355 

5267  356 
as well as indirectly recursive datatypes such as 
5214  357 

5217  358 
datatype 
359 
('a, 'b) term = Var 'a 

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

5214  361 

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

364 

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

366 
<function_name>.simps. 

367 

368 
INCOMPATIBILITIES: 

5214  369 

5217  370 
 Theories using datatypes must now have theory Datatype as an 
371 
ancestor. 

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

373 
generic induct_tac instead. 

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

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

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

381 
some datatype definitions may have to be annotated with explicit 

382 
sort constraints. 

383 
 Primrec definitions no longer require function name and type 

384 
of recursive argument. 

5214  385 

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

388 

389 

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

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

393 
support is as follows: 

394 

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

396 
constructor terms) are part of the standard simpset; 

397 

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

399 
made part of standard simpset and claset via addIffs; 

400 

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

402 
the standard claset (addSWrapper); 

403 

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

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

406 
the name of your record type. 

407 

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

409 

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

411 

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

413 
blow up into some record constructor term, consequently the 

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

415 
solve record problems automatically. 

416 

5214  417 

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

420 

5650  421 
* automatic simplification of integer sums and comparisons, using cancellation; 
422 

5526  423 
* added option_map_eq_Some and not_Some_eq to the default simpset and claset; 
5127  424 

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

426 

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

428 

429 
* expand_if, expand_split, expand_sum_case and expand_nat_case are now 

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

431 
with add/delsplits); 

5125  432 

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

435 
MAKE EXISTING PROOFS FAIL under rare circumstances (consider 

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

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

439 
%u.f(); 

5125  440 

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

5109  443 

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

446 
disjointness reasoning but breaking a few old proofs. 

5267  447 

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

450 
literature); 

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

451 

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

4838  454 

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

457 
release ONLY. 

458 

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

461 
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

462 

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

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

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

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

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

5282  471 
 new lexicographic orderings and corresponding wellfoundedness theorems. 
4779  472 

5127  473 
* HOL/Arith: 
474 
 removed 'pred' (predecessor) function; 

475 
 generalized some theorems about n1; 

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

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

4766  478 

5127  479 
* HOL/Relation: renamed the relational operator r^1 "converse" 
4842  480 
instead of "inverse"; 
4711  481 

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

484 

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

5127  488 
* directory HOL/UNITY: Chandy and Misra's UNITY formalism; 
4711  489 

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

492 

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

5308  495 
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

496 

5363  497 

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

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

499 

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

5160  502 

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

505 
disjointness reasoning but breaking a few old proofs. 

5267  506 

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

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

510 

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

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

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

5308  515 
Now rew can involve either definitions or equalities (either == or =). 
5142  516 

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

519 

4842  520 

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

522 

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

5207  525 

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

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

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

530 

5251  531 
* removed global_names compatibility flag  all theory declarations 
532 
are qualified by default; 

533 

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

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

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

537 

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

540 

5207  541 
* new tactical CHANGED_GOAL for checking that a tactic modifies a 
542 
subgoal; 

5142  543 

5251  544 
* Display.print_goals function moved to Locale.print_goals; 
545 

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

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

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

550 
for example; 

551 

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

552 

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

553 

4410  554 
New in Isabelle98 (January 1998) 
555 
 

556 

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

558 

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

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

561 

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

563 
simpset / simpset_ref; 

564 

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

566 
implicit merge of thms' signatures; 

567 

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

569 

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

571 

3454  572 

3715  573 
*** General Changes *** 
574 

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

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

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

582 
backward campatibility problems try setting 'global_names' at compile 

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

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

585 
section; 

4108  586 

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

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

589 
replaced by functions simpset:unit>simpset and 

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

591 
to patch your ML files accordingly; 

3856  592 

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

3901  595 
usedir (see i option, ISABELLE_USEDIR_OPTIONS); 
3857  596 

3856  597 
* defs may now be conditional; improved rewrite_goals_tac to handle 
598 
conditional equations; 

599 

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

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

4112  604 
restricted to 'trivial' ones; COMPATIBILITY: one may have to use 
3901  605 
transfer:theory>thm>thm in (rare) cases; 
606 

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

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

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

609 

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

612 

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

614 
show_types); 

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

615 

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

617 

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

618 
* 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

619 

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

621 

3856  622 
* 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

623 

3715  624 
* removed obsolete init_pps and init_database; 
625 

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

627 
fun STATE tacfun st = tacfun st st; 

628 

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

4269  631 

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

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

634 
qualified references to the Sequence structure only!); 

635 

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

4269  638 

3715  639 

640 
*** Classical Reasoner *** 

641 

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

644 
splitting it into several subgoals; 

3715  645 

3719  646 
* Safe_tac: like safe_tac but uses the default claset; 
647 

3715  648 

649 
*** Simplifier *** 

650 

651 
* added simplification meta rules: 

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

653 

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

655 
logics (again); 

656 

657 
* added prems argument to simplification procedures; 

658 

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

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

662 

3715  663 

664 
*** Syntax *** 

665 

4174  666 
* TYPE('a) syntax for type reflection terms; 
667 

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

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

3846  671 

3715  672 
* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; 
673 

674 

675 
*** HOL *** 

676 

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

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

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

4035  683 
protocol TLS; 
3985  684 

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

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

689 
differences; simplification procedures nat_cancel_factor for 

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

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

4335  693 

3580  694 
* HOL/simplifier: terms of the form 
4325  695 
`? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) 
3580  696 
are rewritten to 
4035  697 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', 
698 
and those of the form 

4325  699 
`! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) > R(x)' (or t=x) 
4035  700 
are rewritten to 
701 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) > R(t)', 

702 

703 
* HOL/datatype 

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

3580  705 

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

708 
... 

4189  709 
(!y1 ... ymn. x = Cn y1 ... ymn > P(f1 y1 ... ymn)) 
4035  710 
) 
711 

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

712 
and a theorem `split_t_case_asm' of the form 
4189  713 

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

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

716 
... 

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

718 
) 

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

719 
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

720 
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

721 
split_list_case and split_option_case. 
4189  722 

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

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

726 
because it will disappear altogether at some point. 

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

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

729 
`standard'. 

4357  730 

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

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

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

3570  735 

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

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

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

740 

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

743 
still lacks various theorems and concrete record syntax; 

744 

4125  745 

3715  746 
*** HOLCF *** 
3535  747 

4125  748 
* removed "axioms" and "generated by" sections; 
749 

4123  750 
* replaced "ops" section by extended "consts" section, which is capable of 
4125  751 
handling the continuous function space ">" directly; 
752 

753 
* domain package: 

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

755 
. creates hierachical name space, 

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

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

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

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

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

761 
appear on the lefthand side of the equations only; 

4123  762 

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

3567  764 

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

3579  767 

768 

3719  769 
*** FOL and ZF *** 
770 

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

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

776 

3719  777 

3579  778 

3006  779 
New in Isabelle948 (May 1997) 
780 
 

2654  781 

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

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

783 

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

784 
* 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

785 
still somewhat experimental); old Makefiles etc. still functional; 
2971  786 

3205  787 
* new 'Isabelle System Manual'; 
788 

2825  789 
* INSTALL text, together with ./configure and ./build scripts; 
2773  790 

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

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

793 

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

794 
* 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

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

796 

3006  797 

798 
*** Syntax *** 

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

799 

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

802 

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

803 
* 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

804 
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

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

806 

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

811 
(Syntax.mark_boundT); 

2705  812 

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

2730  816 

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

817 
* 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

818 

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

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

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

821 

3006  822 

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

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

824 

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

825 
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

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

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

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

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

831 
+ 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

832 
[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

833 
+ 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

834 

3107  835 
* substitution with equality assumptions no longer permutes other 
836 
assumptions; 

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

837 

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

838 
* 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

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

841 

5726  842 
* improved combination of classical reasoner and simplifier: 
3317  843 
+ functions for handling clasimpsets 
844 
+ improvement of addss: now the simplifier is called _after_ the 

845 
safe steps. 

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

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

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

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

851 

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

854 
redex); 

855 

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

857 

3107  858 
* 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

859 

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

860 
* 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

861 
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

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

864 

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

865 

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

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

867 

3042  868 
* a generic induction tactic `induct_tac' which works for all datatypes and 
3107  869 
also for type `nat'; 
3042  870 

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

873 

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

875 

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

876 
* patterns in case expressions allow tuple patterns as arguments to 
3107  877 
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

878 

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

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

880 

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

883 

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

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

886 

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

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

889 

3227  890 
* HOL/Modelcheck demonstrates invocation of model checker oracle; 
891 

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

892 
* 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

893 
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

894 

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

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

896 

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

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

898 

3321  899 
* a new constant `arbitrary == @x.False'; 
900 

3107  901 
* HOLCF/IOA replaces old HOL/IOA; 
902 

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

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

905 
+ typedef instead of faking type definitions 
2747  906 
+ eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc. 
2730  907 
+ 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

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

909 
+ 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

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

3006  913 

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

914 
*** ZF *** 
2553  915 

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

918 
as ZF_cs addSIs [equalityI]; 

2553  919 

2554  920 

2732  921 

2553  922 
New in Isabelle947 (November 96) 
923 
 

924 

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

926 

2554  927 
* superlinear speedup for large simplifications; 
928 

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

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

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

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

933 

934 
* improved printing of ==> : ~: 

935 

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

937 
and Modal (thanks to Sara Kalvala); 

938 

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

940 

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

942 
examples on HOL/Auth); 

943 

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

945 
the rewriter and classical reasoner simultaneously; 

946 

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

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

949 

950 

951 

952 
New in Isabelle946 

953 
 

954 

955 
* oracles  these establish an interface between Isabelle and trusted 

956 
external reasoners, which may deliver results as theorems; 

957 

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

959 

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

961 

962 
* "constdefs" section in theory files; 

963 

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

965 

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

967 

968 

969 

970 
New in Isabelle945 

971 
 

972 

973 
* reduced space requirements; 

974 

975 
* automatic HTML generation from theories; 

976 

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

978 

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

980 

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

982 

2553  983 

2557  984 

985 
New in Isabelle944 

986 
 

987 

2747  988 
* greatly reduced space requirements; 
2557  989 

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

991 

5726  992 
* searchable theorem database (see the section "Retrieving theorems" on 
2557  993 
page 8 of the Reference Manual); 
994 

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

996 
Axiom of Choice; 

997 

998 
* The previous version of HOL renamed to Old_HOL; 

999 

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

1003 
* Mutually recursive inductive definitions finally work in HOL; 

1004 

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

1006 
translates to the operator "split"; 

1007 

1008 

1009 

1010 
New in Isabelle943 

1011 
 

1012 

5726  1013 
* new infix operator, addss, allowing the classical reasoner to 
2557  1014 
perform simplification at each step of its search. Example: 
5726  1015 
fast_tac (cs addss ss) 
2557  1016 

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

2557  1019 
look like (a,b) instead of <a,b>; 
1020 

1021 
* PLEASE NOTE: CHOL will eventually replace HOL! 

1022 

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

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

1025 

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

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

1028 

5726  1029 
* Many new examples: I/O automata, ChurchRosser theorem, equivalents 
2557  1030 
of the Axiom of Choice; 
1031 

1032 

1033 

1034 
New in Isabelle942 

1035 
 

1036 

5726  1037 
* Significantly faster resolution; 
2557  1038 

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

1040 
freely; 

1041 

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

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

1044 

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

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

1047 
(theory_of_thm); 

1048 

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

1050 

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

1052 
and HOL_dup_cs obsolete; 

1053 

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

1055 
have been removed; 

1056 

1057 
* Simpler definition of function space in ZF; 

1058 

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

1060 

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

1062 
types; 

1063 

1064 

2553  1065 
$Id$ 