src/HOLCF/Representable.thy
changeset 35431 8758fe1fc9f8
parent 33809 033831fd9ef3
child 35547 991a6af75978
     1.1 --- a/src/HOLCF/Representable.thy	Wed Mar 03 00:32:14 2010 +0100
     1.2 +++ b/src/HOLCF/Representable.thy	Wed Mar 03 00:33:02 2010 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  text "A TypeRep is an algebraic deflation over the universe of values."
     1.5  
     1.6  types TypeRep = "udom alg_defl"
     1.7 -translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
     1.8 +translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
     1.9  
    1.10  definition
    1.11    Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
    1.12 @@ -59,7 +59,7 @@
    1.13        (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
    1.14  
    1.15  syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
    1.16 -translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
    1.17 +translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
    1.18  
    1.19  lemma cast_REP:
    1.20    "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"