# HG changeset patch # User Christian Urban # Date 1325162258 0 # Node ID 3d9562921451bd7da5e9abfc092abc202ee3dff0 # Parent b27e94db1b8ac6c2bed6e2095ca67408bd5e68f0 made the paper running again 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