IOA/meta_theory/Solve.thy

--- 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