src/HOL/HOLCF/IOA/meta_theory/TLS.thy

--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 00:28:31 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 09:30:52 2011 -0800
@@ -10,9 +10,13 @@
 
 default_sort type
 
-types
+type_synonym
   ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
+
+type_synonym
   ('a, 's) step_pred = "('a option,'s)transition predicate"
+
+type_synonym
   's state_pred      = "'s predicate"
 
 consts