# HG changeset patch
# User paulson
# Date 997275090 -7200
# Node ID ec2c382ff4f0b5bcc1983d6b910529c6228b2ef2
# Parent  c77e5401f2ffa18b93bdeccdbe6a20a2527c1f20
Main is the proper parent of IOA

diff -r c77e5401f2ff -r ec2c382ff4f0 src/HOL/IOA/Asig.thy
--- a/src/HOL/IOA/Asig.thy	Wed Aug 08 14:51:10 2001 +0200
+++ b/src/HOL/IOA/Asig.thy	Wed Aug 08 14:51:30 2001 +0200
@@ -6,7 +6,7 @@
 Action signatures
 *)
 
-Asig = Product_Type +
+Asig = Main +
 
 types 
 
diff -r c77e5401f2ff -r ec2c382ff4f0 src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Wed Aug 08 14:51:10 2001 +0200
+++ b/src/HOL/IOA/IOA.thy	Wed Aug 08 14:51:30 2001 +0200
@@ -6,7 +6,7 @@
 The I/O automata of Lynch and Tuttle.
 *)
 
-IOA = Asig + Option +
+IOA = Asig + 
 
 types
    'a seq            =   "nat => 'a"