src/HOL/IOA/ABP/Correctness.thy
changeset 1376 92f83b9d17e1
parent 1151 c820b3cc3df0
child 1476 608483c2122a
--- a/src/HOL/IOA/ABP/Correctness.thy	Thu Nov 30 12:58:44 1995 +0100
+++ b/src/HOL/IOA/ABP/Correctness.thy	Fri Dec 01 12:03:13 1995 +0100
@@ -10,9 +10,9 @@
 
 consts
 
-reduce           :: "'a list => 'a list"
+reduce           :: 'a list => 'a list
 
-abs              :: "'c"
+abs              :: 'c
 system_ioa       :: "('m action, bool * 'm impl_state)ioa"
 system_fin_ioa   :: "('m action, bool * 'm impl_state)ioa"