
1 EDITS TO THE ISABELLE SYSTEM FOR 1993 

2 

3 11 January 

4 

5 */README: Eliminated references to Makefile.NJ, which no longer exists. 

6 

7 **** New tar file placed on /homes/lcp (464K) **** 

8 

9 14 January 

10 

11 Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing 

12 prints conditions correctly. 

13 

14 {CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from 

15 add_mult_dist, to agree with the other _distrib rules 

16 

17 20 January 

18 

19 Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty 

20 printing annotations for types. Only the layout has changed."  Toby 

21 

22 21 January 

23 

24 {CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse 

25 

26 22 January 

27 

28 ZF/ex/equiv: new theory of equivalence classes 

29 ZF/ex/integ: new theory of integers 

30 HOL/set.thy: added indentation of 3 to all binding operators 

31 

32 ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I 

33 

34 25 January 

35 

36 MAKEALL (NJ 0.75) ran perfectly. It took 3:19 hours!? 

37 

38 ZF/bool/not,and,or,xor: new 

39 

40 27 January 

41 

42 ZF/ex/bin: new theory of binary integer arithmetic 

43 

44 27 January 

45 

46 MAKEALL (Poly/ML) ran perfectly. It took 6:33 hours??? 

47 (ZF took almost 5 hours!) 

48 

49 **** New tar file placed on /homes/lcp (472K) **** 

50 

51 HOL/set/UN_cong,INT_cong: new 

52 HOL/subset/mem_rews,set_congs,set_ss: new 

53 HOL/simpdata/o_apply: new; added to HOL_ss 

54 

55 29 January 

56 

57 Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is 

58 now called name^"(type infix)" instead of "", avoid triggering a spurious 

59 error "Attempt to merge different versions of theory: " in 

60 Pure/sign/merge_stamps 

61 

62 2 February 

63 

64 MAKEALL (Poly/ML) ran perfectly. It took 2:48 hours. Runs in 1992 took 

65 under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes 

66 according to make10836.log. 

67 

68 Pure/Thy/scan/comment: renamed from komt 

69 Pure/Thy/scan/numeric: renamed from zahl 

70 

71 Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by 

72 Tobias to change ID, TVAR, ... to lower case. 

73 

74 Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now 

75 with ID, ... in lower case and other tidying 

76 

77 3 February 

78 

79 MAKEALL (Poly/ML) ran perfectly. It took 2:50 hours. 

80 

81 4 February 

82 

83 HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n) 

84 and the nat_case rules and congruence rules 

85 

86 HOL/sum/sumE: now has the "strong" form with equality assumptions. WAS 

87 val prems = goalw Sum.thy [Inl_def,Inr_def] 

88 "[ !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) \ 

89 \ ] ==> P(s)"; 

90 by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1); 

91 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1); 

92 by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1)); 

93 val sumE = result(); 

94 

95 8 February 

96 

97 Changes from Tobias: 

98 Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not 

99 Pure/Thy/syntax: uses new list_of, list_of1 

100 

101 9 February 

102 

103 HOL/ex/arith: moved to main HOL directory 

104 HOL/prod: now define the type "unit" and constant "(): unit" 

105 

106 11 February 

107 

108 HOL/arith: eliminated redefinitions of nat_ss and arith_ss 

109 

110 12 February 

111 

112 MAKEALL (Poly/ML) ran perfectly. It took 2:50 hours. 

113 

114 Pure/Thy/scan/string: now correctly recognizes MLstyle strings. 

115 

116 15 February 

117 

118 MAKEALL (NJ 0.75) ran perfectly. It took 1:37 hours (on albatross) 

119 MAKEALL (NJ 0.75) ran perfectly. It took 2:42 hours (on dunlin) 

120 MAKEALL (Poly/ML) ran perfectly. It took 2:53 hours (on dunlin) 

121 

122 **** New tar file placed on /homes/lcp (480K) **** 

123 

124 18 February 

125 

126 Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as 

127 it was unused. 

128 

129 Pure/Syntax/earley0A: modified accordingly. 

130 

131 19 February 

132 

133 MAKEALL (NJ 0.75) ran perfectly. It took 3:37 hours 

134 MAKEALL (Poly/ML) ran perfectly. It took 2:52 hours 

135 

136 **** New tar file placed on /homes/lcp (480K) **** 

137 

138 20 February 

139 

140 MAKEALL (NJ 0.93) ran perfectly. It took 3:30 hours 

141 

142 10 March 

143 

144 HOL/fun/image_eqI: fixed bad pattern 

145 

146 11 March 

147 

148 MAKEALL (Poly/ML) failed in HOL! 

149 

150 HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws 

151 of Int and Un. 

152 

153 12 March 

154 

155 ZF/ex/misc: new example from Bledsoe 

156 

157 15 March 

158 

159 ZF/perm: two new theorems inspired by Pastre 

160 

161 16 March 

162 

163 Weakened congruence rules for HOL: speeds simplification considerably by 

164 NOT simplifying the body of a conditional or eliminator. 

165 

166 HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules 

167 

168 HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule 

169 

170 HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded 

171 operators < and <= 

172 

173 HOL/prod: weakened the congruence rule for split 

174 HOL/sum: weakened the congruence rule for case 

175 HOL/nat: weakened the congruence rule for nat_case and nat_rec 

176 HOL/list: weakened the congruence rule for List_rec and list_rec 

177 

178 HOL & test rebuilt perfectly 

179 

180 Pure/goals/prepare_proof/mkresult: fixed bug in signature check. Now 

181 compares the FINAL signature with that from the original theory. 

182 

183 Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the 

184 definitions do not update the proof state. 

185 

186 17 March 

187 

188 MAKEALL (Poly/ML) ran perfectly. 

189 

190 18 March 

191 

