changes neede for introducing fairness

--- a/src/HOLCF/IOA/ABP/Abschannel.thy	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel.thy	Thu Jul 17 12:44:16 1997 +0200
@@ -59,7 +59,7 @@
                     b = hd(s) &                                 
                     ((t = s) | (t = tl(s)))    }"
   
-ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
+ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans,{},{})"
 
 (**********************************************************
   C o n c r e t e  C h a n n e l s  b y   R e n a m i n g 

--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy	Thu Jul 17 12:44:16 1997 +0200
@@ -57,7 +57,7 @@
                     b = hd(s) &                                 
                     ((t = s) | (t = tl(s)))    }"
   
-ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
+ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans,{},{})"
 
 end  
 

--- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Jul 17 12:44:16 1997 +0200
@@ -13,7 +13,7 @@
 Delsimps [split_paired_All];
 Addsimps 
  ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
-   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, 
+   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, 
    actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, 
    trans_of_def] @ asig_projections @ set_lemmas);
 

--- a/src/HOLCF/IOA/ABP/Env.thy	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Env.thy	Thu Jul 17 12:44:16 1997 +0200
@@ -41,7 +41,7 @@
       R_ack(b)   => False}"
 
 env_ioa_def "env_ioa == 
- (env_asig, {True}, env_trans)"
+ (env_asig, {True}, env_trans,{},{})"
 
 end
 

--- a/src/HOLCF/IOA/ABP/Receiver.thy	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Receiver.thy	Thu Jul 17 12:44:16 1997 +0200
@@ -54,6 +54,6 @@
       R_ack(b) => False}"
 
 receiver_ioa_def "receiver_ioa == 
- (receiver_asig, {([],False)}, receiver_trans)"
+ (receiver_asig, {([],False)}, receiver_trans,{},{})"
 
 end

--- a/src/HOLCF/IOA/ABP/Sender.thy	Thu Jul 17 12:43:32 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Sender.thy	Thu Jul 17 12:44:16 1997 +0200
@@ -52,6 +52,6 @@
                      sq(t)=sq(s) & sbit(t)=sbit(s)}"
 
 sender_ioa_def "sender_ioa == 
- (sender_asig, {([],True)}, sender_trans)"
+ (sender_asig, {([],True)}, sender_trans,{},{})"
 
 end