summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

edits.txt

author | paulson |

Fri Feb 16 17:24:51 1996 +0100 (1996-02-16) | |

changeset 1511 | 09354d37a5ab |

parent 0 | a5a9c433f639 |

permissions | -rw-r--r-- |

Elimination of fully-functorial style.

Type tactic changed to a type abbrevation (from a datatype).

Constructor tactic and function apply deleted.

Type tactic changed to a type abbrevation (from a datatype).

Constructor tactic and function apply deleted.

1 EDITS TO THE ISABELLE SYSTEM FOR 1993

3 11 January

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

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

9 14 January

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

12 prints conditions correctly.

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

15 add_mult_dist, to agree with the other _distrib rules

17 20 January

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

22 21 January

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

26 22 January

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

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

34 25 January

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

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

40 27 January

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

44 27 January

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

47 (ZF took almost 5 hours!)

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

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

55 29 January

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

62 2 February

64 MAKE-ALL (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.

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

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

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

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

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

77 3 February

79 MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.

81 4 February

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

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();

95 8 February

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

101 9 February

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

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

106 11 February

108 HOL/arith: eliminated redefinitions of nat_ss and arith_ss

110 12 February

112 MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.

114 Pure/Thy/scan/string: now correctly recognizes ML-style strings.

116 15 February

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

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

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

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

124 18 February

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

127 it was unused.

129 Pure/Syntax/earley0A: modified accordingly.

131 19 February

133 MAKE-ALL (NJ 0.75) ran perfectly. It took 3:37 hours

134 MAKE-ALL (Poly/ML) ran perfectly. It took 2:52 hours

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

138 20 February

140 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:30 hours

142 10 March

144 HOL/fun/image_eqI: fixed bad pattern

146 11 March

148 MAKE-ALL (Poly/ML) failed in HOL!

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

151 of Int and Un.

153 12 March

155 ZF/ex/misc: new example from Bledsoe

157 15 March

159 ZF/perm: two new theorems inspired by Pastre

161 16 March

163 Weakened congruence rules for HOL: speeds simplification considerably by

164 NOT simplifying the body of a conditional or eliminator.

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

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

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

171 operators < and <=

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

178 HOL & test rebuilt perfectly

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

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

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

184 definitions do not update the proof state.

186 17 March

188 MAKE-ALL (Poly/ML) ran perfectly.

190 18 March

192 MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions

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

195 necessary

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

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

201 Pure/library/gen_ins,gen_union: new

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

205 18 March

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

208 ex/Subst/alist

210 HOL/list/list_congs: new; re-organized simpsets a bit

212 Pure/goals/sign_error: new

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

215 the signature of the proof state changes

217 HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing

218 the library functions fst, snd

220 HOL/fun/image_compose: new

222 21 March

224 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:50 hours

225 MAKE-ALL (Poly/ML) ran perfectly. It took 3:21 hours

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

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

230 ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing

231 the library functions fst, snd

233 HOL/prod/prod_fun_imageI,E: new

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

236 of Pure

238 24 March

240 HOL/trancl/comp_subset_Sigma: new

241 HOL/wf/wfI: new

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

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

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

248 HOL/gfp,llist: new

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

251 Sexp is now the set of all well-founded 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 well-founded trees.

257 25 March

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

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

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:

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();

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

272 goal Set.thy "True = False";

273 brs rls 1; br singletonI 1;

274 result();

276 Marcus Moore noted that the error only occurred with

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

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

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

281 Vars in tpairs.

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

284 to newAs.

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

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

289 def_Tarski to def_lfp_Tarski

291 26 March

293 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:25 hours!

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

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

297 Pure/library, and these versions used non-Standard string comparisons!

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.

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

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

309 MAKE-ALL on this directory ran perfectly

310 /usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version

312 29 March

314 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:14 hours!

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

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

319 30 March

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.

324 8 April

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

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

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

332 Pure/pattern.ML: new, pattern unification

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

336 Pure/library.ML: added predicate downto0

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

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

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

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

346 9 April

348 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:05 hours!

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

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

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

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

360 *Affected files (those mentioning compat_resolve_tac)

361 Pure/tactic.ML

362 Provers/typedsimp.ML

363 CTT/ctt.ML

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

370 Pure/goals/compat_goal: DELETED

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

373 delete_thm,head_string: DELETED

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

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

381 Provers/simp: replaced by new version

383 Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and

384 updated comments

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

389 CTT tested

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

393 FOL tested

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

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

399 typechk_tac now respects this ordering!

401 ZF tested

403 DOCUMENTATION

405 Logics/CTT: Removed mention of compat_resolve_tac

406 Ref/goals: deleted compat_goal's entry

408 Provers/hypsubst/lasthyp_subst_tac: deleted

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

412 12 April

414 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:03 hours!

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

417 FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac

418 FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac

419 FOLP/{int-prover,classical}/step_tac: calls inst_step_tac

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

422 used explicitly!!

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

426 FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call

427 uniq_assume_tac

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

431 13 April

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

435 Unification bug (nothing to do with pattern unification)

436 Cleaning of flex-flex 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!

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

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

444 14 April

446 MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK

448 LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex

449 changes

451 Pure/goals/gethyps: now calls METAHYPS directly

453 rm-logfiles: 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

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

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

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

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.

468 ZF: tested with new version

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

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

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);

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

