--- a/IOA/meta_theory/Solve.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/Solve.thy Wed Jun 21 15:12:40 1995 +0200
@@ -15,12 +15,12 @@
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), \
-\ f(s)=f(t)))"
+ "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