--- a/src/HOLCF/IOA/NTP/Abschannel.thy Thu Jul 17 12:44:16 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Abschannel.thy Thu Jul 17 12:44:58 1997 +0200
@@ -24,6 +24,9 @@
srch_asig,
rsch_asig :: 'm action signature
+srch_wfair, srch_sfair, rsch_sfair,
+rsch_wfair ::('m action)set set
+
srch_trans :: ('m action, 'm packet multiset)transition set
rsch_trans :: ('m action, bool multiset)transition set
@@ -39,6 +42,12 @@
srch_trans_def "srch_trans == trans_of(srch_ioa)"
rsch_trans_def "rsch_trans == trans_of(rsch_ioa)"
+srch_wfair_def "srch_wfair == wfair_of(srch_ioa)"
+rsch_wfair_def "rsch_wfair == wfair_of(rsch_ioa)"
+
+srch_sfair_def "srch_sfair == sfair_of(srch_ioa)"
+rsch_sfair_def "rsch_sfair == sfair_of(rsch_ioa)"
+
srch_ioa_def "srch_ioa == rename ch_ioa srch_actions"
rsch_ioa_def "rsch_ioa == rename ch_ioa rsch_actions"
@@ -53,7 +62,7 @@
of S(b) => t = addm s b |
R(b) => count s b ~= 0 & t = delm s b}"
-ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
+ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans,{},{})"
rsch_actions_def "rsch_actions (akt) ==