480 METAHYPS version work

482 ZF/arith/add_not_less_self: adds anti_refl_rew

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

485 Swapping the premises of UN_I would probably allow instantiation.

487 ZF otherwise seems to work!

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

491 HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in

492 (CCONTR_rule RS allI)

494 *** REJECTED

496 15 April

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.

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

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

505 ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down

506 discrimination nets (and this rewrite used only ONCE)

508 ZF/mem_not_refl: new; replaces obsolete anti_refl_rew

510 **Timing experiments**

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

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.

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 object-logics.

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

526 only one subgoal.

528 19 April

530 MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.

531 MAKE-ALL (Poly/ML) ran perfectly. It took 3:23 hours

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

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

536 to the auto_tac.

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

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

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

546 20 April

548 MAKE-ALL failed in HOL/Subst

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";

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

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

560 21 April

562 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:44 hours

563 MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space

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

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

568 reduces their space by more than 1/3

570 rm-logfiles: now deletes compressed log files.

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.

577 ZF: used the point above to simplify many proofs

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

580 22 April

582 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:52 hours??

583 MAKE-ALL (Poly/ML) ran perfectly. It took 3:16 hours

585 30 April

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

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

590 new derivations for "singleton"

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

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

596 4 May

598 MAKE-ALL (NJ 0.93) ran out of space in LK.

599 MAKE-ALL (Poly/ML) ran perfectly. It took 3:14 hours

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

602 write-protected

604 5 May

606 HOL/list/not_Cons_self: renamed from l_not_Cons_l

607 HOL/list/not_CONS_self: new

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

610 HOL/llist.ML: changed Lconst theorems

612 6 May

614 MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours

616 ** Installation of new HOL from Tobias **

618 HOL/ex/{finite,prop-log} 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

626 ** end Installation **

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

630 7 May

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

633 simplification now proves the subgoal.

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

637 ** Installation of new simplifier from Tobias **

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.

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.

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

648 MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours

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

651 DEPTH_SOLVE

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

655 HOL/hol.thy: declaration of NORM

656 HOL/simpdata: NORM_def supplied to SimpFun

658 10 May

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

662 11 May

664 HOL/prod/Prod_eq: renamed Pair_eq

665 HOL/ex/lex-prod: wf_lex_prod: simplified proof

667 HOL/fun/inj_eq: new

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

671 12 May

673 MAKE-ALL (NJ 0.93) ran out of space in HOL.

674 MAKE-ALL (Poly/ML) failed in HOL.

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

