src/HOL/Bali/Eval.thy
changeset 41778 5f79a9e42507
parent 40340 d1c14898fd04
child 44890 22f665a2e91c
--- a/src/HOL/Bali/Eval.thy	Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Eval.thy	Fri Feb 18 16:36:42 2011 +0100
@@ -96,8 +96,8 @@
 *}
 
 
-types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
-      vals  =        "(val, vvar, val list) sum3"
+type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+type_synonym vals = "(val, vvar, val list) sum3"
 translations
   (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   (type) "vals" <= (type) "(val, vvar, val list) sum3"