# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1337869345 -3600
# Node ID 7ff1a681f7584a59581856e336ef44f97c274c7c
# Parent  d8c376662bb49653a83ce073749743fbcdacb4f3
updated

diff -r d8c376662bb4 -r 7ff1a681f758 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Mon Apr 30 14:43:52 2012 +0100
+++ b/ProgTutorial/Advanced.thy	Thu May 24 15:22:25 2012 +0100
@@ -205,13 +205,9 @@
 
 lemma "True"
 proof -
-  txt_raw {*\mbox{}\\[-7mm]*} 
   ML_prf {* Variable.dest_fixes @{context} *} 
-  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
- fix x y  
-  txt_raw {*\mbox{}\\[-7mm]*}
-  ML_prf {* Variable.dest_fixes @{context} *} 
-  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
+  fix x y  
+  ML_prf {* Variable.dest_fixes @{context} *}(*<*)oops(*>*)
 
 text {*
   The interesting point is that we injected ML-code before and after
@@ -232,13 +228,9 @@
 proof -
   fix x y
   { fix z w
-  txt_raw {*\mbox{}\\[-7mm]*}
-  ML_prf {* Variable.dest_fixes @{context} *} 
-  txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
- }
-  txt_raw {*\mbox{}\\[-7mm]*}
-  ML_prf {* Variable.dest_fixes @{context} *} 
-  txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
+    ML_prf {* Variable.dest_fixes @{context} *} 
+  }
+  ML_prf {* Variable.dest_fixes @{context} *}(*<*)oops(*>*)
 
 text {*
   Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables;
diff -r d8c376662bb4 -r 7ff1a681f758 progtutorial.pdf
Binary file progtutorial.pdf has changed