# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262301551 -3600
# Node ID 95461cf6fd077af90e982580e8d9f43bb7d6f4c8
# Parent  73f716b9201ae3b4ffaca3c71fc5aacb9432b9be
updated to new Isabelle

diff -r 73f716b9201a -r 95461cf6fd07 ProgTutorial/Advanced.thy
--- 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 {*
diff -r 73f716b9201a -r 95461cf6fd07 ProgTutorial/FirstSteps.thy
--- 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
diff -r 73f716b9201a -r 95461cf6fd07 ProgTutorial/Tactical.thy
--- 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
diff -r 73f716b9201a -r 95461cf6fd07 progtutorial.pdf
Binary file progtutorial.pdf has changed