192 MAKEALL (Poly/ML) failed in HOL/ex/Substitutions 

193 

194 HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where 

195 necessary 

196 

197 ZF/perm: proved some rules about inj and surj 

198 

199 ZF/ex/misc: did some of Pastre's examples 

200 

201 Pure/library/gen_ins,gen_union: new 

202 

203 HOL/ex/Subst/subst: renamed rangeE to srangeE 

204 

205 18 March 

206 

207 MAKEALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in 

208 ex/Subst/alist 

209 

210 HOL/list/list_congs: new; reorganized simpsets a bit 

211 

212 Pure/goals/sign_error: new 

213 

214 Pure/goals/prepare_proof,by_com: now print the list of new theories when 

215 the signature of the proof state changes 

216 

217 HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid overwriting 

218 the library functions fst, snd 

219 

220 HOL/fun/image_compose: new 

221 

222 21 March 

223 

224 MAKEALL (NJ 0.93) ran perfectly. It took 3:50 hours 

225 MAKEALL (Poly/ML) ran perfectly. It took 3:21 hours 

226 Much slower now (about 30 minutes!) because of HOL/ex/Subst 

227 

228 **** New tar file placed on /homes/lcp (504K) **** 

229 

230 ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid overwriting 

231 the library functions fst, snd 

232 

233 HOL/prod/prod_fun_imageI,E: new 

234 

235 HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify 

236 of Pure 

237 

238 24 March 

239 

240 HOL/trancl/comp_subset_Sigma: new 

241 HOL/wf/wfI: new 

242 

243 HOL/Subst: moved from HOL/ex/Subst to shorten pathnames 

244 HOL/Makefile: target 'test' now loads Subst/ROOT separately 

245 

246 *** Installation of gfp, coinduction, ... to HOL *** 

247 

248 HOL/gfp,llist: new 

249 HOL/univ,sexp,list: replaced with new version 

250 

251 Sexp is now the set of all wellfounded trees, each of type 'a node set. 

252 There is no longer a type 'sexp'. Initial algebras require more explicit 

253 type checking than before. Defining a type 'sexp' would eliminate this, 

254 but would also require a whole new set of primitives, similar to those 

255 defined in univ.thy but restricted to wellfounded trees. 

256 

257 25 March 

258 

259 Pure/thm: renamed 'bires' to 'eres' in many places (not exported)  

260 biresolution now refers to resolution with (flag,rule) pairs. 

261 

262 Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming. A Var in 

263 a premise was getting renamed when its occurrence in the flexflex pairs was 

264 not. Martin Coen supplied the following proof of True=False in HOL: 

265 

266 val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c"; 

267 br (prem RS bexE) 1; be ssubst 1; be singletonD 1; 

268 val l1 = result(); 

269 

270 val rls = [refl] RL [bexI] RL [l1]; 

271 

272 goal Set.thy "True = False"; 

273 brs rls 1; br singletonI 1; 

274 result(); 

275 

276 Marcus Moore noted that the error only occurred with 

277 Logic.auto_rename:=false. Elements of the fix: 

278 

279 1. rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the 

280 existing flexflex pairs) as an extra argument. rename_bvs preserves all 

281 Vars in tpairs. 

282 

283 2. bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs 

284 to newAs. 

285 

286 HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski 

287 

288 HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed 

289 def_Tarski to def_lfp_Tarski 

290 

291 26 March 

292 

293 MAKEALL (NJ 0.93) ran perfectly. It took 4:25 hours! 

294 MAKEALL (Poly/ML) ran perfectly. It took 3:54 hours! (jobs overlapped) 

295 

296 Pure/Thy/scan/is_digit,is_letter: deleted. They are already in 

297 Pure/library, and these versions used nonStandard string comparisons! 

298 

299 Repairing a fault reported by David Aspinall: 

300 show_types := true; read "a"; (* followed by 'prin it' for NJ *) 

301 Raises exception LIST "hd". Also has the side effect of leaving 

302 show_types set at false. 

303 

304 Pure/goals/read: no longer creates a null TVar 

305 Pure/Syntax/lexicon/string_of_vname: now handles null names 

306 Pure/Syntax/printer/string_of_typ: tidied 

307 

308 /usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug 

309 MAKEALL on this directory ran perfectly 

310 /usr/groups/theory/mlaftp/Isabelle92.tar.Z: replaced by new version 

311 

312 29 March 

313 

314 MAKEALL (NJ 0.93) ran perfectly. It took 4:14 hours! 

315 MAKEALL (Poly/ML) ran perfectly. It took 3:43 hours! 

316 

317 **** New tar file placed on /homes/lcp (518K) **** 

318 

319 30 March 

320 

321 ZF/univ/cons_in_Vfrom: deleted "[ a: Vfrom(A,i); b<=Vfrom(A,i) ] ==> 

322 cons(a,b) : Vfrom(A,succ(i))" since it was useless. 

323 

324 8 April 

325 

326 MAKEALL (Poly/ML) ran perfectly. It took 3:49 hours! 

327 

328 **** New tar file placed on /homes/lcp (520K) **** 

329 

330 **** Updates for pattern unification (Tobias Nipkow) **** 

331 

332 Pure/pattern.ML: new, pattern unification 

333 

334 Pure/Makefile and ROOT.ML: included pattern.ML 

335 

336 Pure/library.ML: added predicate downto0 

337 

338 Pure/unify.ML: call pattern unification first. Removed call to could_unify. 

339 

340 FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead) 

341 

342 **** Installation of Martin Coen's FOLP (FOL + proof objects) **** 

343 

344 renamed PFOL, PIFOL to FOLP, IFOLP, etc. 

345 

346 9 April 

347 

348 MAKEALL (NJ 0.93) ran perfectly. It took 4:05 hours! 

