changeset 7848 | 6ddcc24038e1 |
parent 5851 | 15ce4c1c8313 |
--- a/doc-src/Tutorial/Datatype/tidproof.ML Wed Oct 13 15:18:15 1999 +0200 +++ b/doc-src/Tutorial/Datatype/tidproof.ML Wed Oct 13 15:41:24 1999 +0200 @@ -1,4 +1,4 @@ Goal "subst Var t = (t ::('a,'b)term) & \ \ substs Var ts = (ts::('a,'b)term list)"; -by(mutual_induct_tac ["t", "ts"] 1); +by(induct_tac "t ts" 1); by(Auto_tac);