Fri, 16 Dec 1994 13:43:01 +0100 moved congruence rule conj_cong2 to FOL/IFOL.ML
lcp [Fri, 16 Dec 1994 13:43:01 +0100] rev 794
moved congruence rule conj_cong2 to FOL/IFOL.ML
Fri, 16 Dec 1994 13:30:34 +0100 conj_cong2: new congruence rule
lcp [Fri, 16 Dec 1994 13:30:34 +0100] rev 793
conj_cong2: new congruence rule
Thu, 15 Dec 1994 11:50:53 +0100 case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted
lcp [Thu, 15 Dec 1994 11:50:53 +0100] rev 792
case_ss: now built upon ZF/Order/bij_inverse_ss. Deleted own bij_inverse_ss and replaces uses by case_ss
Thu, 15 Dec 1994 11:17:49 +0100 updated comment;
lcp [Thu, 15 Dec 1994 11:17:49 +0100] rev 791
updated comment; renamed converse_of_Un to converse_Un
Thu, 15 Dec 1994 11:08:22 +0100 qconverse_qconverse, qconverse_prod: renamed from
lcp [Thu, 15 Dec 1994 11:08:22 +0100] rev 790
qconverse_qconverse, qconverse_prod: renamed from qconverse_of_qconverse, qconverse_of_prod
Wed, 14 Dec 1994 17:24:23 +0100 well_ord_iso_predE replaces not_well_ord_iso_pred
lcp [Wed, 14 Dec 1994 17:24:23 +0100] rev 789
well_ord_iso_predE replaces not_well_ord_iso_pred well_ord_iso_unique: eliminated a premise using well_ord_ord_iso Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred, part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso, well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans, mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map, ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset, domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy deleted bij_ss in favour of bij_inverse_ss
Wed, 14 Dec 1994 17:15:54 +0100 Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of
lcp [Wed, 14 Dec 1994 17:15:54 +0100] rev 788
Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of not_well_ord_iso_pred
Wed, 14 Dec 1994 16:57:55 +0100 converse_UN, Diff_eq_0_iff: new
lcp [Wed, 14 Dec 1994 16:57:55 +0100] rev 787
converse_UN, Diff_eq_0_iff: new
Wed, 14 Dec 1994 16:54:13 +0100 added constants mono_map, ord_iso_map
lcp [Wed, 14 Dec 1994 16:54:13 +0100] rev 786
added constants mono_map, ord_iso_map
Wed, 14 Dec 1994 16:51:16 +0100 cardinal_UN_Ord_lt_csucc: added comment
lcp [Wed, 14 Dec 1994 16:51:16 +0100] rev 785
cardinal_UN_Ord_lt_csucc: added comment le_UN_Ord_lt_csucc: tided proof by proving the lemma inj_UN_subset
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip