changeset 12484 | 7ad150f5fc10 |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
--- a/src/HOLCF/Cfun2.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/Cfun2.ML Wed Dec 12 20:37:31 2001 +0100 @@ -94,9 +94,9 @@ (* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1 *) Goal "chain Y ==> chain (%i. f\\<cdot>(Y i))"; -br chainI 1; -br monofun_cfun_arg 1; -be chainE 1; +by (rtac chainI 1); +by (rtac monofun_cfun_arg 1); +by (etac chainE 1); qed "chain_monofun";