author  wenzelm 
Wed, 10 Mar 1999 16:31:33 +0100  
changeset 6343  97c697a32b73 
parent 6278  37b76155a49e 
child 6386  e9e8af97f48f 
permissions  rwrr 
6269  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 

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

5931  12 

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

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

6057  17 

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

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

6141  21 

6057  22 

6069  23 
*** Proof tools *** 
24 

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

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

28 
instantiated for other types and logics as well. 

6069  29 

30 

6014  31 
*** General *** 
32 

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

5973  35 

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

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

38 

6343  39 
* new print_mode "HTML"; 
40 

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

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

42 

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

45 

6028  46 

6057  47 
*** HOL *** 
48 

6343  49 
* There are now decision procedures for linear arithmetic over nat and 
50 
int: 

6131  51 

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

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

55 
are ignored; quantified subformulae are ignored unless they are 

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

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

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

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

6131  60 

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

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

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

65 
simplifier. 

6131  66 

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

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

6028  70 

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

73 
temporal levels more uniformly; introduces INCOMPATIBILITIES due to 

74 
changed syntax and (many) tactics; 

75 

6269  76 

6064  77 
*** ZF *** 
78 

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

6269  80 
directly (as in HOL) over datatypes and the natural numbers; 
6064  81 

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

6064  84 

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

86 

6141  87 
* simplification automatically does freeness reasoning for datatype 
6269  88 
constructors; 
6141  89 

6269  90 
* automatic typeinference, with AddTCs command to insert new 
91 
typechecking rules; 

6155  92 

6269  93 
* datatype introduction rules are now added as Safe Introduction rules 
94 
to the claset; 

6155  95 

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

98 

6069  99 

6343  100 
*** Internal programming interfaces *** 
101 

102 
* tuned current_goals_markers semantics: begin / end goal avoids 

103 
printing empty lines; 

104 

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

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

107 
uncoditionally; replaced prs_fn by writeln_fn; consider std_output: 

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

109 

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

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

112 
mode to get Isabelle font glyphs as before; 

113 

114 
* refined token_translation interface; INCOMPATIBILITY: output length 

115 
now of type real instead of int; 

116 

117 

6064  118 

5781  119 
New in Isabelle981 (October 1998) 
120 
 

121 

5127  122 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
4842  123 

5726  124 
* several changes of automated proof tools; 
5373  125 

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

5214  128 

