# HG changeset patch
# User mueller
# Date 869136256 -7200
# Node ID a34c20f4bf442e7847d2e3a11d6d9dc89216d72b
# Parent  bdc51b4c6050a8d5b936b0c6160ea98d6284d0d1
changes neede for introducing fairness

diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Abschannel.thy
--- 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 
diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Abschannel_finite.thy
--- 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  
 
diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Correctness.ML
--- 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);
 
diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Env.thy
--- 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
 
diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Receiver.thy
--- 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
diff -r bdc51b4c6050 -r a34c20f4bf44 src/HOLCF/IOA/ABP/Sender.thy
--- 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