| Thu, 03 Nov 1994 11:45:41 +0100 | lcp | Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE | changeset | files |
| Thu, 03 Nov 1994 08:34:53 +0100 | clasohm | added warning message | changeset | files |
| Wed, 02 Nov 1994 12:48:22 +0100 | lcp | Provers/classical: now takes theorem "classical" as argument, proves "swap" | changeset | files |
| Wed, 02 Nov 1994 12:44:03 +0100 | lcp | Provers/hypsubst: greatly simplified! No longer simulates a | changeset | files |
| Wed, 02 Nov 1994 10:45:14 +0100 | lcp | Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of | changeset | files |
| Wed, 02 Nov 1994 09:09:30 +0100 | nipkow | Modified pattern.ML to perform proper matching of Higher-Order Patterns. | changeset | files |