src/HOL/IOA/NTP/Sender.thy
changeset 1376 92f83b9d17e1
parent 1328 9a449a91425d
--- a/src/HOL/IOA/NTP/Sender.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/NTP/Sender.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -15,13 +15,13 @@
 
 consts
 
-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"
-ssent,srcvd   :: "'m sender_state => bool multiset"
-sbit          :: "'m sender_state => bool"
-ssending      :: "'m sender_state => bool"
+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
+ssent,srcvd   :: 'm sender_state => bool multiset
+sbit          :: 'm sender_state => bool
+ssending      :: 'm sender_state => bool
 
 defs