5726  129 
* HOL: renamed r^1 to 'converse' from 'inverse'; 'inj_onto' is now 
5217  130 
called `inj_on'; 
5160  131 

5275  132 
* HOL: removed duplicate thms in Arith: 
133 
less_imp_add_less should be replaced by trans_less_add1 

134 
le_imp_add_le should be replaced by trans_le_add1 

5160  135 

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

5490  138 

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

141 
now taken as an integer constant. 

5541  142 

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

144 

5363  145 

5127  146 
*** Proof tools *** 
4880  147 

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

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

149 
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

150 
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

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

152 
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

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

154 
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

155 
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

156 
2. The simplifier now knows a little bit about natarithmetic. 
4880  157 

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

160 
wrapper functionals. This implies that addbefore, addSbefore, 

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

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

163 
one (emitting a warning). 

4824  164 
type wrapper = (int > tactic) > (int > tactic) 
4649  165 
setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by 
4824  166 
addWrapper, addSWrapper: claset * (string * wrapper) > claset 
167 
delWrapper, delSWrapper: claset * string > claset 

4649  168 
getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; 
169 

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

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

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

174 
by Force_tac; 

5524  175 

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

5524  178 

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

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

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

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

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

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

187 
split_all_tac for record fields. 

5127  188 

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

191 
Addsimps. They can be removed via Delsplits just like 

192 
Delsimps. Lowercase versions are also available. 

5127  193 

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

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

197 
either remove split_if completely from the default simpset by 

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

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

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

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

202 
t is the name of the datatype). 

5127  203 

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

5726  207 
aimed to solve the given subgoal completely. 
5127  208 

209 

210 
*** General *** 

211 

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

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

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

4842  218 

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

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

224 

5127  225 
* new theory section 'nonterminals' for purely syntactic types; 
4858  226 

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

4869  229 

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

232 

5363  233 
* isatool install  install binaries with absolute references to 
234 
ISABELLE_HOME/bin; 

235 

5572  236 
* isatool logo  create instances of the Isabelle logo (as EPS); 
237 

5407  238 
* print mode 'emacs' reserved for Isamode; 
239 

5726  240 
* support multiple print (ast) translations per constant name; 
241 

4711  242 

4661  243 
*** HOL *** 
244 

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

5217  247 
* HOL/inductive package reorganized and improved: now supports mutual 
5267  248 
definitions such as 
5217  249 

250 
inductive EVEN ODD 

251 
intrs 

252 
null "0 : EVEN" 

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

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

255 

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

257 
recursive sets; inductive definitions now handle disjunctive premises 

258 
correctly (also ZF); 

5214  259 

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

262 
contained in "induct"; 

263 

264 

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

5267  266 
supports mutually recursive datatypes such as 
5217  267 

268 
datatype 

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

270 
 SUM ('a aexp) ('a aexp) 

271 
 DIFF ('a aexp) ('a aexp) 

272 
 NUM 'a 

273 
and 

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

275 
 AND ('a bexp) ('a bexp) 

276 
 OR ('a bexp) ('a bexp) 

277 

5267  278 
as well as indirectly recursive datatypes such as 
5214  279 

5217  280 
datatype 
281 
('a, 'b) term = Var 'a 

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

5214  283 

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

286 

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

288 
<function_name>.simps. 

289 

290 
INCOMPATIBILITIES: 

5214  291 

5217  292 
 Theories using datatypes must now have theory Datatype as an 
293 
ancestor. 

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

295 
generic induct_tac instead. 

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

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

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

303 
some datatype definitions may have to be annotated with explicit 

304 
sort constraints. 

305 
 Primrec definitions no longer require function name and type 

306 
of recursive argument. 

5214  307 

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

310 

311 

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

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

315 
support is as follows: 

316 

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

318 
constructor terms) are part of the standard simpset; 

319 

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

321 
made part of standard simpset and claset via addIffs; 

322 

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

324 
the standard claset (addSWrapper); 

325 

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

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

328 
the name of your record type. 

329 

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

331 

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

333 

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

335 
blow up into some record constructor term, consequently the 

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

337 
solve record problems automatically. 

338 

5214  339 

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

342 

5650  343 
* automatic simplification of integer sums and comparisons, using cancellation; 
344 

5526  345 
* added option_map_eq_Some and not_Some_eq to the default simpset and claset; 
5127  346 

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

348 

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

350 

351 
* expand_if, expand_split, expand_sum_case and expand_nat_case are now 

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

353 
with add/delsplits); 

5125  354 

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

357 
MAKE EXISTING PROOFS FAIL under rare circumstances (consider 

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

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

361 
%u.f(); 

5125  362 

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

5109  365 

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

368 
disjointness reasoning but breaking a few old proofs. 

5267  369 

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

372 
literature); 

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

373 

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

4838  376 

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

379 
release ONLY. 

380 

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

383 
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

384 

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

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

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

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

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

5282  393 
 new lexicographic orderings and corresponding wellfoundedness theorems. 
4779  394 

5127  395 
* HOL/Arith: 
396 
 removed 'pred' (predecessor) function; 

397 
 generalized some theorems about n1; 

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

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

4766  400 

5127  401 
* HOL/Relation: renamed the relational operator r^1 "converse" 
4842  402 
instead of "inverse"; 
4711  403 

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

406 

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

5127  410 
* directory HOL/UNITY: Chandy and Misra's UNITY formalism; 
4711  411 

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

414 

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

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

418 

5363  419 

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

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

421 

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

5160  424 

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

427 
disjointness reasoning but breaking a few old proofs. 

5267  428 

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

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

432 

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

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

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

5308  437 
Now rew can involve either definitions or equalities (either == or =). 
5142  438 

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

441 

4842  442 

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

444 

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

5207  447 

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

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

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

452 

5251  453 
* removed global_names compatibility flag  all theory declarations 
454 
are qualified by default; 

455 

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

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

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

459 

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

462 

5207  463 
* new tactical CHANGED_GOAL for checking that a tactic modifies a 
464 
subgoal; 

5142  465 

5251  466 
* Display.print_goals function moved to Locale.print_goals; 
467 

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

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

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

472 
for example; 

473 

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

474 

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

475 

4410  476 
New in Isabelle98 (January 1998) 
477 
 

478 

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

480 

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

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

483 

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

485 
simpset / simpset_ref; 

486 

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

488 
implicit merge of thms' signatures; 

489 

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

491 

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

493 

3454  494 

3715  495 
*** General Changes *** 
496 

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

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

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

504 
backward campatibility problems try setting 'global_names' at compile 

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

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

507 
section; 

4108  508 

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

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

511 
replaced by functions simpset:unit>simpset and 

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

513 
to patch your ML files accordingly; 

3856  514 

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

3901  517 
usedir (see i option, ISABELLE_USEDIR_OPTIONS); 
3857  518 

3856  519 
* defs may now be conditional; improved rewrite_goals_tac to handle 
520 
conditional equations; 

521 

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

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

4112  526 
restricted to 'trivial' ones; COMPATIBILITY: one may have to use 
3901  527 
transfer:theory>thm>thm in (rare) cases; 
528 

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

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

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

531 

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

534 

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

536 
show_types); 

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

537 

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

539 

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

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

541 

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

543 

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

545 

3715  546 
* removed obsolete init_pps and init_database; 
547 

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

549 
fun STATE tacfun st = tacfun st st; 

550 

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

4269  553 

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

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

556 
qualified references to the Sequence structure only!); 

557 

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

4269  560 

3715  561 

562 
*** Classical Reasoner *** 

563 

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

566 
splitting it into several subgoals; 

3715  567 

3719  568 
* Safe_tac: like safe_tac but uses the default claset; 
569 

3715  570 

571 
*** Simplifier *** 

572 

573 
* added simplification meta rules: 

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

575 

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

577 
logics (again); 

578 

579 
* added prems argument to simplification procedures; 

580 

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

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

584 

3715  585 

586 
*** Syntax *** 

587 

4174  588 
* TYPE('a) syntax for type reflection terms; 
589 

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

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

3846  593 

3715  594 
* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; 
595 

596 

597 
*** HOL *** 

598 

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

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

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

4035  605 
protocol TLS; 
3985  606 

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

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

611 
differences; simplification procedures nat_cancel_factor for 

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

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

4335  615 

3580  616 
* HOL/simplifier: terms of the form 
4325  617 
`? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) 
3580  618 
are rewritten to 
4035  619 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', 
620 
and those of the form 

