Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Representable.thy
changeset 35431 8758fe1fc9f8
parent 33809 033831fd9ef3
child 35547 991a6af75978 
--- a/src/HOLCF/Representable.thy	Wed Mar 03 00:32:14 2010 +0100
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 00:33:02 2010 +0100
@@ -49,7 +49,7 @@
 text "A TypeRep is an algebraic deflation over the universe of values."
 
 types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
 
 definition
   Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -59,7 +59,7 @@
       (emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
 
 syntax "_REP" :: "type \<Rightarrow> TypeRep"  ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
 
 lemma cast_REP:
   "cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
isabelle