| Thu, 12 Jan 1995 03:04:10 +0100 | lcp | Proved case_cong and case_case. | changeset | files |
| Thu, 12 Jan 1995 03:03:45 +0100 | lcp | Renamed single_fun to singleton_fun. | changeset | files |
| Thu, 12 Jan 1995 03:03:25 +0100 | lcp | Now also depends upon equalities.thy, allowing use of the | changeset | files |
| Thu, 12 Jan 1995 03:03:07 +0100 | lcp | Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps | changeset | files |
| Thu, 12 Jan 1995 03:02:34 +0100 | lcp | Removed spurious comment about eq_cs | changeset | files |
| Thu, 12 Jan 1995 03:02:05 +0100 | lcp | Moved theorems Ord_cases_lemma and Ord_cases to Ordinal.ML | changeset | files |
| Thu, 12 Jan 1995 03:01:40 +0100 | lcp | Now depends upon Bool, so that 1 and 2 are defined | changeset | files |