src/HOL/IOA/Solve.thy

--- a/src/HOL/IOA/Solve.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/IOA/Solve.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -10,9 +10,7 @@
 imports IOA
 begin
 
-constdefs
-
-  is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
+definition is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool" where
   "is_weak_pmap f C A ==
    (!s:starts_of(C). f(s):starts_of(A)) &
    (!s t a. reachable C s &