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