Thu, 12 Jan 1995 10:53:42 +0100 lcp prove_fun now includes equalityI. Added the rewrite rules
Thu, 12 Jan 1995 10:39:47 +0100 lcp Proved sum_bij, sum_ord_iso_cong, prod_bij,
Thu, 12 Jan 1995 03:04:10 +0100 lcp Proved case_cong and case_case.
Thu, 12 Jan 1995 03:03:45 +0100 lcp Renamed single_fun to singleton_fun.
Thu, 12 Jan 1995 03:03:25 +0100 lcp Now also depends upon equalities.thy, allowing use of the
Thu, 12 Jan 1995 03:03:07 +0100 lcp Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
Thu, 12 Jan 1995 03:02:34 +0100 lcp Removed spurious comment about eq_cs
Thu, 12 Jan 1995 03:02:05 +0100 lcp Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML
Thu, 12 Jan 1995 03:01:40 +0100 lcp Now depends upon Bool, so that 1 and 2 are defined
Thu, 12 Jan 1995 03:01:20 +0100 lcp Moved theorems Ord_cases_lemma and Ord_cases here from Univ,
Thu, 12 Jan 1995 03:00:58 +0100 lcp Added constants Ord_alt, ++, **
Thu, 12 Jan 1995 03:00:38 +0100 lcp Proved equivalence of Ord and Ord_alt. Proved
Wed, 11 Jan 1995 18:47:03 +0100 lcp Proved ord_isoI, ord_iso_refl. Simplified proof of
Wed, 11 Jan 1995 18:42:06 +0100 lcp Proved cadd_cmult_distrib.
Wed, 11 Jan 1995 18:30:37 +0100 lcp Now proof of Ord_jump_cardinal uses
Wed, 11 Jan 1995 18:21:39 +0100 lcp Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
Wed, 11 Jan 1995 13:25:23 +0100 wenzelm pretty_gram: now sorts productions;
Wed, 11 Jan 1995 10:57:39 +0100 wenzelm removed print_sign, print_axioms;
Wed, 11 Jan 1995 10:53:22 +0100 wenzelm slightly changed OFCLASS syntax;
Mon, 02 Jan 1995 12:16:12 +0100 wenzelm fixed minor typos;
Mon, 02 Jan 1995 12:14:26 +0100 wenzelm added;
Fri, 23 Dec 1994 16:51:10 +0100 lcp RepFun_eq_0_iff, RepFun_0: new
Fri, 23 Dec 1994 16:50:22 +0100 lcp Moved Transset_includes_summands and Transset_sum_Int_subset
Fri, 23 Dec 1994 16:49:48 +0100 lcp Re-indented declarations; declared the number 2
Fri, 23 Dec 1994 16:35:42 +0100 lcp Added Krzysztof's theorems irrefl_converse, trans_on_converse,
Fri, 23 Dec 1994 16:35:08 +0100 lcp Added Krzysztof's theorems irrefl_rvimage, trans_on_rvimage,
Fri, 23 Dec 1994 16:34:27 +0100 lcp singleton_iff: new
Fri, 23 Dec 1994 16:33:37 +0100 lcp Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
Fri, 23 Dec 1994 16:32:39 +0100 lcp Added Krzysztof's constants lesspoll and Finite
Fri, 23 Dec 1994 16:32:02 +0100 lcp Added Krzysztof's theorem pred_Memrel
Fri, 23 Dec 1994 16:31:23 +0100 lcp Moved Transset_includes_summands and Transset_sum_Int_subset to
Fri, 23 Dec 1994 16:30:35 +0100 lcp natE0: deleted, since unused
Fri, 23 Dec 1994 16:29:53 +0100 lcp Changed succ(1) to 2 in in_VLimit, two_in_univ
Fri, 23 Dec 1994 16:29:04 +0100 lcp csquare_rel_def: renamed k to K
Fri, 23 Dec 1994 16:28:26 +0100 lcp inj_apply_equality: new
Fri, 23 Dec 1994 16:27:45 +0100 lcp Added Krzysztof's theorems subst_elem, not_emptyI, not_emptyE
Fri, 23 Dec 1994 16:27:07 +0100 lcp empty_fun: generalized from -> to Pi
Fri, 23 Dec 1994 16:26:34 +0100 lcp Changed succ(1) to 2 in cmult_2; Simplified proof of InfCard_is_Limit
Fri, 23 Dec 1994 16:25:45 +0100 lcp Added Krzysztof's theorems singleton_eq_iff, fst_type, snd_type
Fri, 23 Dec 1994 10:52:25 +0100 lcp Added Krzysztof's theorem disj_imp_disj
Wed, 21 Dec 1994 13:36:02 +0100 lcp Id: marker.
Wed, 21 Dec 1994 13:26:26 +0100 lcp Added comments and Id: marker.
Wed, 21 Dec 1994 13:10:39 +0100 lcp Added comments and Id: marker.
Wed, 21 Dec 1994 12:53:45 +0100 lcp Tools description, largely taken from ../README
Wed, 21 Dec 1994 12:46:52 +0100 lcp Moved description of tools to Tools/README
Tue, 20 Dec 1994 16:20:50 +0100 lcp ord_iso_rvimage: new
Tue, 20 Dec 1994 15:58:52 +0100 lcp Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
Tue, 20 Dec 1994 13:24:04 +0100 clasohm qed is a utility that makes ML files store the defined theories in Isabelle's
Tue, 20 Dec 1994 10:21:32 +0100 lcp Simplified proof of ord_iso_image_pred using bij_inverse_ss.
Tue, 20 Dec 1994 10:19:24 +0100 lcp Used bind_thm to store domain_rel_subset and range_rel_subset
Mon, 19 Dec 1994 15:30:30 +0100 lcp removed quotes around "Datatype",
Mon, 19 Dec 1994 15:22:42 +0100 lcp removed quotes around "Inductive"
Mon, 19 Dec 1994 15:17:29 +0100 lcp ran expandshort script
Mon, 19 Dec 1994 15:11:50 +0100 lcp ran expandshort script
Mon, 19 Dec 1994 13:24:58 +0100 lcp removed quotes around "Inductive"
Mon, 19 Dec 1994 13:18:54 +0100 lcp added true theory dependencies
Mon, 19 Dec 1994 13:01:30 +0100 lcp ran expandshort script
Fri, 16 Dec 1994 18:07:12 +0100 lcp changed useless "qed" calls for lemmas back to uses of "result",
Fri, 16 Dec 1994 17:46:02 +0100 lcp Defines ZF theory sections (inductive, datatype) at the start/
Fri, 16 Dec 1994 17:44:09 +0100 lcp Added Limit_csucc from CardinalArith
(0) -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip