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 35547 991a6af75978
parent 35527 f4282471461d
parent 35431 8758fe1fc9f8
child 35563 f5ec817df77f 
--- a/src/HOLCF/Representable.thy	Wed Mar 03 15:19:34 2010 +0100
+++ b/src/HOLCF/Representable.thy	Wed Mar 03 16:43:55 2010 +0100
@@ -50,7 +50,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"
@@ -60,7 +60,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