349 MAKEALL (Poly/ML) ran perfectly. It took 3:31 hours! 

350 

351 **** New tar file placed on /homes/lcp (576K) **** 

352 

353 **** Installation of Discrimination Nets **** 

354 

355 *Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac) 

356 Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML 

357 Provers/simp.ML 

358 HOL/ex/meson.ML 

359 

360 *Affected files (those mentioning compat_resolve_tac) 

361 Pure/tactic.ML 

362 Provers/typedsimp.ML 

363 CTT/ctt.ML 

364 

365 Pure/stringtree: saved on Isabelle/old 

366 Pure/net: new 

367 Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML 

368 Pure/ROOT: now mentions net.ML, not stringtree.ML 

369 

370 Pure/goals/compat_goal: DELETED 

371 

372 Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm, 

373 delete_thm,head_string: DELETED 

374 

375 Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac, 

376 net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac, 

377 net_resolve_tac, net_match_tac: NEW 

378 

379 Pure/tactic/filt_resolve_tac: new implementation using nets! 

380 

381 Provers/simp: replaced by new version 

382 

383 Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and 

384 updated comments 

385 

386 CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac 

387 ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac 

388 

389 CTT tested 

390 

391 HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net 

392 

393 FOL tested 

394 

395 Provers/simp/cong_const: new, replaces head_string call in cong_consts 

396 Provers/simp: renamed variables: atomic to at and cong_consts to ccs 

397 

398 ZF/ex/bin/integ_of_bin_type: proof required reordering of rules  

399 typechk_tac now respects this ordering! 

400 

401 ZF tested 

402 

403 DOCUMENTATION 

404 

405 Logics/CTT: Removed mention of compat_resolve_tac 

406 Ref/goals: deleted compat_goal's entry 

407 

408 Provers/hypsubst/lasthyp_subst_tac: deleted 

409 

410 FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works! 

411 

412 12 April 

413 

414 MAKEALL (NJ 0.93) ran perfectly. It took 4:03 hours! 

415 MAKEALL (Poly/ML) ran perfectly. It took 3:28 hours! 

416 

417 FOLP/{intprover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac 

418 FOLP/{intprover,classical}/inst_step_tac: restored, calls assume and mp_tac 

419 FOLP/{intprover,classical}/step_tac: calls inst_step_tac 

420 

421 {FOL,FOLP}/intprover/safe_brls: removed (asm_rl,true) since assume_tac is 

422 used explicitly!! 

423 

424 FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless 

425 

426 FOLP/{intprover,classical}/uniq_mp_tac: replace eq_mp_tac and call 

427 uniq_assume_tac 

428 

429 Provers/classical: REPLACED BY 'NET' VERSION! 

430 

431 13 April 

432 

433 MAKEALL (Poly/ML) failed in ZF and ran out of quota for Cube. 

434 

435 Unification bug (nothing to do with pattern unification) 

436 Cleaning of flexflex pairs attempts to remove all occurrences of bound 

437 variables not common to both sides. Arguments containing "banned" bound 

438 variables are deleted  but this should ONLY be done if the occurrence is 

439 rigid! 

440 

441 unify/CHANGE_FAIL: new, for flexible occurrence of bound variable 

442 unify/change_bnos: now takes "flex" as argument, indicating path status 

443 

444 14 April 

445 

446 MAKEALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK 

447 

448 LK/ex/hardquant/37: added "by flexflex_tac" to compensate for flexflex 

449 changes 

450 

451 Pure/goals/gethyps: now calls METAHYPS directly 

452 

453 rmlogfiles: no longer mentions directories. WAS 

454 rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log 

455 rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test 

456 rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML 

457 rm {FOL,ZF,HOL}/ex/.*.thy.ML 

458 

459 MAKEALL (Poly/ML) ran perfectly. It took 2:39 hours! (albatross) 

460 

461 New version of simp on Isabelle/new  instantiates unknowns provided only 

462 one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR] 

463 

464 works with FOLP/ex/nat, but in general could fail in the event of 

465 overlapping rewrite rules, since FOLP always instantiates unknowns during 

466 rewriting. 

467 

468 ZF: tested with new version 

469 

470 HOL: tested with new version, appeared to loop in llist/Lmap_ident 

471 

472 **** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS **** 

473 

474 ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous! 

475 ZF/wfrec: all uses of wf_ss' require 

476 by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN 

477 SIMP_TAC (wf_ss' addrews (hyps)) 1) 1); 

478 

479 ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes 

480 METAHYPS version work 

481 

482 ZF/arith/add_not_less_self: adds anti_refl_rew 

483 

484 ZF/ex/proplog/hyps_finite: the use of UN_I is very bad  too undirected. 

485 Swapping the premises of UN_I would probably allow instantiation. 

486 

487 ZF otherwise seems to work! 

488 

489 HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars 

490 

491 HOL/ex/proplog/comp_lemma: failed due to uninstantiated Var in 

492 (CCONTR_rule RS allI) 

493 

494 *** REJECTED 

495 

496 15 April 

497 

498 These overnight runs involve Provers/simp.ML with old treatment of rules 

499 (match_tac) and no METAHYPS; they test the new flexflex pairs and 

500 discrimination nets, to see whether it runs faster. 

501 

502 MAKEALL (NJ 0.93) ran perfectly. It took 3:39 hours (4 mins faster) 

503 MAKEALL (Poly/ML) ran perfectly. It took 3:23 hours (5 mins faster) 

504 

505 ZF/simpdata/ZF_ss: deleted anti_refl_rew; nonlinear patterns slow down 

506 discrimination nets (and this rewrite used only ONCE) 

507 

508 ZF/mem_not_refl: new; replaces obsolete anti_refl_rew 

509 

510 **Timing experiments** 

511 

512 fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1); 

513 

514 On large examples such as ... 

515 HOL/arith/mod_quo_equality 

516 HOL/llist/LListD_implies_ntrunc_equality 

517 ZF/ex/bin/integ_of_bin_succ 

518 ... it is 1.5 to 3 times faster than ASM_SIMP_TAC. But cannot replace 

519 ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions. 

520 If there are few assumptions then HYP_SIMP_TAC is no better. 

521 

522 Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling 

523 make_database, so that users can call make_database for their objectlogics. 

524 

525 Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is 

526 only one subgoal. 

527 

528 19 April 

529 

530 MAKEALL (NJ 0.93) failed in HOL due to lack of disc space. 

531 MAKEALL (Poly/ML) ran perfectly. It took 3:23 hours 

532 

533 **** Installation of new simplifier **** 

534 

535 Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg 

536 to the auto_tac. 

537 

538 FOL,HOL/simpdata: auto_tac now handles the hyps argument 

539 

540 ZF/simpdata/standard_auto_tac: deleted 

541 ZF/simpdata/auto_tac: added hyps argument 

542 ZF/epsilon/eclose_least_lemma: no special auto_tac 

543 

544 */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..." 

545 

546 20 April 

547 

548 MAKEALL failed in HOL/Subst 

549 

550 HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified. 

551 Old version caused ambiguity in rewriting: 

552 "[ P ==> P>Q; ~P ==> ~P>Q ] ==> Q"; 

553 

554 **** New tar file placed on /homes/lcp (????) **** 

555 

556 Pure/Syntax: improvements to the printing of syntaxes 

557 Pure/Syntax/lexicon.ML: added name_of_token 

558 Pure/Syntax/earley0A.ML: updated print_gram 

559 

560 21 April 

561 

562 MAKEALL (NJ 0.93) ran perfectly. It took 3:44 hours 

563 MAKEALL (Poly/ML) failed in HOL due to lack of disc space 

564 

565 HOL/list,llist: now share NIL, CONS, List_Fun and List_case 

566 

567 makeall: now compresses the log files, which were taking up 4M; this 

568 reduces their space by more than 1/3 

569 

570 rmlogfiles: now deletes compressed log files. 

571 

572 ** Patrick Meche has noted that if the goal is stated with a leading !! 

573 quantifier, then the list of premises is always empty  this gives the 

574 effect of an initial (cut_facts_tac prems 1). The final theorem is the 

575 same as it would be without the quantifier. 

576 

577 ZF: used the point above to simplify many proofs 

578 ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac 

579 

580 22 April 

581 

582 MAKEALL (NJ 0.93) ran perfectly. It took 3:52 hours?? 

583 MAKEALL (Poly/ML) ran perfectly. It took 3:16 hours 

584 

585 30 April 

586 

587 HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow) 

588 

589 HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert", 

590 new derivations for "singleton" 

591 

592 HOL/llist.thy,llist.ML: changed {x.False} to {} 

593 

594 **** New tar file placed on /homes/lcp (584K) **** 

595 

596 4 May 

597 

598 MAKEALL (NJ 0.93) ran out of space in LK. 

599 MAKEALL (Poly/ML) ran perfectly. It took 3:14 hours 

600 

601 Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is 

602 writeprotected 

603 

604 5 May 

605 

606 HOL/list/not_Cons_self: renamed from l_not_Cons_l 

607 HOL/list/not_CONS_self: new 

608 

609 HOL/llist.thy/Lconst: changed type and def to remove Leaf 

610 HOL/llist.ML: changed Lconst theorems 

611 

612 6 May 

613 

614 MAKEALL (Poly/ML) ran perfectly. It took 3:18 hours 

615 

616 ** Installation of new HOL from Tobias ** 

617 

618 HOL/ex/{finite,proplog} made like the ZF versions 

619 HOL/hol.thy: type classes plus, minus, times; overloaded operators +  * 

620 HOL/set: set enumeration via "insert" 

621 additions to set_cs and set_ss 

622 HOL/set,subset,equalities: various lemmas to do with {}, insert and  

623 HOL/llist: One of the proofs needs one fewer commands 

624 HOL/arith: many proofs require type constraints due to overloading 

625 

626 ** end Installation ** 

627 

628 ZF/ex/misc: added new lemmas from Abrial's paper 

629 

630 7 May 

631 

632 HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous 

633 simplification now proves the subgoal. 

634 

635 **** New tar file placed on /homes/lcp (584K) **** 

636 

637 ** Installation of new simplifier from Tobias ** 

638 

639 The "case_splits" parameter of SimpFun is moved from the signature to the 

640 simpset. SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed. The ordinary 

641 simplification tactics perform case splits if present in the simpset. 

642 

643 The simplifier finds out for itself what constant is affected. Instead of 

644 supplying the pair (expand_if,"if"), supply just the rule expand_if. 

645 

646 This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun. 

647 

648 MAKEALL (Poly/ML) ran perfectly. It took 3:18 hours 

649 

650 Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and 

651 DEPTH_SOLVE 

652 

653 HOL: installation of NORM tag for simplication. How was it forgotten?? 

654 

655 HOL/hol.thy: declaration of NORM 

656 HOL/simpdata: NORM_def supplied to SimpFun 

657 

658 10 May 

659 

660 MAKEALL (Poly/ML) ran perfectly. It took 3:33 hours?? 

661 

662 11 May 

663 

664 HOL/prod/Prod_eq: renamed Pair_eq 

665 HOL/ex/lexprod: wf_lex_prod: simplified proof 

666 

667 HOL/fun/inj_eq: new 

668 

669 HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits! 

670 

671 12 May 

672 

673 MAKEALL (NJ 0.93) ran out of space in HOL. 

674 MAKEALL (Poly/ML) failed in HOL. 

675 HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules 

676 

677 13 May 

678 

