src/ZF/Cardinal.ML
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 14 Apr 1995 11:24:10 +0200 lcp Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
Thu, 13 Apr 1995 11:30:57 +0200 lcp Proved lesspoll_succ_iff.
Wed, 11 Jan 1995 18:21:39 +0100 lcp Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
Fri, 23 Dec 1994 16:33:37 +0100 lcp Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
Fri, 16 Dec 1994 18:07:12 +0100 lcp changed useless "qed" calls for lemmas back to uses of "result",
Thu, 15 Dec 1994 11:50:53 +0100 lcp case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted
Wed, 14 Dec 1994 11:41:49 +0100 clasohm added bind_thm for theorems defined by "standard ..."
Thu, 08 Dec 1994 13:38:13 +0100 lcp Card_cardinal_le: new
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
Mon, 22 Aug 1994 11:11:17 +0200 lcp ZF/Cardinal: some results moved here from CardinalArith
Mon, 15 Aug 1994 18:11:00 +0200 lcp ZF/Cardinal/Card_Un: new
Tue, 26 Jul 1994 13:21:20 +0200 lcp Axiom of choice, cardinality results, etc.
Tue, 12 Jul 1994 18:05:03 +0200 lcp new cardinal arithmetic developments
Thu, 23 Jun 1994 17:38:12 +0200 lcp modifications for cardinal arithmetic
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
less more (0) tip