# HG changeset patch # User mueller # Date 924771766 -7200 # Node ID a7b1669f5365aff24d851b539ba9da2dba8600a2 # Parent 863834a377695993e41c64c5104bfad0842de5a2 put types into "" because of signature clash; diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Abschannel.thy --- a/src/HOLCF/IOA/ABP/Abschannel.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel.thy Thu Apr 22 11:02:46 1999 +0200 @@ -14,7 +14,7 @@ consts -ch_asig :: 'a abs_action signature +ch_asig :: "'a abs_action signature" ch_trans :: ('a abs_action, 'a list)transition set ch_ioa :: ('a abs_action, 'a list)ioa @@ -22,7 +22,7 @@ srch_actions :: "'m action =>(bool * 'm) abs_action option" srch_asig, -rsch_asig :: 'm action signature +rsch_asig :: "'m action signature" srch_trans :: ('m action, 'm packet list)transition set rsch_trans :: ('m action, bool list)transition set diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Abschannel_finite.thy --- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Thu Apr 22 11:02:46 1999 +0200 @@ -10,14 +10,14 @@ consts -ch_fin_asig :: 'a abs_action signature +ch_fin_asig :: "'a abs_action signature" ch_fin_trans :: ('a abs_action, 'a list)transition set ch_fin_ioa :: ('a abs_action, 'a list)ioa srch_fin_asig, -rsch_fin_asig :: 'm action signature +rsch_fin_asig :: "'m action signature" srch_fin_trans :: ('m action, 'm packet list)transition set rsch_fin_trans :: ('m action, bool list)transition set diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Env.thy --- a/src/HOLCF/IOA/ABP/Env.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Env.thy Thu Apr 22 11:02:46 1999 +0200 @@ -15,7 +15,7 @@ consts -env_asig :: 'm action signature +env_asig :: "'m action signature" env_trans :: ('m action, 'm env_state)transition set env_ioa :: ('m action, 'm env_state)ioa next :: 'm env_state => bool diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Receiver.thy --- a/src/HOLCF/IOA/ABP/Receiver.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Receiver.thy Thu Apr 22 11:02:46 1999 +0200 @@ -16,7 +16,7 @@ consts - receiver_asig :: 'm action signature + receiver_asig :: "'m action signature" receiver_trans:: ('m action, 'm receiver_state)transition set receiver_ioa :: ('m action, 'm receiver_state)ioa rq :: 'm receiver_state => 'm list diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Sender.thy --- a/src/HOLCF/IOA/ABP/Sender.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Sender.thy Thu Apr 22 11:02:46 1999 +0200 @@ -15,7 +15,7 @@ consts -sender_asig :: 'm action signature +sender_asig :: "'m action signature" sender_trans :: ('m action, 'm sender_state)transition set sender_ioa :: ('m action, 'm sender_state)ioa sq :: 'm sender_state => 'm list diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/ABP/Spec.thy --- a/src/HOLCF/IOA/ABP/Spec.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/ABP/Spec.thy Thu Apr 22 11:02:46 1999 +0200 @@ -10,7 +10,7 @@ consts -spec_sig :: 'm action signature +spec_sig :: "'m action signature" spec_trans :: ('m action, 'm list)transition set spec_ioa :: ('m action, 'm list)ioa diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/NTP/Abschannel.thy --- a/src/HOLCF/IOA/NTP/Abschannel.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Abschannel.thy Thu Apr 22 11:02:46 1999 +0200 @@ -12,7 +12,7 @@ consts -ch_asig :: 'a abs_action signature +ch_asig :: "'a abs_action signature" ch_trans :: ('a abs_action, 'a multiset)transition set @@ -22,7 +22,7 @@ srch_actions :: "'m action =>(bool * 'm) abs_action option" srch_asig, -rsch_asig :: 'm action signature +rsch_asig :: "'m action signature" srch_wfair, srch_sfair, rsch_sfair, rsch_wfair ::('m action)set set diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/NTP/Receiver.thy --- a/src/HOLCF/IOA/NTP/Receiver.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Receiver.thy Thu Apr 22 11:02:46 1999 +0200 @@ -16,7 +16,7 @@ consts - receiver_asig :: 'm action signature + receiver_asig :: "'m action signature" receiver_trans:: ('m action, 'm receiver_state)transition set receiver_ioa :: ('m action, 'm receiver_state)ioa rq :: 'm receiver_state => 'm list diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/NTP/Sender.thy --- a/src/HOLCF/IOA/NTP/Sender.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Sender.thy Thu Apr 22 11:02:46 1999 +0200 @@ -15,7 +15,7 @@ consts -sender_asig :: 'm action signature +sender_asig :: "'m action signature" sender_trans :: ('m action, 'm sender_state)transition set sender_ioa :: ('m action, 'm sender_state)ioa sq :: 'm sender_state => 'm list diff -r 863834a37769 -r a7b1669f5365 src/HOLCF/IOA/NTP/Spec.thy --- a/src/HOLCF/IOA/NTP/Spec.thy Thu Apr 22 11:00:30 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Spec.thy Thu Apr 22 11:02:46 1999 +0200 @@ -10,7 +10,7 @@ consts -spec_sig :: 'm action signature +spec_sig :: "'m action signature" spec_trans :: ('m action, 'm list)transition set spec_ioa :: ('m action, 'm list)ioa