679 Pure/logic/flexpair: moved to term, with "equals" etc. Now pervasive 

680 Pure/logic/mk_flexpair: now exported 

681 Pure/logic/dest_flexpair: new 

682 Pure/goals/print_exn: now prints the error message for TERM and TYPE 

683 

684 Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because 

685 flexflex pairs can have any type at all. Thus == must have the same type. 

686 

687 Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}. 

688 

689 Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix) 

690 Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs 

691 

692 Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now, 

693 not by integers. (Changed by Tobias) 

694 

695 *** Installation of more printing functions *** 

696 

697 Pure/sign/sg: changed from a type abbrev to a datatype 

698 Pure/type/type_sig: changed from a type abbrev to a datatype 

699 These changes needed for abstract type printing in NJ 

700 

701 Pure/tctical/print_sg,print_theory: new 

702 

703 Pure/drule: new file containing derived rules and printing functions. 

704 Mostly from tctical.ML, but includes rewriting rules from tactic.ML. 

705 

706 Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now 

707 depend on Drule and have sharing constraints. 

708 

709 14 May 

710 

711 Installing new print functions for New Jersey: incompatible with Poly/ML! 

712 

713 Pure/NJ/install_pp_nj: new (requires datatypes as above) 

714 Pure/POLY/install_pp_nj: a dummy version 

715 

716 Pure/ROOT: calls install_pp_nj to install printing for NJ 

717 

718 */ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for 

719 Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another 

720 logic  make_database is not used] 

721 

722 17 May 

723 

724 MAKEALL (NJ 0.93) ran perfectly. It took 3:57 hours?? 

725 

726 Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias) 

727 

728 18 May 

729 

730 MAKEALL (Poly/ML) ran perfectly. It took 3:36 hours 

731 

732 19 May 

733 

734 ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of 

735 complex assumptions 

736 

737 20 May 

738 

739 HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl, 

740 null and list_case. 

741 

742 1 June 

743 

744 MAKEALL (Poly/ML) ran perfectly. It took 3:39 hours 

745 

746 **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 

747 

748 MAKEALL (NJ 0.93) ran perfectly. It took 1:49 hours on albatross. 

749 

750 Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new 

751 make_elim_preserve to preserve Var indexes when creating the elimination 

752 rule. 

753 

754 ZF/ex/ramsey: modified calls to dres_inst_tac 

755 

756 2 June 

757 

758 Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the 

759 current directory, since the pathname may lead to a nonwriteable area. 

760 

761 HOL/arith: renamed / and // to div and mod 

762 ZF/arith: renamed #/ and #// to div and mod 

763 

764 MAKEALL (Poly/ML) ran perfectly. It took 1:48 hours on albatross. 

765 

766 **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 

767 

768 Pure/NJ/commit: new dummy function 

769 FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems 

770 

771 makeall: now builds FOLP also! 

772 

773 3 June 

774 

775 ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_], 

776 <_,_> are formatted as {(_)}, [(_)], 

777 

778 MAKEALL (Poly/ML) ran perfectly. It took 4:37 hours on muscovy (with FOLP). 

779 

780 ZF/Makefile: removed obsolete target for .rules.ML 

781 

782 All objectlogic Makefiles: EXAMPLES ARE NO LONGER SAVED. This saves disc 

783 and avoids problems (in New Jersey ML) of writing to the currently 

784 executing image. 

785 

786 4 June 

787 

788 Pure/logic/rewritec: now uses nets for greater speed. Functor LogicFun now 

789 takes Net as argument. 

790 

791 Pure/ROOT: now loads net before logic. 

792 

793 MAKEALL (Poly/ML) failed in ZF and HOL. 

794 

795 LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL) 

796 

797 7 June 

798 

799 Pure/tactic/is_letdig: moved to library 

800 Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig 

801 

802 MAKEALL (Poly/ML) ran perfectly. It took 2:07 hours on albatross. 

803 MAKEALL (NJ 0.93) ran perfectly. It took 4:41 hours on dunlin. 

804 

805 HOL/set/UN1,INT1: new union/intersection operators. Binders UN x.B(x), 

806 INT x.B(x). 

807 

808 HOL/univ,llist: now use UN x.B(x) instead of Union(range(B)) 

809 

810 HOL/subset: added lattice properties for INT, UN (both forms) 

811 

812 8 June 

813 

814 MAKEALL (NJ 0.93) ran perfectly. It took 4:45 hours on dunlin. 

815 

816 **** New tar file 92.tar.z placed on /homes/lcp (384K) **** 

817 

818 14 June 

819 

820 HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp. 

821 Using def_wfrec hides such errors!! 

822 

823 **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 

824 

825 ** NEW VERSION FROM MUNICH WITH ==REWRITING ** 

826 

827 ** The following changes are Toby's ** 

828 

829 type.ML: 

830 

831 Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars. 

832 Added both functions to the signature. 

833 

834 sign.ML: 

835 

836 Added val subsig: sg * sg > bool to signature. 

837 Added trueprop :: prop and mark_prop : prop => prop to pure_sg. 

838 

839 Added 

840 

841 val freeze_vars: term > term 

842 val thaw_vars: term > term 

843 val strip_all_imp: term * int > term list * term * int 

844 

845 Moved rewritec_bottom and rewritec_top to thm.ML. 

846 Only bottomup rewriting supported any longer. 

847 

848 thm.ML: 

849 

850 Added 

851 

852 (* internal form of conditional ==rewrite rules *) 

853 type meta_simpset 

854 val add_mss: meta_simpset * thm list > meta_simpset 

855 val empty_mss: meta_simpset 

856 val mk_mss: thm list > meta_simpset 

857 

858 val mark_prop_def: thm 

859 val truepropI: thm 

860 val trueprop_def: thm 

861 

862 (* bottomup conditional ==rewriting with local ==>assumptions *) 