4325  621 
`! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) > R(x)' (or t=x) 
4035  622 
are rewritten to 
623 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) > R(t)', 

624 

625 
* HOL/datatype 

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

3580  627 

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

630 
... 

4189  631 
(!y1 ... ymn. x = Cn y1 ... ymn > P(f1 y1 ... ymn)) 
4035  632 
) 
633 

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

634 
and a theorem `split_t_case_asm' of the form 
4189  635 

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

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

638 
... 

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

640 
) 

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

641 
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

642 
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

643 
split_list_case and split_option_case. 
4189  644 

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

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

648 
because it will disappear altogether at some point. 

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

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

651 
`standard'. 

4357  652 

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

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

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

3570  657 

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

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

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

662 

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

665 
still lacks various theorems and concrete record syntax; 

666 

4125  667 

3715  668 
*** HOLCF *** 
3535  669 

4125  670 
* removed "axioms" and "generated by" sections; 
671 

4123  672 
* replaced "ops" section by extended "consts" section, which is capable of 
4125  673 
handling the continuous function space ">" directly; 
674 

675 
* domain package: 

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

677 
. creates hierachical name space, 

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

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

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

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

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

683 
appear on the lefthand side of the equations only; 

4123  684 

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

3567  686 

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

3579  689 

690 

3719  691 
*** FOL and ZF *** 
692 

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

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

698 

3719  699 

3579  700 

3006  701 
New in Isabelle948 (May 1997) 
702 
 

2654  703 

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

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

705 

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

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

707 
still somewhat experimental); old Makefiles etc. still functional; 
2971  708 

3205  709 
* new 'Isabelle System Manual'; 
710 

2825  711 
* INSTALL text, together with ./configure and ./build scripts; 
2773  712 

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

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

715 

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

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

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

718 

3006  719 

720 
*** Syntax *** 

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

721 

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

724 

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

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

726 
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

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

728 

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

733 
(Syntax.mark_boundT); 

2705  734 

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

2730  738 

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

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

740 

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

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

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

743 

3006  744 

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

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

746 

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

747 
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

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

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

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

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

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

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

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

756 

3107  757 
* substitution with equality assumptions no longer permutes other 
758 
assumptions; 

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

759 

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

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

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

763 

5726  764 
* improved combination of classical reasoner and simplifier: 
3317  765 
+ functions for handling clasimpsets 
766 
+ improvement of addss: now the simplifier is called _after_ the 

767 
safe steps. 

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

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

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

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

773 

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

776 
redex); 

777 

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

779 

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

781 

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

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

783 
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

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

786 

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

787 

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

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

789 

3042  790 
* a generic induction tactic `induct_tac' which works for all datatypes and 
3107  791 
also for type `nat'; 
3042  792 

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

795 

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

797 

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

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

800 

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

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

802 

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

805 

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

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

808 

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

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

811 

3227  812 
* HOL/Modelcheck demonstrates invocation of model checker oracle; 
813 

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

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

815 
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

816 

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

817 
* more examples in HOL/MiniML and HOL/Auth; 
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 
* more default rewrite rules for quantifiers, union/intersection; 
223e5d65faaa
Reorganized under headings. Also documented Blast_tac and LFilter
paulson
parents:
2993
diff
changeset

820 

3321  821 
* a new constant `arbitrary == @x.False'; 
822 

