| Wed, 21 Jul 1999 15:23:18 +0200 | paulson | removed 2 qed_goals | changeset | files |
| Wed, 21 Jul 1999 15:22:11 +0200 | paulson | tweaked proofs to handle new freeness reasoning for data c onstructors | changeset | files |
| Wed, 21 Jul 1999 15:20:26 +0200 | paulson | more existing theorems renamed to use #0; also new results | changeset | files |
| Wed, 21 Jul 1999 15:18:36 +0200 | paulson | now exports mk_bin | changeset | files |
| Wed, 21 Jul 1999 15:17:54 +0200 | paulson | a more robust proof | changeset | files |
| Wed, 21 Jul 1999 15:17:30 +0200 | paulson | tweaked proof after removal of diff_is_0_eq RS iffD2 | changeset | files |
| Wed, 21 Jul 1999 15:16:32 +0200 | paulson | better error message for curried recdefs, etc. | changeset | files |