diff -r c3913a79b6ae -r 492493334e0f 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) & \ -\ :trans_of(C) \ -\ --> if(a:externals(asig_of(C)), \ -\ :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) & + :trans_of(C) + --> if(a:externals(asig_of(C)), + :trans_of(A), + f(s)=f(t)))" end