src/HOL/HOLCF/IOA/meta_theory/Automata.thy
changeset 41476 0fa9629aa399
parent 40945 b8703f63bfb2
child 42151 4da4fc77664b
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,8 +10,10 @@
 
 default_sort type
 
-types
+type_synonym
   ('a, 's) transition = "'s * 'a * 's"
+
+type_synonym
   ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
 
 consts