IOA/meta_theory/Solve.thy

-(* Methods of proof for IOA. *)
+(*  Title:      HOL/IOA/meta_theory/Solve.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+Weak possibilities mapping (abstraction)
+*)
 
 Solve = IOA +
 
 consts
 
   is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
 
-rules
+defs
 
 is_weak_pmap_def
-  "is_weak_pmap(f,C,A) ==                           \
-\   (!s:starts_of(C). f(s):starts_of(A)) &        \
-\   (!s t a. reachable(C,s) &                       \
-\            <s,a,t>:trans_of(C)                    \
-\            --> if(a:externals(asig_of(C)),        \
-\                   <f(s),a,f(t)>:trans_of(A),      \
+  "is_weak_pmap(f,C,A) ==                       \
+\   (!s:starts_of(C). f(s):starts_of(A)) &      \
+\   (!s t a. reachable(C,s) &                   \
+\            <s,a,t>:trans_of(C)                \
+\            --> if(a:externals(asig_of(C)),    \
+\                   <f(s),a,f(t)>:trans_of(A),  \
 \                   f(s)=f(t)))"
 
 end