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
Wed, 14 Dec 1994 16:48:36 +0100 conj_commute,disj_commute: new
lcp [Wed, 14 Dec 1994 16:48:36 +0100] rev 784
conj_commute,disj_commute: new
Wed, 14 Dec 1994 13:03:09 +0100 changed get_thm to search all parent theories if the theorem is not found
clasohm [Wed, 14 Dec 1994 13:03:09 +0100] rev 783
changed get_thm to search all parent theories if the theorem is not found in the current theory
Wed, 14 Dec 1994 11:41:49 +0100 added bind_thm for theorems defined by "standard ..."
clasohm [Wed, 14 Dec 1994 11:41:49 +0100] rev 782
added bind_thm for theorems defined by "standard ..."
Wed, 14 Dec 1994 10:26:30 +0100 added any, sprop to pure_types;
wenzelm [Wed, 14 Dec 1994 10:26:30 +0100] rev 781
added any, sprop to pure_types;
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip