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"