Tue, 07 Nov 2000 18:38:24 +0100 | paulson | better discussion of rule induction | changeset | files |
Tue, 07 Nov 2000 17:55:04 +0100 | berghofe | Thm.dest_abs now takes an additional argument. | changeset | files |
Tue, 07 Nov 2000 17:53:12 +0100 | berghofe | Moved rewriting functions from Thm to MetaSimplifier. | changeset | files |