| Wed, 14 Dec 1994 17:15:54 +0100 | lcp | Ord_iso_implies_eq_lemma: uses well_ord_iso_predE instead of | changeset | files |
| Wed, 14 Dec 1994 16:57:55 +0100 | lcp | converse_UN, Diff_eq_0_iff: new | changeset | files |
| Wed, 14 Dec 1994 16:54:13 +0100 | lcp | added constants mono_map, ord_iso_map | changeset | files |
| Wed, 14 Dec 1994 16:51:16 +0100 | lcp | cardinal_UN_Ord_lt_csucc: added comment | changeset | files |
| Wed, 14 Dec 1994 16:48:36 +0100 | lcp | conj_commute,disj_commute: new | changeset | files |
| Wed, 14 Dec 1994 13:03:09 +0100 | clasohm | changed get_thm to search all parent theories if the theorem is not found | changeset | files |
| Wed, 14 Dec 1994 11:41:49 +0100 | clasohm | added bind_thm for theorems defined by "standard ..." | changeset | files |