# HG changeset patch
# User huffman
# Date 1288397728 25200
# Node ID 1dfdbd66093a176bc7b8aadedf28dd7f0fc5001a
# Parent  73d45866dbda28c28229c76e33e149e7685e287a
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun

diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -191,7 +191,7 @@
 lemma compact_cast_iff: "compact (cast\<cdot>d) \<longleftrightarrow> compact d"
 apply (rule iffI)
 apply (simp only: compact_def cast_below_cast [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 apply (erule compact_cast)
 done
 
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -13,28 +13,28 @@
 
 subsection {* Definition of continuous function type *}
 
-cpodef (CFun)  ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
+cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
 by (auto intro: cont_const adm_cont)
 
 type_notation (xsymbols)
   cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
 
 notation
-  Rep_CFun  ("(_$/_)" [999,1000] 999)
+  Rep_cfun  ("(_$/_)" [999,1000] 999)
 
 notation (xsymbols)
-  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
+  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 notation (HTML output)
-  Rep_CFun  ("(_\<cdot>/_)" [999,1000] 999)
+  Rep_cfun  ("(_\<cdot>/_)" [999,1000] 999)
 
 subsection {* Syntax for continuous lambda abstraction *}
 
 syntax "_cabs" :: "'a"
 
 parse_translation {*
-(* rewrite (_cabs x t) => (Abs_CFun (%x. t)) *)
-  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_CFun})];
+(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
+  [mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* To avoid eta-contraction of body: *}
@@ -50,7 +50,7 @@
           val (x,t') = atomic_abs_tr' abs';
         in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
 
-  in [(@{const_syntax Abs_CFun}, cabs_tr')] end;
+  in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
 *}
 
 text {* Syntax for nested abstractions *}
@@ -88,32 +88,32 @@
 
 text {* Dummy patterns for continuous abstraction *}
 translations
-  "\<Lambda> _. t" => "CONST Abs_CFun (\<lambda> _. t)"
+  "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
 
 subsection {* Continuous function space is pointed *}
 
-lemma UU_CFun: "\<bottom> \<in> CFun"
-by (simp add: CFun_def inst_fun_pcpo)
+lemma UU_cfun: "\<bottom> \<in> cfun"
+by (simp add: cfun_def inst_fun_pcpo)
 
 instance cfun :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
 
 instance cfun :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
 
-lemmas Rep_CFun_strict =
-  typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Rep_cfun_strict =
+  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
 
-lemmas Abs_CFun_strict =
-  typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
+lemmas Abs_cfun_strict =
+  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
 
 text {* function application is strict in its first argument *}
 
-lemma Rep_CFun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
-by (simp add: Rep_CFun_strict)
+lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
+by (simp add: Rep_cfun_strict)
 
 lemma LAM_strict [simp]: "(\<Lambda> x. \<bottom>) = \<bottom>"
-by (simp add: inst_fun_pcpo [symmetric] Abs_CFun_strict)
+by (simp add: inst_fun_pcpo [symmetric] Abs_cfun_strict)
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
@@ -123,11 +123,11 @@
 
 text {* Beta-equality for continuous functions *}
 
-lemma Abs_CFun_inverse2: "cont f \<Longrightarrow> Rep_CFun (Abs_CFun f) = f"
-by (simp add: Abs_CFun_inverse CFun_def)
+lemma Abs_cfun_inverse2: "cont f \<Longrightarrow> Rep_cfun (Abs_cfun f) = f"
+by (simp add: Abs_cfun_inverse cfun_def)
 
 lemma beta_cfun: "cont f \<Longrightarrow> (\<Lambda> x. f x)\<cdot>u = f u"
-by (simp add: Abs_CFun_inverse2)
+by (simp add: Abs_cfun_inverse2)
 
 text {* Beta-reduction simproc *}
 
@@ -144,7 +144,7 @@
   that would otherwise be caused by large continuity side conditions.
 *}
 
-simproc_setup beta_cfun_proc ("Abs_CFun f\<cdot>x") = {*
+simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
   fn phi => fn ss => fn ct =>
     let
       val dest = Thm.dest_comb;
@@ -160,12 +160,12 @@
 text {* Eta-equality for continuous functions *}
 
 lemma eta_cfun: "(\<Lambda> x. f\<cdot>x) = f"
-by (rule Rep_CFun_inverse)
+by (rule Rep_cfun_inverse)
 
 text {* Extensionality for continuous functions *}
 
 lemma cfun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
+by (simp add: Rep_cfun_inject [symmetric] fun_eq_iff)
 
 lemma cfun_eqI: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
 by (simp add: cfun_eq_iff)
@@ -173,7 +173,7 @@
 text {* Extensionality wrt. ordering for continuous functions *}
 
 lemma cfun_below_iff: "f \<sqsubseteq> g \<longleftrightarrow> (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)" 
-by (simp add: below_CFun_def fun_below_iff)
+by (simp add: below_cfun_def fun_below_iff)
 
 lemma cfun_belowI: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
 by (simp add: cfun_below_iff)
@@ -191,32 +191,32 @@
 
 subsection {* Continuity of application *}
 
-lemma cont_Rep_CFun1: "cont (\<lambda>f. f\<cdot>x)"
-by (rule cont_Rep_CFun [THEN cont2cont_fun])
+lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
+by (rule cont_Rep_cfun [THEN cont2cont_fun])
 
-lemma cont_Rep_CFun2: "cont (\<lambda>x. f\<cdot>x)"
-apply (cut_tac x=f in Rep_CFun)
-apply (simp add: CFun_def)
+lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
+apply (cut_tac x=f in Rep_cfun)
+apply (simp add: cfun_def)
 done
 
-lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono]
+lemmas monofun_Rep_cfun = cont_Rep_cfun [THEN cont2mono]
 
-lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard]
-lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun1 = cont_Rep_cfun1 [THEN cont2mono, standard]
+lemmas monofun_Rep_cfun2 = cont_Rep_cfun2 [THEN cont2mono, standard]
 
-text {* contlub, cont properties of @{term Rep_CFun} in each argument *}
+text {* contlub, cont properties of @{term Rep_cfun} in each argument *}
 
 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))"
