| changeset 297 | 5ef75ff3baeb |
| parent 244 | 929fc2c63bd0 |
| child 892 | d0dc8d057929 |
--- a/src/HOLCF/ex/Coind.ML Thu Mar 24 13:25:12 1994 +0100 +++ b/src/HOLCF/ex/Coind.ML Thu Mar 24 13:36:34 1994 +0100 @@ -57,7 +57,7 @@ \ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]" (fn prems => [ - (res_inst_tac [("s","n")] dnat_ind2 1), + (res_inst_tac [("s","n")] dnat_ind 1), (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), (rtac trans 1),