677 13 May

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

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.

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

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

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

693 not by integers. (Changed by Tobias)

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

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

701 Pure/tctical/print_sg,print_theory: new

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

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

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

707 depend on Drule and have sharing constraints.

709 14 May

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

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

714 Pure/POLY/install_pp_nj: a dummy version

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

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]

722 17 May

724 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:57 hours??

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

728 18 May

730 MAKE-ALL (Poly/ML) ran perfectly. It took 3:36 hours

732 19 May

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

735 complex assumptions

737 20 May

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

740 null and list_case.

742 1 June

744 MAKE-ALL (Poly/ML) ran perfectly. It took 3:39 hours

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

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

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.

754 ZF/ex/ramsey: modified calls to dres_inst_tac

756 2 June

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 non-writeable area.

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

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

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

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

768 Pure/NJ/commit: new dummy function

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

771 make-all: now builds FOLP also!

773 3 June

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

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

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

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

782 All object-logic 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.

786 4 June

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

789 takes Net as argument.

791 Pure/ROOT: now loads net before logic.

793 MAKE-ALL (Poly/ML) failed in ZF and HOL.

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

797 7 June

799 Pure/tactic/is_letdig: moved to library

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

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

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

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

806 INT x.B(x).

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

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

812 8 June

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

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

818 14 June

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

821 Using def_wfrec hides such errors!!

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

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

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

829 type.ML:

831 Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.

832 Added both functions to the signature.

834 sign.ML:

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

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

839 Added

841 val freeze_vars: term -> term

842 val thaw_vars: term -> term

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

845 Moved rewritec_bottom and rewritec_top to thm.ML.

846 Only bottom-up rewriting supported any longer.

848 thm.ML:

850 Added

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

858 val mark_prop_def: thm

859 val truepropI: thm

860 val trueprop_def: thm

862 (* bottom-up 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

868 Simplified concl_of: call to Logic.skip_flexpairs redundant.

870 drule.ML:

872 Added

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

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

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

890 val asm_rl: thm

891 val cut_rl: thm

892 val revcut_rl: thm

894 tactic.ML:

896 Added

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

904 Moved to drule.ML:

905 val asm_rl: thm

906 val cut_rl: thm

907 val revcut_rl: thm

909 goals.ML:

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

912 meta-thms is identity.

914 ** End of Toby's changes **

916 16 June

918 Pure/sign/typ_of,read_ctyp: new

919 Pure/logic/dest_flexpair: now exported

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

922 flexpair_abs_elim_list

924 HOL/equalities/image_empty,image_insert: new

925 HOL/ex/finite/Fin_imageI: new

927 Installed Martin Coen's CCL as new object-logic

929 17 June

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

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

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

940 specify -h 8000.

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

944 18 June

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

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

949 types, when exception TYPE is raised.

951 HOL/llist: some tidying

953 23 June

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

957 24 June

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

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

962 identifier in CCL.ML

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

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

968 25 June

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

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

973 HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation

975 HOL/llist/iterates_equality,lmap_lappend_distrib: tidied

977 28 June

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

980 name preservation

982 HOL/llist: co-induction rules applied with res_inst_tac to state the

983 bisimulation directly

985 2 July

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

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

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

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

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

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

999 CHANGES LOG OF Markus Wenzel (MMW)

1000 =======

1002 29-Jun-1993 MMW

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

1004 (should be 99% backwards compatible)

1006 Pure/Thy/ROOT.ML

1007 added keywords for "translations" section

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, ...)

1016 Pure/Thy/read.ML

1017 read_thy: added close_in

1018 added file_exists (not perfect)

1019 use_thy: now uses file_exists

1021 Pure/thm.ML

1022 added syn_of: theory -> syntax

1024 Pure/Makefile

1025 SYNTAX_FILES: added Syntax/ast.ML

1027 Pure/Syntax/pretty.ML

1028 added str_of: T -> string

1030 Pure/Syntax/ast.ML

