src/ZF/Perm.ML
1997-02-28 paulson 1997-02-28 rule_by_tactic no longer standardizes its result
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-08 paulson 1997-01-08 Removal of sum_cs and eq_cs
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-06-07 paulson 1996-06-07 Addition of converse_iff, domain_converse, range_converse as rewrites
1996-06-04 paulson 1996-06-04 Tidied some proofs
1996-06-03 paulson 1996-06-03 Shortened a proof
1996-05-01 paulson 1996-05-01 New lemma inspired by KG
1996-03-26 paulson 1996-03-26 Updated comments
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-09-05 paulson 1995-09-05 Removed duplicate copy of converse_Un
1995-01-13 lcp 1995-01-13 Proved comp_lam.
1994-12-23 lcp 1994-12-23 inj_apply_equality: new
1994-12-15 lcp 1994-12-15 updated comment; renamed converse_of_Un to converse_Un
1994-12-14 clasohm 1994-12-14 added bind_thm for theorems defined by "standard ..."
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-11-24 lcp 1994-11-24 moved version of Cantors theorem to ZF/Perm.ML
1994-11-03 lcp 1994-11-03 ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E ZF/Perm/comp_fun: tidied; removed use of PiI
1994-08-12 lcp 1994-08-12 for infinite datatypes with arbitrary index sets
1994-08-01 lcp 1994-08-01 ZF/Perm.ML/inj_converse_inj, comp_inj: simpler proofs using f_imp_injective many other tidies
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-06-23 lcp 1994-06-23 modifications for cardinal arithmetic
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1994-01-07 lcp 1994-01-07 ZF/perm/image_comp: new
1993-10-07 lcp 1993-10-07 added ~: for "not in"
1993-09-17 lcp 1993-09-17 Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
1993-09-16 clasohm 1993-09-16 Initial revision