--- a/ProgTutorial/Advanced.thy	Sun Dec 06 14:26:14 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Fri Jan 01 00:19:11 2010 +0100
@@ -127,6 +127,10 @@
 
 section {* Contexts (TBD) *}
 
+ML_command "ProofContext.debug := true"
+ML_command "ProofContext.verbose := true"
+
+
 section {* Local Theories (TBD) *}
 
 text {*

--- a/ProgTutorial/FirstSteps.thy	Sun Dec 06 14:26:14 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Fri Jan 01 00:19:11 2010 +0100
@@ -406,10 +406,10 @@
 section {* Combinators\label{sec:combinators} *}
 
 text {*
-  For beginners perhaps the most puzzling parts in the existing code of Isabelle are
-  the combinators. At first they seem to greatly obstruct the
-  comprehension of the code, but after getting familiar with them, they
-  actually ease the understanding and also the programming.
+  For beginners perhaps the most puzzling parts in the existing code of
+  Isabelle are the combinators. At first they seem to greatly obstruct the
+  comprehension of code, but after getting familiar with them and handled with
+  care, they actually ease the understanding and also the programming.
 
   The simplest combinator is @{ML_ind I in Library}, which is just the 
   identity function defined as

--- a/ProgTutorial/Tactical.thy	Sun Dec 06 14:26:14 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Fri Jan 01 00:19:11 2010 +0100
@@ -1411,10 +1411,12 @@
   \footnote{\bf FIXME: show rewriting of cterms}
 
   There is one restriction you have to keep in mind when using the simplifier:
-  it can only deal with rewriting rules that are higher order pattern 
-  (see Section \ref{sec:univ} on unification). If a rule is not a pattern,
-  then you have to use simprocs or conversions, which we shall describe in
-  the next section.
+  it can only deal with rewriting rules whose left-hand sides are higher order 
+  pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern
+  or not can be tested with the function @{ML_ind pattern in Pattern} from
+  the structure @{ML_struct Pattern}. If a rule is not a pattern and you want
+  to use it for rewriting, then you have to use simprocs or conversions, both 
+  of which we shall describe in the next section.
 
   When using the simplifier, the crucial information you have to provide is
   the simpset. If this information is not handled with care, then, as

Binary file progtutorial.pdf has changed