ESOP-Paper/Paper.thy
changeset 3111 60c4c93b30d5
parent 2929 6fac48faee3a
--- a/ESOP-Paper/Paper.thy	Tue Jan 24 14:05:24 2012 +0000
+++ b/ESOP-Paper/Paper.thy	Tue Jan 24 14:29:07 2012 +0000
@@ -1,3 +1,4 @@
+
 (*<*)
 theory Paper
 imports "../Nominal/Nominal2" 
@@ -815,8 +816,8 @@
   %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 (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]} \;\;\text{if and only if}\;\; 
+  %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and bs'="bs", no_vars]}
   %\end{equation}
   %
   %\noindent