1031 added this file

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.

1045 30-Jun-1993 MMW

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

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'

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

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

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

1075 30-Jun-1993, 05-Jul-1993 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?);

1084 Pure/NJ.ML

1085 removed dummy install_pp

1086 added make_pp, install_pp

1088 Pure/POLY.ML

1089 removed dummy install_pp_nj

1090 added make_pp

1092 Pure/ROOT.ML

1093 removed install_pp_nj stuff

1095 Pure/drule.ML

1096 added str_of_sg, str_of_theory, str_of_thm

1098 Pure/install_pp.ML

1099 added this file

1101 Pure/sign.ML

1102 added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp

1104 Pure/goals.ML

1105 added str_of_term, str_of_typ

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"'

1116 01-Jul-1993 MMW

1117 Misc small fixes

1119 CCL/ROOT.ML

1120 HOL/ROOT.ML

1121 added ".ML" suffix to some filenames

1123 HOL/ex/unsolved.ML

1124 replaced HOL_Rule.thy by HOL.thy

1126 Pure/NJ.ML

1127 quit was incorrectly int -> unit

1129 END MMW CHANGES

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

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

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

1139 9 July

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

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

1145 12 July

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

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

1150 22 July

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

1154 ZF: ** installation of inductive definitions **

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

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

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

1164 ZF/mono: new rules for implication

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

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

1169 ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML

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

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

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

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

1176 23 July

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

1179 porting.

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

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

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

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

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

1189 26 July

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

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

1194 field_of_prod:new

1196 ZF/domrange/field_subset: modified

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

1199 ZF/wf/wf_trancl: simplified proof

1201 ZF/equalities: new laws for field

1203 29 July

1205 ZF/trancl/trancl_induct: new

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

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

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

1211 polishing;

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'

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

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

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

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

1233 Cube/cube.thy

1234 removed necontext

1235 replaced fun_tr/tr' by ndependent_tr/dependent_tr'

1237 CTT/ctt.thy

1238 added translations rules for PROD and SUM

1239 removed dependent_tr

1240 removed definitions of ndependent_tr, dependent_tr'

1242 HOL/set.thy: replaced id by idt

1244 CCL/ROOT.ML: Logtic -> Logic

1246 CCL/set.thy

1247 added "translations" section

1248 removed "ML" section

1249 replaced id by idt

1251 CCL/types.thy

1252 added "translations" section

1253 removed definitions of ndependent_tr, dependent_tr'

1254 replaced id by idt

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

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

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

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

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

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

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

1270 Minor changes and additions;

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

1274 Pure/library.ML

1275 added quote: string -> string

1276 added to_lower: string -> bool

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

1280 30 July

1282 MAKE-ALL (Poly/ML) ran perfectly.

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

1285 Pure/goals/prove_goalw: displays exceptions using print_sign_exn

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

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

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

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

1298 Pure/term/subst_free: new

1300 Pure/tactic/is_fact: newly exported

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

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

1305 forall is_letdig

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

1309 2 August

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

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

1314 Pure/drule/triv_forall_equality: new

1315 Pure/tactic/prune_params_tac: new

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

1319 3 August

1321 Pure/tactic/rule_by_tactic: new

1323 ZF/perm/compEpair: now proved via rule_by_tactic

1325 ZF/extend_ind/cases,mk_cases: new

1326 ZF/datatype/mk_free: new

1327 ZF/list: now calls List.mk_cases

1329 4 August

1331 Provers/slow_tac,slow_best_tac: new

1333 5 August

1335 MAKE-ALL (Poly/ML) failed in ZF

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

1341 6 August

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

1344 prints them!

1346 ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from

1347 Transset_Union, Transset_Inter

1349 ZF/ordinal/Transset_Union: new

1350 ZF/univ/pair_in_univ: renamed Pair_in_univ

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

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

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

1357 ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML

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

1361 9 August

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

1364 Syntax/sextension.

1366 11 August

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

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