# HG changeset patch
# User slotosch
# Date 902917040 -7200
# Node ID 5706f0ef1d43102ae7f008fb4c3e6103d078adf1
# Parent  b755c7240348914ed845e0fa7a7381e73c5a3984
eliminated fabs,fapp.
changed all theorem names and functions into Rep_CFun, Abs_CFun

diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun1.ML
--- a/src/HOLCF/Cfun1.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Cfun1.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -9,22 +9,22 @@
 open Cfun1;
 
 (* ------------------------------------------------------------------------ *)
-(* derive old type definition rules for fabs & fapp                         *)
-(* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
+(* derive old type definition rules for Abs_CFun & Rep_CFun                         *)
+(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future      *)
 (* ------------------------------------------------------------------------ *)
-qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun"
+qed_goal "Rep_Cfun" thy "Rep_CFun fo : CFun"
 (fn prems =>
         [
         (rtac Rep_CFun 1)
         ]);
 
-qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo"
+qed_goal "Rep_Cfun_inverse" thy "Abs_CFun (Rep_CFun fo) = fo"
 (fn prems =>
         [
         (rtac Rep_CFun_inverse 1)
         ]);
 
-qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f"
+qed_goal "Abs_Cfun_inverse" thy "f:CFun==>Rep_CFun(Abs_CFun f)=f"
 (fn prems =>
         [
 	(cut_facts_tac prems 1),
@@ -97,7 +97,7 @@
 (* additional lemma about the isomorphism between -> and Cfun               *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f"
+qed_goal "Abs_Cfun_inverse2" thy "cont f ==> Rep_CFun (Abs_CFun f) = f"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -110,7 +110,7 @@
 (* simplification of application                                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x"
+qed_goal "Cfunapp2" thy "cont f ==> (Abs_CFun f)`x = f x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun1.thy
--- a/src/HOLCF/Cfun1.thy	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Cfun1.thy	Wed Aug 12 12:17:20 1998 +0200
@@ -16,12 +16,10 @@
 (* to make << defineable *)
 instance "->"  :: (cpo,cpo)sq_ord
 
-consts  
-        fapp      :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
-					        (* usually Rep_Cfun *)
+syntax
+	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
                                                 (* application      *)
-        fabs      :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
-                                                (* usually Abs_Cfun *)
+        Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
                                                 (* abstraction      *)
         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
 
@@ -30,9 +28,6 @@
   "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
 					("(3\\<Lambda>_./ _)" [0, 10] 10)
 defs 
-  fabs_def	"fabs==Abs_CFun"
-  fapp_def	"fapp==Rep_CFun"
-
-  less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )"
+  less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
 
 end
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Cfun2.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -9,7 +9,7 @@
 open Cfun2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
+qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"
  (fn prems => 
         [
 	(fold_goals_tac [less_cfun_def]),
@@ -20,7 +20,7 @@
 (* access to less_cfun in class po                                          *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
+qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))"
 (fn prems =>
         [
         (simp_tac (simpset() addsimps [inst_cfun_po]) 1)
@@ -30,7 +30,7 @@
 (* Type 'a ->'b  is pointed                                                 *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
+qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f"
 (fn prems =>
         [
         (stac less_cfun 1),
@@ -44,17 +44,17 @@
 qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
 (fn prems =>
         [
-        (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
+        (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1),
         (rtac (minimal_cfun RS allI) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
-(* fapp yields continuous functions in 'a => 'b                             *)
-(* this is continuity of fapp in its 'second' argument                      *)
-(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
+(* Rep_CFun yields continuous functions in 'a => 'b                             *)
+(* this is continuity of Rep_CFun in its 'second' argument                      *)
+(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "cont_fapp2" thy "cont(fapp(fo))"
+qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))"
 (fn prems =>
         [
         (res_inst_tac [("P","cont")] CollectD 1),
@@ -62,30 +62,30 @@
         (rtac Rep_Cfun 1)
         ]);
 
-bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
-(* monofun(fapp(?fo1)) *)
+bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
+(* monofun(Rep_CFun(?fo1)) *)
 
 
-bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
-(* contlub(fapp(?fo1)) *)
+bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub);
+(* contlub(Rep_CFun(?fo1)) *)
 
 (* ------------------------------------------------------------------------ *)
-(* expanded thms cont_fapp2, contlub_fapp2                                 *)
+(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2                                 *)
 (* looks nice with mixfix syntac                                            *)
 (* ------------------------------------------------------------------------ *)
 
-bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
+bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
 (* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
  
-bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
+bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
 (* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
 
 
 (* ------------------------------------------------------------------------ *)
-(* fapp is monotone in its 'first' argument                                 *)
+(* Rep_CFun is monotone in its 'first' argument                                 *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)"
+qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)"
 (fn prems =>
         [
         (strip_tac 1),
@@ -94,7 +94,7 @@
 
 
 (* ------------------------------------------------------------------------ *)
-(* monotonicity of application fapp in mixfix syntax [_]_                   *)
+(* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "monofun_cfun_fun" thy  "f1 << f2 ==> f1`x << f2`x"
@@ -103,15 +103,15 @@
         (cut_facts_tac prems 1),
         (res_inst_tac [("x","x")] spec 1),
         (rtac (less_fun RS subst) 1),
-        (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
+        (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1)
         ]);
 
 
-bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
+bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
 (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
 
 (* ------------------------------------------------------------------------ *)
-(* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
+(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "monofun_cfun" thy
@@ -137,16 +137,16 @@
 (* use MF2 lemmas from Cont.ML                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "ch2ch_fappR" thy 
+qed_goal "ch2ch_Rep_CFunR" thy 
  "chain(Y) ==> chain(%i. f`(Y i))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (etac (monofun_fapp2 RS ch2ch_MF2R) 1)
+        (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1)
         ]);
 
 
-bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
+bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
 (* chain(?F) ==> chain (%i. ?F i`?x)                                  *)
 
 
@@ -161,8 +161,8 @@
         [
         (cut_facts_tac prems 1),
         (rtac lub_MF2_mono 1),
-        (rtac monofun_fapp1 1),
-        (rtac (monofun_fapp2 RS allI) 1),
+        (rtac monofun_Rep_CFun1 1),
+        (rtac (monofun_Rep_CFun2 RS allI) 1),
         (atac 1)
         ]);
 
@@ -179,8 +179,8 @@
         [
         (cut_facts_tac prems 1),
         (rtac ex_lubMF2 1),
-        (rtac monofun_fapp1 1),
-        (rtac (monofun_fapp2 RS allI) 1),
+        (rtac monofun_Rep_CFun1 1),
+        (rtac (monofun_Rep_CFun2 RS allI) 1),
         (atac 1),
         (atac 1)
         ]);
@@ -221,14 +221,14 @@
         (stac Abs_Cfun_inverse2 1),
         (etac cont_lubcfun 1),
         (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
-        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
+        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
         (strip_tac 1),
         (stac less_cfun 1),
         (stac Abs_Cfun_inverse2 1),
         (etac cont_lubcfun 1),
         (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
-        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
-        (etac (monofun_fapp1 RS ub2ub_monofun) 1)
+        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
+        (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1)
         ]);
 
 bind_thm ("thelub_cfun", lub_cfun RS thelubI);
@@ -255,17 +255,17 @@
         [
         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
-        (res_inst_tac [("f","fabs")] arg_cong 1),
+        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
         (rtac ext 1),
         (resolve_tac prems 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
-(* Monotonicity of fabs                                                     *)
+(* Monotonicity of Abs_CFun                                                     *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "semi_monofun_fabs" thy 
-        "[|cont(f);cont(g);f<<g|]==>fabs(f)<<fabs(g)"
+qed_goal "semi_monofun_Abs_CFun" thy 
+        "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
  (fn prems =>
         [
         (rtac (less_cfun RS iffD2) 1),
@@ -285,9 +285,9 @@
         [
         (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
         (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
-        (rtac semi_monofun_fabs 1),
-        (rtac cont_fapp2 1),
-        (rtac cont_fapp2 1),
+        (rtac semi_monofun_Abs_CFun 1),
+        (rtac cont_Rep_CFun2 1),
+        (rtac cont_Rep_CFun2 1),
         (rtac (less_fun RS iffD2) 1),
         (rtac allI 1),
         (resolve_tac prems 1)
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Cfun3.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -7,17 +7,17 @@
 open Cfun3;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x. UU)"
+qed_goal "inst_cfun_pcpo" thy "UU = Abs_CFun(%x. UU)"
  (fn prems => 
         [
         (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
         ]);
 
 (* ------------------------------------------------------------------------ *)
-(* the contlub property for fapp its 'first' argument                       *)
+(* the contlub property for Rep_CFun its 'first' argument                       *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "contlub_fapp1" thy "contlub(fapp)"
+qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)"
 (fn prems =>
         [
         (rtac contlubI 1),
@@ -29,26 +29,26 @@
         (stac Cfunapp2 1),
         (etac cont_lubcfun 1),
         (stac thelub_fun 1),
-        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
+        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
         (rtac refl 1)
         ]);
 
 
 (* ------------------------------------------------------------------------ *)
-(* the cont property for fapp in its first argument                        *)
+(* the cont property for Rep_CFun in its first argument                        *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "cont_fapp1" thy "cont(fapp)"
+qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
-        (rtac monofun_fapp1 1),
-        (rtac contlub_fapp1 1)
+        (rtac monofun_Rep_CFun1 1),
+        (rtac contlub_Rep_CFun1 1)
         ]);
 
 
 (* ------------------------------------------------------------------------ *)
-(* contlub, cont properties of fapp in its first argument in mixfix _[_]   *)
+(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_]   *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_cfun_fun" thy 
@@ -58,9 +58,9 @@
         [
         (cut_facts_tac prems 1),
         (rtac trans 1),
-        (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1),
+        (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1),
         (stac thelub_fun 1),
-        (etac (monofun_fapp1 RS ch2ch_monofun) 1),
+        (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
         (rtac refl 1)
         ]);
 
@@ -72,13 +72,13 @@
         [
         (cut_facts_tac prems 1),
         (rtac thelubE 1),
-        (etac ch2ch_fappL 1),
+        (etac ch2ch_Rep_CFunL 1),
         (etac (contlub_cfun_fun RS sym) 1)
         ]);
 
 
 (* ------------------------------------------------------------------------ *)
-(* contlub, cont  properties of fapp in both argument in mixfix _[_]       *)
+(* contlub, cont  properties of Rep_CFun in both argument in mixfix _[_]       *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_cfun" thy 
@@ -88,9 +88,9 @@
         [
         (cut_facts_tac prems 1),
         (rtac contlub_CF2 1),
-        (rtac cont_fapp1 1),
+        (rtac cont_Rep_CFun1 1),
         (rtac allI 1),
-        (rtac cont_fapp2 1),
+        (rtac cont_Rep_CFun2 1),
         (atac 1),
         (atac 1)
         ]);
@@ -102,9 +102,9 @@
         [
         (cut_facts_tac prems 1),
         (rtac thelubE 1),
-        (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
+        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
         (rtac allI 1),
-        (rtac monofun_fapp2 1),
+        (rtac monofun_Rep_CFun2 1),
         (atac 1),
         (atac 1),
         (etac (contlub_cfun RS sym) 1),
@@ -113,10 +113,10 @@
 
 
 (* ------------------------------------------------------------------------ *)
-(* cont2cont lemma for fapp                                               *)
+(* cont2cont lemma for Rep_CFun                                               *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "cont2cont_fapp" thy 
+qed_goal "cont2cont_Rep_CFun" thy 
         "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
  (fn prems =>
         [
@@ -124,9 +124,9 @@
         (rtac cont2cont_app2 1),
         (rtac cont2cont_app2 1),
         (rtac cont_const 1),
-        (rtac cont_fapp1 1),
+        (rtac cont_Rep_CFun1 1),
         (atac 1),
-        (rtac cont_fapp2 1),
+        (rtac cont_Rep_CFun2 1),
         (atac 1)
         ]);
 
@@ -169,7 +169,7 @@
         (rtac (p1 RS cont2mono_LAM RS ch2ch_monofun) 1),
         (rtac (p2 RS cont2mono) 1),
         (atac 1),
-        (res_inst_tac [("f","fabs")] arg_cong 1),
+        (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
         (rtac ext 1),
         (stac (p1 RS beta_cfun RS ext) 1),
         (etac (p2 RS cont2contlub RS contlubE RS spec RS mp) 1)
@@ -179,8 +179,8 @@
 (* cont2cont tactic                                                       *)
 (* ------------------------------------------------------------------------ *)
 
-val cont_lemmas1 = [cont_const, cont_id, cont_fapp2,
-                    cont2cont_fapp,cont2cont_LAM];
+val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
+                    cont2cont_Rep_CFun,cont2cont_LAM];
 
 Addsimps cont_lemmas1;
 
@@ -193,7 +193,7 @@
 (* function application _[_]  is strict in its first arguments              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "strict_fapp1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
+qed_goal "strict_Rep_CFun1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
  (fn prems =>
         [
         (stac inst_cfun_pcpo 1),
@@ -322,7 +322,7 @@
         (rtac (Istrictify2 RS sym) 1),
         (fast_tac HOL_cs 1),
         (rtac ch2ch_monofun 1),
-        (rtac monofun_fapp2 1),
+        (rtac monofun_Rep_CFun2 1),
         (atac 1),
         (rtac ch2ch_monofun 1),
         (rtac monofun_Istrictify2 1),
@@ -362,7 +362,7 @@
 (* Instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
+Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2];
 
 
 (* ------------------------------------------------------------------------ *)
@@ -376,7 +376,7 @@
 (* some lemmata for functions with flat/chfin domain/range types	    *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "chfin_fappR" thy 
+qed_goal "chfin_Rep_CFunR" thy 
     "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
 (fn prems => 
 	[
@@ -384,7 +384,7 @@
 	rtac allI 1,
 	stac contlub_cfun_fun 1,
 	 atac 1,
-	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
+	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_Rep_CFunL])1
 	]);
 
 (* ------------------------------------------------------------------------ *)
@@ -451,7 +451,7 @@
         (rtac exE 1),
         (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
         (etac spec 1),
-        (etac ch2ch_fappR 1),
+        (etac ch2ch_Rep_CFunR 1),
         (rtac exI 1),
         (strip_tac 1),
         (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Fix.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -65,13 +65,13 @@
         (rtac antisym_less 1),
         (rtac lub_mono 1),
         (rtac chain_iterate 1),
-        (rtac ch2ch_fappR 1),
+        (rtac ch2ch_Rep_CFunR 1),
         (rtac chain_iterate 1),
         (rtac allI 1),
         (rtac (iterate_Suc RS subst) 1),
         (rtac (chain_iterate RS chainE RS spec) 1),
         (rtac is_lub_thelub 1),
-        (rtac ch2ch_fappR 1),
+        (rtac ch2ch_Rep_CFunR 1),
         (rtac chain_iterate 1),
         (rtac ub_rangeI 1),
         (rtac allI 1),
@@ -120,7 +120,7 @@
 (* ------------------------------------------------------------------------ *)
 (* the following lemma uses contlub_cfun which itself is based on a         *)
 (* diagonalisation lemma for continuous functions with two arguments.       *)
-(* In this special case it is the application function fapp                 *)
+(* In this special case it is the application function Rep_CFun                 *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "contlub_iterate" thy  [contlub] "contlub(iterate(i))"
@@ -138,9 +138,9 @@
         (rtac (less_fun RS iffD2) 1),
         (rtac allI 1),
         (rtac (chainE RS spec) 1),
-        (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1),
+        (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
         (rtac allI 1),
-        (rtac monofun_fapp2 1),
+        (rtac monofun_Rep_CFun2 1),
         (atac 1),
         (rtac ch2ch_fun 1),
         (rtac (monofun_iterate RS ch2ch_monofun) 1),
@@ -547,7 +547,7 @@
 qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))"
     (fn _ => [
 	strip_tac 1,
-	dtac chfin_fappR 1,
+	dtac chfin_Rep_CFunR 1,
 	eres_inst_tac [("x","s")] allE 1,
 	fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]);
 
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -924,8 +924,8 @@
 by (stac contlub_cfun_fun 1);
 by (rtac chain_iterate 1);
 by (rtac lub_mono 1);
-by (rtac (chain_iterate RS ch2ch_fappL) 1);
-by (rtac (chain_iterate RS ch2ch_fappL) 1);
+by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
+by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1);
 by (rtac allI 1);
 by (resolve_tac prems 1);
 qed"take_lemma_less1";
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Lift.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -58,7 +58,7 @@
 
 val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg,
                        cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, 
-                       cont_fapp_app,cont_fapp_app_app,cont_if];
+                       cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if];
 
 val cont_lemmas2 =  cont_lemmas1 @ cont_lemmas_ext;
                  
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Lift3.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -143,13 +143,13 @@
 by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
 by Auto_tac;
-qed"cont_fapp_app";
+qed"cont_Rep_CFun_app";
 
 Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
 by (rtac cont2cont_CF1L 1);
-by (etac cont_fapp_app 1);
+by (etac cont_Rep_CFun_app 1);
 by (assume_tac 1);
-qed"cont_fapp_app_app";
+qed"cont_Rep_CFun_app_app";
 
 
 (* continuity of if then else *)
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Ssum3.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -262,7 +262,7 @@
         (atac 1),
         (fast_tac HOL_cs 1),
         (simp_tac (simpset_of Cfun3.thy) 1),
-        (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
+        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
         ]);
@@ -326,7 +326,7 @@
         (atac 1),
         (fast_tac HOL_cs 1),
         (simp_tac (simpset_of Cfun3.thy) 1),
-        (rtac (monofun_fapp2 RS ch2ch_monofun) 1),
+        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1),
         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
         (etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
         ]);
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/Up3.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -110,7 +110,7 @@
         (stac contlub_cfun_arg 1),
         (etac (monofun_Ifup2 RS ch2ch_monofun) 1),
         (rtac lub_equal2 1),
-        (rtac (monofun_fapp2 RS ch2ch_monofun) 2),
+        (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2),
         (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
         (etac (monofun_Ifup2 RS ch2ch_monofun) 2),
         (rtac (chain_mono2 RS exE) 1),
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/cont_consts.ML
--- a/src/HOLCF/cont_consts.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/cont_consts.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -35,7 +35,7 @@
   val vnames = argnames (ord "A") n;
   val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1);
   in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames),
-			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") 
+			  foldl (fn (t,arg) => (Ast.mk_appl (Constant "Rep_CFun") 
 						[t,Variable arg]))
 			  (Constant name1,vnames))]
      @(case mx of InfixlName _ => [extra_parse_rule] 
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/domain/axioms.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -57,14 +57,14 @@
 
   val dis_defs = let
 	fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == 
-		 mk_cfapp(%%(dname^"_when"),map 
+		 mk_cRep_CFun(%%(dname^"_when"),map 
 			(fn (con',args) => (foldr /\#
 			   (args,if con'=con then %%"TT" else %%"FF"))) cons))
 	in map ddef cons end;
 
   val sel_defs = let
 	fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == 
-		 mk_cfapp(%%(dname^"_when"),map 
+		 mk_cRep_CFun(%%(dname^"_when"),map 
 			(fn (con',args) => if con'<>con then %%"UU" else
 			 foldr /\# (args,Bound (length args - n))) cons));
 	in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
@@ -116,8 +116,8 @@
 	fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
 			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
 	val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
-	   Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1),
-	   Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2)));
+	   Bound(allargs_cnt+1)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns1),
+	   Bound(allargs_cnt+0)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns2)));
         in foldr mk_ex (allvns, foldr mk_conj 
 			      (map (defined o Bound) nonlazy_idxs,capps)) end;
       fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/domain/library.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -145,11 +145,11 @@
 infix 1 <<;  fun S <<  T = %%"op <<" $ S $ T;
 infix 1 ~<<; fun S ~<< T = mk_not (S << T);
 
-infix 9 `  ; fun f`  x = %%"fapp" $ f $ x;
+infix 9 `  ; fun f`  x = %%"Rep_CFun" $ f $ x;
 infix 9 `% ; fun f`% s = f` % s;
 infix 9 `%%; fun f`%%s = f` %%s;
-fun mk_cfapp (F,As) = foldl (op `) (F,As);
-fun con_app2 con f args = mk_cfapp(%%con,map f args);
+fun mk_cRep_CFun (F,As) = foldl (op `) (F,As);
+fun con_app2 con f args = mk_cRep_CFun(%%con,map f args);
 fun con_app con = con_app2 con %#;
 fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
 fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
@@ -166,7 +166,7 @@
 		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
 fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
-fun /\ v T = %%"fabs" $ mk_lam(v,T);
+fun /\ v T = %%"Abs_CFun" $ mk_lam(v,T);
 fun /\# (arg,T) = /\ (vname arg) T;
 infixr 9 oo; fun S oo T = %%"cfcomp"`S`T;
 val UU = %%"UU";
@@ -176,12 +176,12 @@
 fun lift_defined f = lift (fn x => defined (f x));
 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
 
-fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = 
+fun cont_eta_contract (Const("Abs_CFun",TT) $ Abs(a,T,body)) = 
       (case cont_eta_contract body  of
-        body' as (Const("fapp",Ta) $ f $ Bound 0) => 
+        body' as (Const("Rep_CFun",Ta) $ f $ Bound 0) => 
 	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
-	  else   Const("fabs",TT) $ Abs(a,T,body')
-      | body' => Const("fabs",TT) $ Abs(a,T,body'))
+	  else   Const("Abs_CFun",TT) $ Abs(a,T,body')
+      | body' => Const("Abs_CFun",TT) $ Abs(a,T,body'))
 |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
 |   cont_eta_contract t    = t;
 
@@ -197,7 +197,7 @@
 		in cont_eta_contract (foldr'' 
 			(fn (a,t) => %%"ssplit"`(/\# (a,t)))
 			(args,
-			fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args))))
+			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
 			) end;
 in (if length cons = 1 andalso length(snd(hd cons)) <= 1
     then fn t => %%"strictify"`t else Id)
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/domain/syntax.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -71,7 +71,7 @@
 					 (string_of_int m));
 	fun app s (l,r)   = mk_appl (Constant s) [l,r];
 	fun case1 n (con,mx,args) = mk_appl (Constant "@case1")
-		 [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)),
+		 [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)),
 		  expvar n];
 	fun arg1 n (con,_,args) = if args = [] then expvar n 
 				  else mk_appl (Constant "LAM ") 
@@ -81,8 +81,8 @@
       (mk_appl (Constant "@case") [Variable "x", foldr'
 				(fn (c,cs) => mk_appl (Constant"@case2") [c,cs])
 				 (mapn case1 1 cons')],
-       mk_appl (Constant "fapp") [foldl 
-				(fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ])
+       mk_appl (Constant "Rep_CFun") [foldl 
+				(fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ])
 				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
 				 Variable "x"])
   end;
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -41,7 +41,7 @@
                                 asm_simp_tac (HOLCF_ss addsimps rews) i;
 
 val chain_tac = REPEAT_DETERM o resolve_tac 
-                [chain_iterate, ch2ch_fappR, ch2ch_fappL];
+                [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL];
 
 (* ----- general proofs ----------------------------------------------------- *)
 
@@ -175,7 +175,7 @@
 val when_apps = let fun one_when n (con,args) = pg axs_con_def 
                 (bind_fun (lift_defined % (nonlazy args, 
                 mk_trp(when_app`(con_app con args) ===
-                       mk_cfapp(bound_fun n 0,map %# args)))))[
+                       mk_cRep_CFun(bound_fun n 0,map %# args)))))[
                 asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
         in mapn one_when 1 cons end;
 end;
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -262,7 +262,7 @@
         (rtac adm_eq 1),
         (cont_tacR 1),
         (rtac allI 1),
-        (stac strict_fapp1 1),
+        (stac strict_Rep_CFun1 1),
         (rtac refl 1),
         (Simp_tac 1),
         (rtac allI 1),
@@ -295,7 +295,7 @@
         (rtac adm_eq 1),
         (cont_tacR 1),
         (rtac allI 1),
-        (stac strict_fapp1 1),
+        (stac strict_Rep_CFun1 1),
         (rtac refl 1),
         (rtac allI 1),
         (Simp_tac 1),
@@ -336,7 +336,7 @@
         (rtac adm_eq 1),
         (cont_tacR 1),
         (rtac allI 1),
-        (stac strict_fapp1 1),
+        (stac strict_Rep_CFun1 1),
         (rtac refl 1),
         (rtac allI 1),
         (Simp_tac 1),
diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Mon Aug 10 17:06:02 1998 +0200
+++ b/src/HOLCF/ex/Stream.ML	Wed Aug 12 12:17:20 1998 +0200
@@ -77,7 +77,7 @@
 
 qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [
 	stream_case_tac "s" 1,
-	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews))
+	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews))
 	]);