put types into "" because of signature clash;
authormueller
Thu, 22 Apr 1999 11:02:46 +0200
changeset 6468 a7b1669f5365
parent 6467 863834a37769
child 6469 bafd705ee38e
put types into "" because of signature clash;
src/HOLCF/IOA/ABP/Abschannel.thy
src/HOLCF/IOA/ABP/Abschannel_finite.thy
src/HOLCF/IOA/ABP/Env.thy
src/HOLCF/IOA/ABP/Receiver.thy
src/HOLCF/IOA/ABP/Sender.thy
src/HOLCF/IOA/ABP/Spec.thy
src/HOLCF/IOA/NTP/Abschannel.thy
src/HOLCF/IOA/NTP/Receiver.thy
src/HOLCF/IOA/NTP/Sender.thy
src/HOLCF/IOA/NTP/Spec.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
--- 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
--- 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
--- 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
--- 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
--- 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
 
--- 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
--- 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
--- 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
--- 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