# HG changeset patch
# User oheimb
# Date 991320617 -7200
# Node ID 100edbd42dba5df99522a7ff378077f5cb3e25fb
# Parent  34a9a9126c49baad1c1781452a1075a4941d221d
added chain_monofun

diff -r 34a9a9126c49 -r 100edbd42dba src/HOLCF/Cfun2.ML
--- 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 [_]_             *)
 (* ------------------------------------------------------------------------ *)