--- a/src/HOLCF/Cfun2.ML Thu May 31 16:50:16 2001 +0200
+++ b/src/HOLCF/Cfun2.ML Thu May 31 16:50:17 2001 +0200
@@ -93,6 +93,13 @@
bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
(* ?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;
+qed "chain_monofun";
+
+
(* ------------------------------------------------------------------------ *)
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *)
(* ------------------------------------------------------------------------ *)