author  paulson 
Wed, 18 Nov 1998 15:10:46 +0100  
changeset 5931  325300576da7 
parent 5781  d37380544c39 
child 5973  040f6d2af50d 
permissions  rwrr 
5726  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 

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

11 

5781  12 
*** General *** 
13 

14 
* tuned current_goals_markers semantics: begin / end goal avoids 

15 
printing empty lines; 

16 

17 

18 
New in Isabelle981 (October 1998) 

19 
 

20 

5127  21 
*** Overview of INCOMPATIBILITIES (see below for more details) *** 
4842  22 

5726  23 
* several changes of automated proof tools; 
5373  24 

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

5214  27 

5726  28 
* HOL: renamed r^1 to 'converse' from 'inverse'; 'inj_onto' is now 
5217  29 
called `inj_on'; 
5160  30 

5275  31 
* HOL: removed duplicate thms in Arith: 
32 
less_imp_add_less should be replaced by trans_less_add1 

33 
le_imp_add_le should be replaced by trans_le_add1 

5160  34 

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

5490  37 

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

40 
now taken as an integer constant. 

5541  41 

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

43 

5363  44 

5127  45 
*** Proof tools *** 
4880  46 

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

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

48 
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

49 
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

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

51 
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

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

53 
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

54 
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

55 
2. The simplifier now knows a little bit about natarithmetic. 
4880  56 

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

59 
wrapper functionals. This implies that addbefore, addSbefore, 

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

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

62 
one (emitting a warning). 

4824  63 
type wrapper = (int > tactic) > (int > tactic) 
4649  64 
setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by 
4824  65 
addWrapper, addSWrapper: claset * (string * wrapper) > claset 
66 
delWrapper, delSWrapper: claset * string > claset 

4649  67 
getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; 
68 

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

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

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

73 
by Force_tac; 

5524  74 

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

5524  77 

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

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

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

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

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

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

86 
split_all_tac for record fields. 

5127  87 

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

90 
Addsimps. They can be removed via Delsplits just like 

91 
Delsimps. Lowercase versions are also available. 

5127  92 

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

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

96 
either remove split_if completely from the default simpset by 

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

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

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

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

101 
t is the name of the datatype). 

5127  102 

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

5726  106 
aimed to solve the given subgoal completely. 
5127  107 

108 

109 
*** General *** 

110 

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

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

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

4842  117 

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

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

123 

5127  124 
* new theory section 'nonterminals' for purely syntactic types; 
4858  125 

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

4869  128 

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

131 

5363  132 
* isatool install  install binaries with absolute references to 
133 
ISABELLE_HOME/bin; 

134 

5572  135 
* isatool logo  create instances of the Isabelle logo (as EPS); 
136 

5407  137 
* print mode 'emacs' reserved for Isamode; 
138 

5726  139 
* support multiple print (ast) translations per constant name; 
140 

4711  141 

4661  142 
*** HOL *** 
143 

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

5217  146 
* HOL/inductive package reorganized and improved: now supports mutual 
5267  147 
definitions such as 
5217  148 

149 
inductive EVEN ODD 

150 
intrs 

151 
null "0 : EVEN" 

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

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

154 

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

156 
recursive sets; inductive definitions now handle disjunctive premises 

157 
correctly (also ZF); 

5214  158 

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

161 
contained in "induct"; 

162 

163 

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

5267  165 
supports mutually recursive datatypes such as 
5217  166 

167 
datatype 

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

169 
 SUM ('a aexp) ('a aexp) 

170 
 DIFF ('a aexp) ('a aexp) 

171 
 NUM 'a 

172 
and 

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

174 
 AND ('a bexp) ('a bexp) 

175 
 OR ('a bexp) ('a bexp) 

176 

5267  177 
as well as indirectly recursive datatypes such as 
5214  178 

5217  179 
datatype 
180 
('a, 'b) term = Var 'a 

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

5214  182 

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

185 

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

187 
<function_name>.simps. 

188 

189 
INCOMPATIBILITIES: 

5214  190 

5217  191 
 Theories using datatypes must now have theory Datatype as an 
192 
ancestor. 

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

194 
generic induct_tac instead. 

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

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

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

202 
some datatype definitions may have to be annotated with explicit 

203 
sort constraints. 

204 
 Primrec definitions no longer require function name and type 

205 
of recursive argument. 

5214  206 

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

209 

210 

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

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

214 
support is as follows: 

215 

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

217 
constructor terms) are part of the standard simpset; 

218 

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

220 
made part of standard simpset and claset via addIffs; 

221 

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

223 
the standard claset (addSWrapper); 

224 

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

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

227 
the name of your record type. 

228 

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

230 

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

232 

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

234 
blow up into some record constructor term, consequently the 

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

236 
solve record problems automatically. 

237 

5214  238 

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

241 

5650  242 
* automatic simplification of integer sums and comparisons, using cancellation; 
243 

5526  244 
* added option_map_eq_Some and not_Some_eq to the default simpset and claset; 
5127  245 

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

247 

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

249 

250 
* expand_if, expand_split, expand_sum_case and expand_nat_case are now 

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

252 
with add/delsplits); 

5125  253 

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

256 
MAKE EXISTING PROOFS FAIL under rare circumstances (consider 

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

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

260 
%u.f(); 

5125  261 

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

5109  264 

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

267 
disjointness reasoning but breaking a few old proofs. 

5267  268 

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

271 
literature); 

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

272 

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

4838  275 

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

278 
release ONLY. 

279 

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

282 
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

283 

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

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

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

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

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

5282  292 
 new lexicographic orderings and corresponding wellfoundedness theorems. 
4779  293 

5127  294 
* HOL/Arith: 
295 
 removed 'pred' (predecessor) function; 

296 
 generalized some theorems about n1; 

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

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

4766  299 

5127  300 
* HOL/Relation: renamed the relational operator r^1 "converse" 
4842  301 
instead of "inverse"; 
4711  302 

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

305 

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

5127  309 
* directory HOL/UNITY: Chandy and Misra's UNITY formalism; 
4711  310 

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

313 

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

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

317 

5363  318 

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

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

320 

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

5160  323 

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

326 
disjointness reasoning but breaking a few old proofs. 

5267  327 

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

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

331 

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

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

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

5308  336 
Now rew can involve either definitions or equalities (either == or =). 
5142  337 

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

340 

4842  341 

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

343 

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

5207  346 

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

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

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

351 

5251  352 
* removed global_names compatibility flag  all theory declarations 
353 
are qualified by default; 

354 

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

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

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

358 

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

361 

5207  362 
* new tactical CHANGED_GOAL for checking that a tactic modifies a 
363 
subgoal; 

5142  364 

5251  365 
* Display.print_goals function moved to Locale.print_goals; 
366 

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

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

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

371 
for example; 

372 

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

373 

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

374 

4410  375 
New in Isabelle98 (January 1998) 
376 
 

377 

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

379 

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

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

382 

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

384 
simpset / simpset_ref; 

385 

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

387 
implicit merge of thms' signatures; 

388 

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

390 

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

392 

3454  393 

3715  394 
*** General Changes *** 
395 

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

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

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

403 
backward campatibility problems try setting 'global_names' at compile 

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

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

406 
section; 

4108  407 

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

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

410 
replaced by functions simpset:unit>simpset and 

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

412 
to patch your ML files accordingly; 

3856  413 

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

3901  416 
usedir (see i option, ISABELLE_USEDIR_OPTIONS); 
3857  417 

3856  418 
* defs may now be conditional; improved rewrite_goals_tac to handle 
419 
conditional equations; 

420 

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

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

4112  425 
restricted to 'trivial' ones; COMPATIBILITY: one may have to use 
3901  426 
transfer:theory>thm>thm in (rare) cases; 
427 

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

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

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

430 

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

433 

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

435 
show_types); 

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

436 

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

438 

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

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

440 

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

442 

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

444 

3715  445 
* removed obsolete init_pps and init_database; 
446 

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

448 
fun STATE tacfun st = tacfun st st; 

449 

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

4269  452 

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

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

455 
qualified references to the Sequence structure only!); 

456 

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

4269  459 

3715  460 

461 
*** Classical Reasoner *** 

462 

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

465 
splitting it into several subgoals; 

3715  466 

3719  467 
* Safe_tac: like safe_tac but uses the default claset; 
468 

3715  469 

470 
*** Simplifier *** 

471 

472 
* added simplification meta rules: 

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

474 

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

476 
logics (again); 

477 

478 
* added prems argument to simplification procedures; 

479 

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

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

483 

3715  484 

485 
*** Syntax *** 

486 

4174  487 
* TYPE('a) syntax for type reflection terms; 
488 

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

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

3846  492 

3715  493 
* Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories; 
494 

495 

496 
*** HOL *** 

497 

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

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

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

4035  504 
protocol TLS; 
3985  505 

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

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

510 
differences; simplification procedures nat_cancel_factor for 

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

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

4335  514 

3580  515 
* HOL/simplifier: terms of the form 
4325  516 
`? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)' (or t=x) 
3580  517 
are rewritten to 
4035  518 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)', 
519 
and those of the form 

