diff -r b27e94db1b8a -r 3d9562921451 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Fri Dec 23 15:04:01 2011 +0000 +++ b/LMCS-Paper/Paper.thy Thu Dec 29 12:37:38 2011 +0000 @@ -854,7 +854,7 @@ "abs\<^bsub>set\<^esub>"} we have \begin{equation}\label{abseqiff} - @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; + @{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\;\text{if and only if}\;\;\; @{term "alpha_set_ex (as, x) equal supp (bs, y)"} \end{equation}\smallskip