3107  823 
* HOLCF/IOA replaces old HOL/IOA; 
824 

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

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

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

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

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

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

3006  835 

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

836 
*** ZF *** 
2553  837 

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

840 
as ZF_cs addSIs [equalityI]; 

2553  841 

2554  842 

2732  843 

2553  844 
New in Isabelle947 (November 96) 
845 
 

846 

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

848 

2554  849 
* superlinear speedup for large simplifications; 
850 

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

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

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

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

855 

856 
* improved printing of ==> : ~: 

857 

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

859 
and Modal (thanks to Sara Kalvala); 

860 

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

862 

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

864 
examples on HOL/Auth); 

865 

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

867 
the rewriter and classical reasoner simultaneously; 

868 

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

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

871 

872 

873 

874 
New in Isabelle946 

875 
 

876 

877 
* oracles  these establish an interface between Isabelle and trusted 

878 
external reasoners, which may deliver results as theorems; 

879 

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

881 

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

883 

884 
* "constdefs" section in theory files; 

885 

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

887 

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

889 

890 

891 

892 
New in Isabelle945 

893 
 

894 

895 
* reduced space requirements; 

896 

897 
* automatic HTML generation from theories; 

898 

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

900 

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

902 

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

904 

2553  905 

2557  906 

907 
New in Isabelle944 

908 
 

909 

2747  910 
* greatly reduced space requirements; 
2557  911 

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

913 

5726  914 
* searchable theorem database (see the section "Retrieving theorems" on 
2557  915 
page 8 of the Reference Manual); 
916 

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

918 
Axiom of Choice; 

919 

920 
* The previous version of HOL renamed to Old_HOL; 

921 

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

925 
* Mutually recursive inductive definitions finally work in HOL; 

926 

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

928 
translates to the operator "split"; 

929 

930 

931 

932 
New in Isabelle943 

933 
 

934 

5726  935 
* new infix operator, addss, allowing the classical reasoner to 
2557  936 
perform simplification at each step of its search. Example: 
5726  937 
fast_tac (cs addss ss) 
2557  938 

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

2557  941 
look like (a,b) instead of <a,b>; 
942 

943 
* PLEASE NOTE: CHOL will eventually replace HOL! 

944 

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

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

947 

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

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

950 

5726  951 
* Many new examples: I/O automata, ChurchRosser theorem, equivalents 
2557  952 
of the Axiom of Choice; 
953 

954 

955 

956 
New in Isabelle942 

957 
 

958 

5726  959 
* Significantly faster resolution; 
2557  960 

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

962 
freely; 

963 

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

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

966 

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

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

969 
(theory_of_thm); 

970 

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

972 

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

974 
and HOL_dup_cs obsolete; 

975 

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

977 
have been removed; 

978 

979 
* Simpler definition of function space in ZF; 

980 

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

982 

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

984 
types; 

985 

986 

2553  987 
$Id$ 