4325  520 
`! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) > R(x)' (or t=x) 
4035  521 
are rewritten to 
522 
`P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) > R(t)', 

523 

524 
* HOL/datatype 

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

3580  526 

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

529 
... 

4189  530 
(!y1 ... ymn. x = Cn y1 ... ymn > P(f1 y1 ... ymn)) 
4035  531 
) 
532 

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

533 
and a theorem `split_t_case_asm' of the form 
4189  534 

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

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

537 
... 

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

539 
) 

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

540 
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

541 
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

542 
split_list_case and split_option_case. 
4189  543 

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

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

547 
because it will disappear altogether at some point. 

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

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

550 
`standard'. 

4357  551 

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

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

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

3570  556 

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

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

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

561 

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

564 
still lacks various theorems and concrete record syntax; 

565 

4125  566 

3715  567 
*** HOLCF *** 
3535  568 

4125  569 
* removed "axioms" and "generated by" sections; 
570 

4123  571 
* replaced "ops" section by extended "consts" section, which is capable of 
4125  572 
handling the continuous function space ">" directly; 
573 

574 
* domain package: 

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

576 
. creates hierachical name space, 

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

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

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

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

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

582 
appear on the lefthand side of the equations only; 

4123  583 

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

3567  585 

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

3579  588 

589 

