--- a/src/HOL/IOA/IOA.thy Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IOA/IOA.thy Wed Mar 30 23:26:40 2011 +0200
@@ -9,12 +9,11 @@
imports Asig
begin
-types
- 'a seq = "nat => 'a"
- 'a oseq = "nat => 'a option"
- ('a,'b)execution = "'a oseq * 'b seq"
- ('a,'s)transition = "('s * 'a * 's)"
- ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set"
+type_synonym 'a seq = "nat => 'a"
+type_synonym 'a oseq = "nat => 'a option"
+type_synonym ('a, 'b) execution = "'a oseq * 'b seq"
+type_synonym ('a, 's) transition = "('s * 'a * 's)"
+type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
consts