# HG changeset patch # User Christian Urban # 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 \ 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