--- a/ProgTutorial/Advanced.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -14,6 +14,12 @@
 chapter {* Advanced Isabelle *}
 
 text {*
+   \begin{flushright}
+  {\em All things are difficult before they are easy.} \\[1ex]
+  proverb
+  \end{flushright}
+
+  \medskip
   While terms, types and theorems are the most basic data structures in
   Isabelle, there are a number of layers built on top of them. Most of these
   layers are concerned with storing and manipulating data. Handling them

--- a/ProgTutorial/Essential.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Essential.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -14,9 +14,16 @@
 chapter {* Isabelle Essentials *}
 
 text {*
+   \begin{flushright}
+  {\em One man's obfuscation is another man's abstraction.} \\[1ex]
+  Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ 
+  24~Nov.~2009
+  \end{flushright}
+
+  \medskip
   Isabelle is build around a few central ideas. One central idea is the
   LCF-approach to theorem proving where there is a small trusted core and
-  everything else is build on top of this trusted core 
+  everything else is built on top of this trusted core 
   \cite{GordonMilnerWadsworth79}. The fundamental data
   structures involved in this core are certified terms and certified types, 
   as well as theorems.

--- a/ProgTutorial/Solutions.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Solutions.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -256,10 +256,7 @@
 
 val add_conv = More_Conv.bottom_conv add_simple_conv
 
-fun add_tac ctxt = CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (add_conv ctxt) then_conv
-          Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*}
+fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
 
 text {*
   A test case for this conversion is as follows

--- a/ProgTutorial/Tactical.thy	Wed Dec 02 17:08:37 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Thu Dec 03 14:19:13 2009 +0100
@@ -2402,7 +2402,8 @@
   goal states. This can be done with the help of the function 
   @{ML_ind CONVERSION in Tactical},
   and also some predefined conversion combinators that traverse a goal
-  state. The combinators for the goal state are: 
+  state and can selectively apply the conversion. The combinators for 
+  the goal state are: 
 
   \begin{itemize}
   \item @{ML_ind params_conv in Conv} for converting under parameters
@@ -2448,7 +2449,9 @@
 
 text {*
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
-  the conclusion according to @{ML true_conj1_conv}.
+  the conclusion according to @{ML true_conj1_conv}. If we only have one
+  conversion that should be uniformly applied to the whole goal state, we
+  can also use @{ML_ind top_conv in More_Conv}.
 
   Conversions can also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following

Binary file progtutorial.pdf has changed