Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <urbanc@in.tum.de>
Thu, 24 May 2012 15:22:25 +0100
changeset 518 7ff1a681f758
parent 517 d8c376662bb4
child 519 cf471fa86091
updated
ProgTutorial/Advanced.thy file | annotate | diff | comparison | revisions
progtutorial.pdf file | annotate | diff | comparison | revisions 
--- 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;
Binary file progtutorial.pdf has changed
isabelle-cookbook