src/HOL/IMP/Fold.thy
changeset 45134 9b02f6665fc8
parent 45015 fdac1e9880eb
child 45200 1f1897ac7877
--- a/src/HOL/IMP/Fold.thy	Wed Oct 12 22:48:23 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Thu Oct 13 11:45:33 2011 +0200
@@ -4,7 +4,7 @@
 
 subsection "Simple folding of arithmetic expressions"
 
-types
+type_synonym
   tab = "name \<Rightarrow> val option"
 
 (* maybe better as the composition of substitution and the existing simp_const(0) *)