# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1356985255 0
# Node ID 96d10631eec22d1f5ad3b0d4ceaac2b31a92f5a2
# Parent  d144fc51fe04a8469b6dc5e0384912ef50fe4ca3
added readme and fixed output in Subgoal.FOCUS section

diff -r d144fc51fe04 -r 96d10631eec2 ProgTutorial/Parsing.thy
--- 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}
diff -r d144fc51fe04 -r 96d10631eec2 ProgTutorial/Tactical.thy
--- 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}
 *}
diff -r d144fc51fe04 -r 96d10631eec2 README
--- /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
diff -r d144fc51fe04 -r 96d10631eec2 progtutorial.pdf
Binary file progtutorial.pdf has changed