3719  590 
*** FOL and ZF *** 
591 

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

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

597 

3719  598 

3579  599 

3006  600 
New in Isabelle948 (May 1997) 
601 
 

2654  602 

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

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

604 

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

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

606 
still somewhat experimental); old Makefiles etc. still functional; 
2971  607 

3205  608 
* new 'Isabelle System Manual'; 
609 

2825  610 
* INSTALL text, together with ./configure and ./build scripts; 
2773  611 

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

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

614 

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

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

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

617 

3006  618 

619 
*** Syntax *** 

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

620 

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

623 

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

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

625 
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

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

627 

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

632 
(Syntax.mark_boundT); 

2705  633 

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

2730  637 

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

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

639 

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

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

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

642 

3006  643 

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

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

645 

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

646 
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

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

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

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

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

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

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

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

655 

3107  656 
* substitution with equality assumptions no longer permutes other 
657 
assumptions; 

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

658 

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

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

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

662 

5726  663 
* improved combination of classical reasoner and simplifier: 
3317  664 
+ functions for handling clasimpsets 
665 
+ improvement of addss: now the simplifier is called _after_ the 

666 
safe steps. 

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

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

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

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

672 

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

675 
redex); 

676 

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

678 

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

680 

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

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

682 
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

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

685 

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

686 

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

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

688 

3042  689 
* a generic induction tactic `induct_tac' which works for all datatypes and 
3107  690 
also for type `nat'; 
3042  691 

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

694 

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

696 

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

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

699 

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

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

701 

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

704 

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

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

707 

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

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

710 

3227  711 
* HOL/Modelcheck demonstrates invocation of model checker oracle; 
712 

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

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

714 
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

715 

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

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

717 

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

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

719 

3321  720 
* a new constant `arbitrary == @x.False'; 
721 

3107  722 
* HOLCF/IOA replaces old HOL/IOA; 
723 

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

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

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

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

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

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

3006  734 

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

735 
*** ZF *** 
2553  736 

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

739 
as ZF_cs addSIs [equalityI]; 

2553  740 

2554  741 

2732  742 

2553  743 
New in Isabelle947 (November 96) 
744 
 

745 

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

747 

2554  748 
* superlinear speedup for large simplifications; 
749 

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

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

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

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

754 

755 
* improved printing of ==> : ~: 

756 

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

758 
and Modal (thanks to Sara Kalvala); 

759 

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

761 

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

763 
examples on HOL/Auth); 

764 

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

766 
the rewriter and classical reasoner simultaneously; 

767 

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

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

770 

771 

772 

773 
New in Isabelle946 

774 
 

775 

776 
* oracles  these establish an interface between Isabelle and trusted 

777 
external reasoners, which may deliver results as theorems; 

778 

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

780 

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

782 

783 
* "constdefs" section in theory files; 

784 

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

786 

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

788 

789 

790 

791 
New in Isabelle945 

792 
 

793 

794 
* reduced space requirements; 

795 

796 
* automatic HTML generation from theories; 

797 

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

799 

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

801 

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

803 

2553  804 

2557  805 

806 
New in Isabelle944 

807 
 

808 

2747  809 
* greatly reduced space requirements; 
2557  810 

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

812 

5726  813 
* searchable theorem database (see the section "Retrieving theorems" on 
2557  814 
page 8 of the Reference Manual); 
815 

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

817 
Axiom of Choice; 

818 

819 
* The previous version of HOL renamed to Old_HOL; 

820 

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

824 
* Mutually recursive inductive definitions finally work in HOL; 

825 

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

827 
translates to the operator "split"; 

828 

829 

830 

831 
New in Isabelle943 

832 
 

833 

5726  834 
* new infix operator, addss, allowing the classical reasoner to 
2557  835 
perform simplification at each step of its search. Example: 
5726  836 
fast_tac (cs addss ss) 
2557  837 

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

2557  840 
look like (a,b) instead of <a,b>; 
841 

842 
* PLEASE NOTE: CHOL will eventually replace HOL! 

843 

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

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

846 

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

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

849 

5726  850 
* Many new examples: I/O automata, ChurchRosser theorem, equivalents 
2557  851 
of the Axiom of Choice; 
852 

853 

854 

855 
New in Isabelle942 

856 
 

857 

5726  858 
* Significantly faster resolution; 
2557  859 

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

861 
freely; 

862 

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

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

865 

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

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

868 
(theory_of_thm); 

869 

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

871 

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

873 
and HOL_dup_cs obsolete; 

874 

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

876 
have been removed; 

877 

878 
* Simpler definition of function space in ZF; 

879 

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

881 

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

883 
types; 

884 

885 

2553  886 
$Id$ 