863 val rewrite_cterm: meta_simpset > (thm > thm list) 

864 > (meta_simpset > thm list > Sign.cterm > thm) 

865 > Sign.cterm > thm 

866 val trace_simp: bool ref 

867 

868 Simplified concl_of: call to Logic.skip_flexpairs redundant. 

869 

870 drule.ML: 

871 

872 Added 

873 

874 (* rewriting *) 

875 val asm_rewrite_rule: (thm > thm list) > thm list > thm > thm 

876 val rewrite_goal_rule: (thm > thm list) > thm list > int > thm > thm 

877 val rewrite_goals_rule: (thm > thm list) > thm list > thm > thm 

878 

879 (* derived concepts *) 

880 val forall_trueprop_eq: thm 

881 val implies_trueprop_eq: thm 

882 val mk_trueprop_eq: thm > thm 

883 val reflexive_eq: thm 

884 val reflexive_thm: thm 

885 val trueprop_implies_eq: thm 

886 val thm_implies: thm > thm > thm 

887 val thm_equals: thm > thm > thm 

888 

889 (*Moved here from tactic.ML:*) 

890 val asm_rl: thm 

891 val cut_rl: thm 

892 val revcut_rl: thm 

893 

894 tactic.ML: 

895 

896 Added 

897 

898 val asm_rewrite_goal_tac: (thm > thm list) > thm list > int > tactic 

899 val asm_rewrite_goals_tac: (thm > thm list) > thm list > tactic 

900 val asm_rewrite_tac: (thm > thm list) > thm list > tactic 

901 val fold_goal_tac: thm list > int > tactic 

902 val rewrite_goal_tac: thm list > int > tactic 

903 

904 Moved to drule.ML: 

905 val asm_rl: thm 

906 val cut_rl: thm 

907 val revcut_rl: thm 

908 

909 goals.ML: 

910 

911 Changed prepare_proof to make sure that rewriting with empty list of 

912 metathms is identity. 

913 

914 ** End of Toby's changes ** 

915 

916 16 June 

917 

918 Pure/sign/typ_of,read_ctyp: new 

919 Pure/logic/dest_flexpair: now exported 

920 

921 Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in 

922 flexpair_abs_elim_list 

923 

924 HOL/equalities/image_empty,image_insert: new 

925 HOL/ex/finite/Fin_imageI: new 

926 

927 Installed Martin Coen's CCL as new objectlogic 

928 

929 17 June 

930 

931 ** More changes from Munich (Markus Wenzel) ** 

932 

933 Pure/library: added the, is_some, is_none, separate and improved space_implode 

934 Pure/sign: Sign.extend now calls Syntax.extend with list of constants 

935 Pure/symtab: added is_null 

936 Pure/Syntax/sextension: added empty_sext 

937 Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version 

938 

939 HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to 

940 specify h 8000. 

941 

942 HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption 

943 

944 18 June 

945 

946 MAKEALL (Poly/ML) ran perfectly. It took 4:59 hours on dunlin (with CCL). 

947 

948 Pure/sign/read_def_cterm: now prints the offending terms, as well as the 

949 types, when exception TYPE is raised. 

950 

951 HOL/llist: some tidying 

952 

953 23 June 

954 

955 HOL/llist/Lconst_type: generalized from Lconst(M): LList({M}) 

956 

957 24 June 

958 

959 MAKEALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross (with CCL) 

960 

961 MAKEALL (NJ 0.93) failed in CCL due to use of "abstraction" as an 

962 identifier in CCL.ML 

963 

964 **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL) 

965 

966 CCL/ROOT: added ".ML" extension to use commands for NJ compatibility 

967 

968 25 June 

969 

970 MAKEALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross. 

971 MAKEALL (NJ 0.93) failed in HOL due to lack of ".ML" extension 

972 

973 HOL/fun/rangeE,imageE: etaexpanded f to get variable name preservation 

974 

975 HOL/llist/iterates_equality,lmap_lappend_distrib: tidied 

976 

977 28 June 

978 

979 HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable 

980 name preservation 

981 

982 HOL/llist: coinduction rules applied with res_inst_tac to state the 

983 bisimulation directly 

984 

985 2 July 

986 

987 MAKEALL (NJ 0.93) ran perfectly. It took 2:10 hours on albatross. 

988 MAKEALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross. 

989 

990 92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database= 

991 

992 **** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL) 

993 

994 

995 ** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER ** 

996 

997 I have merged in the changes shown above since 24 June 

998 

999 CHANGES LOG OF Markus Wenzel (MMW) 

1000 ======= 

1001 

1002 29Jun1993 MMW 

1003 *** Beta release of new syntax module *** 

1004 (should be 99% backwards compatible) 

1005 

1006 Pure/Thy/ROOT.ML 

1007 added keywords for "translations" section 

1008 

1009 Pure/Thy/syntax.ML 

1010 minor cleanup 

1011 added syntax for "translations" section 

1012 .*.thy.ML files now human readable 

1013 .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section 

1014 "ML" section no longer demands any definitions (parse_translation, ...) 

1015 

1016 Pure/Thy/read.ML 

1017 read_thy: added close_in 

1018 added file_exists (not perfect) 

1019 use_thy: now uses file_exists 

1020 

1021 Pure/thm.ML 

1022 added syn_of: theory > syntax 

1023 

1024 Pure/Makefile 

1025 SYNTAX_FILES: added Syntax/ast.ML 

1026 

1027 Pure/Syntax/pretty.ML 

1028 added str_of: T > string 

1029 

1030 Pure/Syntax/ast.ML 

1031 added this file 

1032 

1033 Pure/Syntax/extension.ML 

1034 Pure/Syntax/parse_tree.ML 

1035 Pure/Syntax/printer.ML 