-by (rule cont_Rep_CFun2 [THEN cont2contlubE])
+by (rule cont_Rep_cfun2 [THEN cont2contlubE])
 
 lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)"
-by (rule cont_Rep_CFun2 [THEN contE])
+by (rule cont_Rep_cfun2 [THEN contE])
 
 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)"
-by (rule cont_Rep_CFun1 [THEN cont2contlubE])
+by (rule cont_Rep_cfun1 [THEN cont2contlubE])
 
 lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x"
-by (rule cont_Rep_CFun1 [THEN contE])
+by (rule cont_Rep_cfun1 [THEN contE])
 
 text {* monotonicity of application *}
 
@@ -224,7 +224,7 @@
 by (simp add: cfun_below_iff)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
-by (rule monofun_Rep_CFun2 [THEN monofunE])
+by (rule monofun_Rep_cfun2 [THEN monofunE])
 
 lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
 by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
@@ -232,15 +232,15 @@
 text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
 
 lemma chain_monofun: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (erule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+by (erule monofun_Rep_cfun2 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
-by (rule monofun_Rep_CFun2 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunR: "chain Y \<Longrightarrow> chain (\<lambda>i. f\<cdot>(Y i))"
+by (rule monofun_Rep_cfun2 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
-by (rule monofun_Rep_CFun1 [THEN ch2ch_monofun])
+lemma ch2ch_Rep_cfunL: "chain F \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>x)"
+by (rule monofun_Rep_cfun1 [THEN ch2ch_monofun])
 
-lemma ch2ch_Rep_CFun [simp]:
+lemma ch2ch_Rep_cfun [simp]:
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> chain (\<lambda>i. (F i)\<cdot>(Y i))"
 by (simp add: chain_def monofun_cfun)
 
@@ -248,7 +248,7 @@
   "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
 by (simp add: chain_def cfun_below_iff)
 
-text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
+text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
 
 lemma contlub_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
@@ -257,15 +257,15 @@
 lemma cont_cfun: 
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
 apply (rule thelubE)
-apply (simp only: ch2ch_Rep_CFun)
+apply (simp only: ch2ch_Rep_cfun)
 apply (simp only: contlub_cfun)
 done
 
 lemma contlub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
-apply (simp add: thelub_CFun)
-apply (simp add: Abs_CFun_inverse2)
+apply (simp add: thelub_cfun)
+apply (simp add: Abs_cfun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
 
@@ -291,7 +291,7 @@
 
 subsection {* Continuity simplification procedure *}
 
-text {* cont2cont lemma for @{term Rep_CFun} *}
+text {* cont2cont lemma for @{term Rep_cfun} *}
 
 lemma cont2cont_APP [simp, cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
@@ -299,9 +299,9 @@
   shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
 proof -
   have 1: "\<And>y. cont (\<lambda>x. (f x)\<cdot>y)"
-    using cont_Rep_CFun1 f by (rule cont_compose)
+    using cont_Rep_cfun1 f by (rule cont_compose)
   show "cont (\<lambda>x. (f x)\<cdot>(t x))"
-    using t cont_Rep_CFun2 1 by (rule cont_apply)
+    using t cont_Rep_cfun2 1 by (rule cont_apply)
 qed
 
 text {*
@@ -334,9 +334,9 @@
   assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
   assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
   shows "cont (\<lambda>x. \<Lambda> y. f x y)"
-proof (rule cont_Abs_CFun)
+proof (rule cont_Abs_cfun)
   fix x
-  from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+  from f1 show "f x \<in> cfun" by (simp add: cfun_def)
   from f2 show "cont f" by (rule cont2cont_lambda)
 qed
 
@@ -356,24 +356,24 @@
 by (simp add: cont2cont_LAM)
 
 lemmas cont_lemmas1 =
-  cont_const cont_id cont_Rep_CFun2 cont2cont_APP cont2cont_LAM
+  cont_const cont_id cont_Rep_cfun2 cont2cont_APP cont2cont_LAM
 
 subsection {* Miscellaneous *}
 
-text {* Monotonicity of @{term Abs_CFun} *}
+text {* Monotonicity of @{term Abs_cfun} *}
 
-lemma semi_monofun_Abs_CFun:
-  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: below_CFun_def Abs_CFun_inverse2)
+lemma semi_monofun_Abs_cfun:
+  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_cfun f \<sqsubseteq> Abs_cfun g"
+by (simp add: below_cfun_def Abs_cfun_inverse2)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
-lemma chfin_Rep_CFunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
+lemma chfin_Rep_cfunR: "chain (Y::nat => 'a::cpo->'b::chfin)  
       ==> !s. ? n. (LUB i. Y i)$s = Y n$s"
 apply (rule allI)
 apply (subst contlub_cfun_fun)
 apply assumption
-apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_CFunL)
+apply (fast intro!: thelubI chfin lub_finch2 chfin2finch ch2ch_Rep_cfunL)
 done
 
 lemma adm_chfindom: "adm (\<lambda>(u::'a::cpo \<rightarrow> 'b::chfin). P(u\<cdot>s))"
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -265,7 +265,7 @@
 lemma compact_convex_unit_iff [simp]: "compact {x}\<natural> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_convex_unit)
 apply (simp only: compact_def convex_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_convex_plus [simp]:
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Deflation.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -207,7 +207,7 @@
 proof -
   assume "compact (e\<cdot>x)"
   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
-  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
   thus "compact x" by (rule compactI)
 qed
@@ -216,7 +216,7 @@
 proof -
   assume "compact x"
   hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
-  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
+  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
   hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
   thus "compact (e\<cdot>x)" by (rule compactI)
 qed
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Domain_Aux.thy
--- a/src/HOLCF/Domain_Aux.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Domain_Aux.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -83,7 +83,7 @@
 lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
 proof (unfold compact_def)
   assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
-  with cont_Rep_CFun2
+  with cont_Rep_cfun2
   have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
   then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
 qed
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Fixrec.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -222,11 +222,11 @@
 by simp
 
 lemma def_cont_fix_eq:
-  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
+  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
 by (simp, subst fix_eq, simp)
 
 lemma def_cont_fix_ind:
-  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
+  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
 by (simp add: fix_ind)
 
 text {* lemma for proving rewrite rules *}
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -901,8 +901,8 @@
 apply (rule_tac t="s1" in seq.reach [THEN subst])
 apply (rule_tac t="s2" in seq.reach [THEN subst])
 apply (rule lub_mono)
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
-apply (rule seq.chain_take [THEN ch2ch_Rep_CFunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
+apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
 apply (rule assms)
 done
 
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Library/Stream.thy
--- a/src/HOLCF/Library/Stream.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Library/Stream.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -921,7 +921,7 @@
 by (rule monofun_cfun_arg,simp)
 
 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
-by (rule cont2contlubE [OF cont_Rep_CFun2, symmetric])
+by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric])
 
 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==>
                         (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -256,7 +256,7 @@
 lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_lower_unit)
 apply (simp only: compact_def lower_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_lower_plus [simp]:
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Ssum.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -120,11 +120,11 @@
 
 lemma compact_sinlD: "compact (sinl\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinl]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinl]], simp)
 
 lemma compact_sinrD: "compact (sinr\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=sinr]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=sinr]], simp)
 
 lemma compact_sinl_iff [simp]: "compact (sinl\<cdot>x) = compact x"
 by (safe elim!: compact_sinl compact_sinlD)
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -453,7 +453,7 @@
       fun argvars n args = map_index (argvar n) args;
       fun app s (l, r) = mk_appl (Constant s) [l, r];
       val cabs = app "_cabs";
-      val capp = app @{const_syntax Rep_CFun};
+      val capp = app @{const_syntax Rep_cfun};
       val capps = Library.foldl capp
       fun con1 authentic n (con,args) =
           Library.foldl capp (c_ast authentic con, argvars n args);
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOLCF/Tools/Domain/domain_induction.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_induction.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -132,7 +132,7 @@
       mk_trp (p $ HOLCF_Library.mk_bottom T) :: map (con_assm true p) cons;
   val assms = maps eq_assms (Ps ~~ newTs ~~ map #con_specs constr_infos);
 
-  val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+  val take_ss = HOL_ss addsimps (@{thm Rep_cfun_strict1} :: take_rews);
   fun quant_tac ctxt i = EVERY
     (map (fn name => res_inst_tac ctxt [(("x", 0), name)] spec i) x_names);
 
@@ -317,7 +317,7 @@
         end;
       val goal =
           mk_trp (foldr1 mk_conj (map one (newTs ~~ Rs ~~ take_consts)));
-      val rules = @{thm Rep_CFun_strict1} :: take_0_thms;
+      val rules = @{thm Rep_cfun_strict1} :: take_0_thms;
       fun tacf {prems, context} =
         let
           val prem' = rewrite_rule [bisim_def_thm] (hd prems);
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -155,7 +155,7 @@
     (* convert parameters to lambda abstractions *)
     fun mk_eqn (lhs, rhs) =
         case lhs of
-          Const (@{const_name Rep_CFun}, _) $ f $ (x as Free _) =>
+          Const (@{const_name Rep_cfun}, _) $ f $ (x as Free _) =>
             mk_eqn (f, big_lambda x rhs)
         | f $ Const (@{const_name TYPE}, T) =>
             mk_eqn (f, Abs ("t", T, rhs))
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -28,7 +28,7 @@
   in
     [Syntax.ParsePrintRule
       (Syntax.mk_appl (Constant name2) (map Variable vnames),
-        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_CFun}) [t, Variable a])
+        fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
           vnames (Constant name1))] @
     (case mx of
       Infix _ => [extra_parse_rule]
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/cont_proc.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -21,17 +21,17 @@
 val cont_I = @{thm cont_id};
 val cont_A = @{thm cont2cont_APP};
 val cont_L = @{thm cont2cont_LAM};
-val cont_R = @{thm cont_Rep_CFun2};
+val cont_R = @{thm cont_Rep_cfun2};
 
 (* checks whether a term contains no dangling bound variables *)
 fun is_closed_term t = not (Term.loose_bvar (t, 0));
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
       is_lcf_term t
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ t) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
       is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
@@ -67,17 +67,17 @@
   (* first list: cont thm for each dangling bound variable *)
   (* second list: cont thm for each LAM in t *)
   (* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
+  fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
     let
       val (cs1,ls1) = cont_thms1 b f;
       val (cs2,ls2) = cont_thms1 b t;
     in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
     let
       val (cs, ls) = cont_thms1 b t;
       val (cs', l) = lam cs;
     in (cs', l::ls) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ t) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
     let
       val t' = Term.incr_boundvars 1 t $ Bound 0;
       val (cs, ls) = cont_thms1 b t';
@@ -109,7 +109,7 @@
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
-        val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f;
       in
         if is_lcf_term f'
         then new_cont_tac f'
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -65,7 +65,7 @@
 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
 
 (* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f
+fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
   | chead_of u = u;
 
 infix 0 ==;  val (op ==) = Logic.mk_equals;
@@ -82,7 +82,7 @@
     val run = Const(@{const_name Fixrec.run}, mT ->> T)
   in
     case t of
-      Const(@{const_name Rep_CFun}, _) $
+      Const(@{const_name Rep_cfun}, _) $
         Const(@{const_name Fixrec.succeed}, _) $ u => u
     | _ => run ` t
   end;
@@ -226,7 +226,7 @@
     (* compiles a monadic term for a constructor pattern *)
     and comp_con T p rhs vs taken =
       case p of
-        Const(@{const_name Rep_CFun},_) $ f $ x =>
+        Const(@{const_name Rep_cfun},_) $ f $ x =>
           let val (rhs', v, taken') = comp_pat x rhs taken
           in comp_con T f rhs' (v::vs) taken' end
       | f $ x =>
@@ -250,7 +250,7 @@
 (* returns (constant, (vars, matcher)) *)
 fun compile_lhs match_name pat rhs vs taken =
   case pat of
-    Const(@{const_name Rep_CFun}, _) $ f $ x =>
+    Const(@{const_name Rep_cfun}, _) $ f $ x =>
       let val (rhs', v, taken') = compile_pat match_name x rhs taken;
       in compile_lhs match_name f rhs' (v::vs) taken' end
   | Free(_,_) => (pat, (vs, rhs))
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Tools/holcf_library.ML
--- a/src/HOLCF/Tools/holcf_library.ML	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Tools/holcf_library.ML	Fri Oct 29 17:15:28 2010 -0700
@@ -76,10 +76,10 @@
   | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
 
 fun capply_const (S, T) =
-  Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T));
+  Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T));
 
 fun cabs_const (S, T) =
-  Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T));
+  Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T));
 
 fun mk_cabs t =
   let val T = fastype_of t
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/Up.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -237,7 +237,7 @@
 
 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x"
 unfolding compact_def
-by (drule adm_subst [OF cont_Rep_CFun2 [where f=up]], simp)
+by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp)
 
 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x"
 by (safe elim!: compact_up compact_upD)
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -252,7 +252,7 @@
 lemma compact_upper_unit_iff [simp]: "compact {x}\<sharp> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_upper_unit)
 apply (simp only: compact_def upper_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_upper_plus [simp]:
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/ex/Domain_Proofs.thy
--- a/src/HOLCF/ex/Domain_Proofs.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -31,7 +31,7 @@
   foo_bar_baz_deflF ::
     "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
 where
-  "foo_bar_baz_deflF = (\<Lambda> a. Abs_CFun (\<lambda>(t1, t2, t3). 
+  "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>a)\<cdot>(u_defl\<cdot>t2))
     , u_defl\<cdot>(cfun_defl\<cdot>t3\<cdot>DEFL(tr))
     , u_defl\<cdot>(cfun_defl\<cdot>(convex_defl\<cdot>t1)\<cdot>DEFL(tr)))))"
@@ -269,7 +269,7 @@
      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
 where
-  "foo_bar_baz_mapF = (\<Lambda> f. Abs_CFun (\<lambda>(d1, d2, d3).
+  "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
     (
       foo_abs oo
         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
diff -r 73d45866dbda -r 1dfdbd66093a src/HOLCF/ex/Pattern_Match.thy
--- a/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -115,9 +115,9 @@
 
 parse_translation {*
 (* rewrite (_pat x) => (succeed) *)
-(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *)
+(* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
-  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})];
+  mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* Printing Case expressions *}
@@ -127,14 +127,14 @@
 
 print_translation {*
   let
-    fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
+    fun dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax unit_when},_) $ t) =
           (Syntax.const @{syntax_const "_noargs"}, t)
-    |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
+    |   dest_LAM (Const (@{const_syntax Rep_cfun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let
             val (v1, t1) = dest_LAM t;
             val (v2, t2) = dest_LAM t1;
           in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end
-    |   dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) =
+    |   dest_LAM (Const (@{const_syntax Abs_cfun},_) $ t) =
           let
             val abs =
               case t of Abs abs => abs
@@ -149,7 +149,7 @@
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
-  in [(@{const_syntax Rep_CFun}, Case1_tr')] end;
+  in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
 *}
 
 translations
@@ -485,7 +485,7 @@
       open Syntax
       fun syntax c = Syntax.mark_const (fst (dest_Const c));
       fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
-      val capp = app @{const_syntax Rep_CFun};
+      val capp = app @{const_syntax Rep_cfun};
       val capps = Library.foldl capp
 
       fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];