--- a/src/HOL/IOA/ABP/Impl_finite.thy Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Impl_finite.thy Fri Dec 01 12:03:13 1995 +0100
@@ -16,11 +16,11 @@
consts
- impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa"
- sen_fin :: "'m impl_fin_state => 'm sender_state"
- rec_fin :: "'m impl_fin_state => 'm receiver_state"
- srch_fin :: "'m impl_fin_state => 'm packet list"
- rsch_fin :: "'m impl_fin_state => bool list"
+ impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
+ sen_fin :: 'm impl_fin_state => 'm sender_state
+ rec_fin :: 'm impl_fin_state => 'm receiver_state
+ srch_fin :: 'm impl_fin_state => 'm packet list
+ rsch_fin :: 'm impl_fin_state => bool list
defs