1036 Pure/Syntax/ROOT.ML 

1037 Pure/Syntax/sextension.ML 

1038 Pure/Syntax/syntax.ML 

1039 Pure/Syntax/type_ext.ML 

1040 Pure/Syntax/xgram.ML 

1041 These files have been completely rewritten, though the global structure 

1042 is similar to the old one. 

1043 

1044 

1045 30Jun1993 MMW 

1046 New versions of HOL and Cube: use translation rules wherever possible; 

1047 

1048 HOL/hol.thy 

1049 cleaned up 

1050 removed alt_tr', mk_bindopt_tr' 

1051 alternative binders now implemented via translation rules and mk_alt_ast_tr' 

1052 

1053 HOL/set.thy 

1054 cleaned up 

1055 removed type "finset" 

1056 now uses category "args" for finite sets 

1057 junked "ML" section 

1058 added "translations" section 

1059 

1060 HOL/list.thy 

1061 cleaned up 

1062 removed type "listenum" 

1063 now uses category "args" for lists 

1064 junked "ML" section 

1065 added "translations" section 

1066 

1067 Cube/cube.thy 

1068 cleaned up 

1069 changed indentation of Lam and Pi from 2 to 3 

1070 removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr' 

1071 fixed fun_tr': all but one newly introduced frees will have type dummyT 

1072 added "translations" section 

1073 

1074 

1075 30Jun1993, 05Jul1993 MMW 

1076 Improved toplevel pretty printers: 

1077  unified interface for POLY and NJ; 

1078  print functions now insert atomic string into the toplevel's pp stream, 

1079 rather than writing it to std_out (advantage: output appears at the 

1080 correct position, disadvantage: output cannot be broken); 

1081 (Is there anybody in this universe who exactly knows how Poly's install_pp 

1082 is supposed to work?); 

1083 

1084 Pure/NJ.ML 

1085 removed dummy install_pp 

1086 added make_pp, install_pp 

1087 

1088 Pure/POLY.ML 

1089 removed dummy install_pp_nj 

1090 added make_pp 

1091 

1092 Pure/ROOT.ML 

1093 removed install_pp_nj stuff 

1094 

1095 Pure/drule.ML 

1096 added str_of_sg, str_of_theory, str_of_thm 

1097 

1098 Pure/install_pp.ML 

1099 added this file 

1100 

1101 Pure/sign.ML 

1102 added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp 

1103 

1104 Pure/goals.ML 

1105 added str_of_term, str_of_typ 

1106 

1107 CTT/ROOT.ML 

1108 Cube/ROOT.ML 

1109 FOL/ROOT.ML 

1110 FOLP/ROOT.ML 

1111 HOL/ROOT.ML 

1112 LK/ROOT.ML 

1113 replaced install_pp stuff by 'use "../Pure/install_pp.ML"' 

1114 

1115 

1116 01Jul1993 MMW 

1117 Misc small fixes 

1118 

1119 CCL/ROOT.ML 

1120 HOL/ROOT.ML 

1121 added ".ML" suffix to some filenames 

1122 

1123 HOL/ex/unsolved.ML 

1124 replaced HOL_Rule.thy by HOL.thy 

1125 

1126 Pure/NJ.ML 

1127 quit was incorrectly int > unit 

1128 

1129 END MMW CHANGES 

1130 

1131 Pure/Syntax/sextension/eta_contract: now initially false 

1132 

1133 Pure/library/cat_lines: no longer calls "distinct" 

1134 Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines 

1135 NB This could cause duplicate error messages from Pure/sign and Pure/type 

1136 

1137 Pure/goals/prove_goalw: now prints some of the information from print_exn 

1138 

1139 9 July 

1140 

1141 MAKEALL (Poly/ML) ran perfectly. It took 2:26 hours on albatross. 

1142 

1143 **** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 

1144 

1145 12 July 

1146 

1147 MAKEALL (NJ 0.93) ran perfectly. It took 2:13 hours on albatross. 

1148 MAKEALL (Poly/ML) ran perfectly. It took 2:25 hours on albatross. 

1149 

1150 22 July 

1151 

1152 ZF/zf.thy: new version from Marcus Wenzel 

1153 

1154 ZF: ** installation of inductive definitions ** 

1155 

1156 changing the argument order of "split"; affects fst/snd too 

1157 sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy 

1158 pair.ML ex/integ.ML 

1159 

1160 changing the argument order of "case" and adding "Part": sum.thy sum.ML 

1161 

1162 ZF/zf.ML/rev_subsetD,rev_bspec: new 

1163 

1164 ZF/mono: new rules for implication 

1165 ZF/mono/Collect_mono: now for use with implication rules 

1166 

1167 ZF/zf.ML/ballE': renamed rev_ballE 

1168 

1169 ZF/list.thy,list.ML: files renamed listfn.thy, listfn.ML 

1170 ZF/list.ML: new version simply holds the datatype definition 

1171 NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair. 

1172 

1173 ZF/extend_ind.ML, datatype.ML: new files 

1174 ZF/fin.ML: moved from ex/finite.ML 

1175 

1176 23 July 

1177 

1178 ZF/ex/sexp: deleted this example  it seems hardly worth the trouble of 

1179 porting. 

1180 

1181 ZF/ex/bt.thy,bt.ML: files renamed btfn.thy, btfn.ML 

1182 ZF/ex/bt.ML: new version simply holds the datatype definition 

1183 

1184 ZF/ex/term.thy,term.ML: files renamed termfn.thy, termfn.ML 

1185 ZF/ex/term.ML: new version simply holds the datatype definition 

1186 

1187 ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI 

1188 

1189 26 July 

1190 

1191 ZF/univ/rank_ss: new, for proving recursion equations 

1192 

1193 ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff, 

1194 field_of_prod:new 

1195 

