src/HOLCF/Representable.thy
changeset 35525 fa231b86cb1e
parent 35514 a2cfa413eaab
child 35527 f4282471461d
--- a/src/HOLCF/Representable.thy	Tue Mar 02 17:20:03 2010 -0800
+++ b/src/HOLCF/Representable.thy	Tue Mar 02 17:21:10 2010 -0800
@@ -416,7 +416,7 @@
 
 text "Functions between representable types are representable."
 
-instantiation "->" :: (rep, rep) rep
+instantiation cfun :: (rep, rep) rep
 begin
 
 definition emb_cfun_def: "emb = udom_emb oo cfun_map\<cdot>prj\<cdot>emb"
@@ -431,7 +431,7 @@
 
 text "Strict products of representable types are representable."
 
-instantiation "**" :: (rep, rep) rep
+instantiation sprod :: (rep, rep) rep
 begin
 
 definition emb_sprod_def: "emb = udom_emb oo sprod_map\<cdot>emb\<cdot>emb"
@@ -446,7 +446,7 @@
 
 text "Strict sums of representable types are representable."
 
-instantiation "++" :: (rep, rep) rep
+instantiation ssum :: (rep, rep) rep
 begin
 
 definition emb_ssum_def: "emb = udom_emb oo ssum_map\<cdot>emb\<cdot>emb"
@@ -784,13 +784,13 @@
 
 setup {*
   fold Domain_Isomorphism.add_type_constructor
-    [(@{type_name "->"}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
+    [(@{type_name cfun}, @{term cfun_defl}, @{const_name cfun_map}, @{thm REP_cfun},
         @{thm isodefl_cfun}, @{thm cfun_map_ID}, @{thm deflation_cfun_map}),
 
-     (@{type_name "++"}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
+     (@{type_name ssum}, @{term ssum_defl}, @{const_name ssum_map}, @{thm REP_ssum},
         @{thm isodefl_ssum}, @{thm ssum_map_ID}, @{thm deflation_ssum_map}),
 
-     (@{type_name "**"}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
+     (@{type_name sprod}, @{term sprod_defl}, @{const_name sprod_map}, @{thm REP_sprod},
         @{thm isodefl_sprod}, @{thm sprod_map_ID}, @{thm deflation_sprod_map}),
 
      (@{type_name "*"}, @{term cprod_defl}, @{const_name cprod_map}, @{thm REP_cprod},