--- a/ProgTutorial/Parsing.thy	Sat Dec 01 16:50:46 2012 +0000
+++ b/ProgTutorial/Parsing.thy	Mon Dec 31 20:20:55 2012 +0000
@@ -12,6 +12,14 @@
   Tony Travis in an email about the\\ ``LINUX is obsolete'' debate 
   \end{flushright}
 
+  \begin{flushright}
+  {\em
+  Document your code as if someone else might have to take it over at any 
+  moment and know what to do with it. That person might actually be you -- 
+  how often have you had to revisit your own code and thought to yourself, 
+  what was I trying to do here?} \\[1ex]
+  Phil Chu in ``Seven Habits of Highly Effective Programmers'' 
+  \end{flushright}
 
   Isabelle distinguishes between \emph{outer} and \emph{inner}
   syntax. Commands, such as \isacommand{definition}, \isacommand{inductive}

--- a/ProgTutorial/Tactical.thy	Sat Dec 01 16:50:46 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Dec 31 20:20:55 2012 +0000
@@ -524,7 +524,11 @@
 ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
 let 
   fun assgn1 f1 f2 xs =
-    Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 
+    let
+      val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
+    in
+      Pretty.list "" "" out
+    end 
 
   fun assgn2 f xs = assgn1 f f xs 
  
@@ -558,10 +562,10 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{text "x:= x"}, @{text "y:= y"}\\
-  schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}\\
   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
-  premises:    & @{term "A x y"}
+  premises:    & @{term "A x y"}\\
+  schematics:  & @{text "?z:=z"}
   \end{tabular}
   \end{quote}
 
@@ -586,10 +590,10 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{text "x:= x"}, @{text "y:= y"}\\
-  schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}, @{term "B y x"}\\
   conclusion:  & @{term "C (z y) x"}\\
-  premises:    & @{term "A x y"}, @{term "B y x"}
+  premises:    & @{term "A x y"}, @{term "B y x"}\\
+  schematics:  & @{text "?z:=z"}
   \end{tabular}
   \end{quote}
 *}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README	Mon Dec 31 20:20:55 2012 +0000
@@ -0,0 +1,4 @@
+Building
+========
+
+isabelle build -c -v -d . Cookbook

Binary file progtutorial.pdf has changed