1196 ZF/domrange/field_subset: modified 

1197 

1198 ZF/list/list_cases: no longer proved by induction! 

1199 ZF/wf/wf_trancl: simplified proof 

1200 

1201 ZF/equalities: new laws for field 

1202 

1203 29 July 

1204 

1205 ZF/trancl/trancl_induct: new 

1206 ZF/trancl/rtrancl_induct,trancl_induct: now with more type information 

1207 

1208 ** More changes from Munich (Markus Wenzel) ** 

1209 

1210 Update of new syntax module (aka macro system): mostly internal cleanup and 

1211 polishing; 

1212 

1213 Pure/Syntax/* 

1214 added Ast.stat_norm 

1215 added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax 

1216 cleaned type and Pure syntax: "_CLASSES" > "classes", "_SORTS" > "sorts", 

1217 "_==>" > "==>", "_fun" > "fun", added some space for printing 

1218 Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before 

1219 any Var or Free of type propT 

1220 Syntax: added ndependent_tr, dependent_tr' 

1221 

1222 Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext) 

1223 

1224 Changes to object logics: minor cleanups and replacement of most remaining ML 

1225 translations by rewrite rules (see also file "Translations"); 

1226 

1227 ZF/zf.thy 

1228 added "translations" section 

1229 removed all parse/print translations except ndependent_tr, dependent_tr' 

1230 fixed dependent_tr': all but one newly introduced frees have type dummyT 

1231 replaced id by idt in order to make terms rereadable if !show_types 

1232 

1233 Cube/cube.thy 

1234 removed necontext 

1235 replaced fun_tr/tr' by ndependent_tr/dependent_tr' 

1236 

1237 CTT/ctt.thy 

1238 added translations rules for PROD and SUM 

1239 removed dependent_tr 

1240 removed definitions of ndependent_tr, dependent_tr' 

1241 

1242 HOL/set.thy: replaced id by idt 

1243 

1244 CCL/ROOT.ML: Logtic > Logic 

1245 

1246 CCL/set.thy 

1247 added "translations" section 

1248 removed "ML" section 

1249 replaced id by idt 

1250 

1251 CCL/types.thy 

1252 added "translations" section 

1253 removed definitions of ndependent_tr, dependent_tr' 

1254 replaced id by idt 

1255 

1256 Yet another improvement of toplevel pretty printers: output now breakable; 

1257 

1258 Pure/NJ.ML Pure/POLY.ML improved make_pp 

1259 

1260 Pure/install_pp.ML: replaced str_of_* by pprint_* 

1261 

1262 Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_* 

1263 

1264 Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_* 

1265 

1266 Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_* 

1267 

1268 Pure/Syntax/pretty.ML: added pprint, quote 

1269 

1270 Minor changes and additions; 

1271 

1272 Pure/sign.ML: renamed stamp "PURE" to "Pure" 

1273 

1274 Pure/library.ML 

1275 added quote: string > string 

1276 added to_lower: string > bool 

1277 

1278 Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm 

1279 

1280 30 July 

1281 

1282 MAKEALL (Poly/ML) ran perfectly. 

1283 

1284 Pure/goals/print_sign_exn: new, takes most code from print_exn 

1285 Pure/goals/prove_goalw: displays exceptions using print_sign_exn 

1286 

1287 Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg 

1288 

1289 Pure/library,...: replaced front/nth_tail by take/drop. 

1290 

1291 Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new 

1292 thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above 

1293 

1294 Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless: 

1295 moved to term, joining similar functions for type variables; 

1296 Logic.vars and Logic.frees are now term_vars and term_frees 

1297 

1298 Pure/term/subst_free: new 

1299 

1300 Pure/tactic/is_fact: newly exported 

1301 

1302 Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules 

1303 

1304 Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of 

1305 forall is_letdig 

1306 

1307 **** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 

1308 

1309 2 August 

1310 

1311 MAKEALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr 

1312 MAKEALL (Poly/ML) failed in ZF/enum. It took 2:33 hours on albatross. 

1313 

1314 Pure/drule/triv_forall_equality: new 

1315 Pure/tactic/prune_params_tac: new 

1316 

1317 Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac 

1318 

1319 3 August 

1320 

1321 Pure/tactic/rule_by_tactic: new 

1322 

1323 ZF/perm/compEpair: now proved via rule_by_tactic 

1324 

1325 ZF/extend_ind/cases,mk_cases: new 

1326 ZF/datatype/mk_free: new 

1327 ZF/list: now calls List.mk_cases 

1328 

1329 4 August 

1330 

1331 Provers/slow_tac,slow_best_tac: new 

1332 

1333 5 August 

1334 

1335 MAKEALL (Poly/ML) failed in ZF 

1336 

1337 ZF/sum/sumE2: deleted since unused 

1338 ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new 

1339 ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset 

1340 

1341 6 August 

1342 

1343 Pure/goals/prepare_proof: after "Additional hypotheses", now actually 

1344 prints them! 

1345 

1346 ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from 

1347 Transset_Union, Transset_Inter 

1348 

1349 ZF/ordinal/Transset_Union: new 

1350 ZF/univ/pair_in_univ: renamed Pair_in_univ 

1351 

1352 ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ 

1353 

1354 ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed 

1355 uses in extend_ind.ML, nat.ML, trancl.ML. 

1356 

1357 ZF/ex/misc: SchroederBernstein Theorem moved here from lfp.ML 

1358 

1359 ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added 

1360 

1361 9 August 

1362 

1363 ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on 

1364 Syntax/sextension. 

1365 

1366 11 August 

1367 

1368 Pure/library.ML: added functions 

1369 assocs: (''a * 'b list) list > ''a > 'b list 

1370 transitive_closure: (''a * ''a list) list > (''a * ''a list) list 

1371 

1372 Pure/type.ML: deleted (inefficient) transitive_closure 