| Mon, 26 May 1997 12:40:51 +0200 | paulson | Deleted option_case_tac because exhaust_tac performs a similar function. | changeset | files |
| Mon, 26 May 1997 12:39:57 +0200 | paulson | Renamed lessD to Suc_leI | changeset | files |
| Mon, 26 May 1997 12:38:29 +0200 | paulson | New operator "lists" for formalizing sets of lists | changeset | files |
| Mon, 26 May 1997 12:37:24 +0200 | paulson | New theorem subset_inj_onto | changeset | files |
| Mon, 26 May 1997 12:36:56 +0200 | paulson | Two results suggested by Florian Kammueller | changeset | files |
| Mon, 26 May 1997 12:36:16 +0200 | paulson | Tidying and a couple of useful lemmas | changeset | files |
| Mon, 26 May 1997 12:34:54 +0200 | paulson | Added recdef | changeset | files |
| Mon, 26 May 1997 12:34:05 +0200 | paulson | Primrec: New example ported from ZF | changeset | files |