src/HOLCF/ex/Domain_Proofs.thy
changeset 40327 1dfdbd66093a
parent 40038 9d061b3d8f46
child 40491 6de5839e2fb3
--- 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))