# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# 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