| Tue, 22 May 2001 15:15:16 +0200 | berghofe | Inductive characterization of wfrec combinator. | changeset | files |
| Tue, 22 May 2001 15:12:11 +0200 | berghofe | Transitive closure is now defined via "inductive". | changeset | files |
| Tue, 22 May 2001 15:11:43 +0200 | berghofe | Representing set for type nat is now defined via "inductive". | changeset | files |
| Tue, 22 May 2001 15:10:06 +0200 | berghofe | Inductive definitions are now introduced earlier in the theory hierarchy. | changeset | files |
| Tue, 22 May 2001 09:26:57 +0200 | paulson | nat_diff_split_asm, for the assumptions | changeset | files |
| Mon, 21 May 2001 14:53:30 +0200 | paulson | if_splits and split_if_asm | changeset | files |