src/HOLCF/Representable.thy

 
 subsubsection {* Representable type constructors *}
 
 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"
 definition prj_cfun_def: "prj = cfun_map\<cdot>emb\<cdot>prj oo udom_prj"
 

 
 end
 
 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"
 definition prj_sprod_def: "prj = sprod_map\<cdot>prj\<cdot>prj oo udom_prj"
 

 
 end
 
 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"
 definition prj_ssum_def: "prj = ssum_map\<cdot>prj\<cdot>prj oo udom_prj"
 

 use "Tools/Domain/domain_take_proofs.ML"
 use "Tools/Domain/domain_isomorphism.ML"
 
 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},
         @{thm isodefl_cprod}, @{thm cprod_map_ID}, @{thm deflation_cprod_map}),