--- a/IOA/meta_theory/Solve.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Solve.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,10 @@
-(* 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 +
@@ -6,15 +12,15 @@
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