changeset 42765 | aec61b60ff7b |
parent 27015 | f8537d69f514 |
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Thu May 12 16:58:55 2011 +0200 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Thu May 12 17:17:57 2011 +0200 @@ -15,7 +15,7 @@ appropriate function itself. *} -types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"; +type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"; datatype ('a,'v)expr = Cex 'v | Vex 'a | Bex "'v binop" "('a,'v)expr" "('a,'v)expr";