--- 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

--- a/IsaMakefile	Tue Jan 24 14:05:24 2012 +0000
+++ b/IsaMakefile	Tue Jan 24 14:29:07 2012 +0000
@@ -1,10 +1,10 @@
 
 ## targets
 
-default: tests
+default: session
 images: 
 
-all: tests esop pearl pearl-jv qpaper slides
+all: tests esop pearl pearl-jv qpaper slides lmcs
 
 
 ## global settings
@@ -196,7 +196,7 @@
 	cp Slides/generated9/root.beamer.pdf Slides/slides9.pdf 
 
 
-slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8
+slides: slides1 slides2 slides3 slides4 slides5 slides6 slides7 slides8 slides8 slides9
 
 
 

--- a/Quotient-Paper/Paper.thy	Tue Jan 24 14:05:24 2012 +0000
+++ b/Quotient-Paper/Paper.thy	Tue Jan 24 14:29:07 2012 +0000
@@ -45,7 +45,7 @@
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
     val concl =
-      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => proj (l, r)
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT9.ML	Tue Jan 24 14:29:07 2012 +0000
@@ -0,0 +1,6 @@
+(*show_question_marks := false;*)
+quick_and_dirty := true;
+
+no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
+
+use_thy "Slides9"
\ No newline at end of file