| changeset 13454 | 01e2496dee05 |
| parent 12036 | 49f6c49454c2 |
| child 15188 | 9d57263faf9e |
--- a/src/HOLCF/ex/Dagstuhl.ML Mon Aug 05 14:30:06 2002 +0200 +++ b/src/HOLCF/ex/Dagstuhl.ML Mon Aug 05 14:32:56 2002 +0200 @@ -31,7 +31,7 @@ val prems = goal Dagstuhl.thy "YS = YYS"; by (resolve_tac stream.take_lemmas 1); -by (nat_ind_tac "n" 1); +by (induct_tac "n" 1); by (simp_tac (simpset() addsimps stream.rews) 1); by (stac YS_def2 1); by (stac YYS_def2 1);