| changeset 5851 | 15ce4c1c8313 |
| child 7848 | 6ddcc24038e1 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Tutorial/Datatype/abgoalfind.ML Thu Nov 12 16:45:40 1998 +0100 @@ -0,0 +1,4 @@ +Goal + "evala env (substa s a) = evala (%x. evala env (s x)) a & \ +\ evalb env (substb s b) = evalb (%x. evala env (s x)) b"; +by(mutual_induct_tac ["a","b"] 1);