--- a/ProgTutorial/FirstSteps.thy	Sun Nov 01 10:49:25 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Nov 02 12:47:00 2009 +0100
@@ -254,6 +254,38 @@
   commas (map (string_of_term ctxt) ts)*}
 
 text {*
+  Sometimes you want to print out a term together with some type information.
+  This can be achieved by setting the reference 
+  @{ML_ind show_types}\footnote{\bf FIXME: ``forgotten'' structure Printer, Mixfix etc.} 
+  to @{ML true}.
+*}
+
+ML{*show_types := true*}
+
+text {*
+  Now @{ML string_of_term} prints out
+
+  @{ML_response_fake [display, gray]
+  "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+  "(1::nat, x::'a)"}
+
+  where @{text 1} and @{text x} are displayed with their type.
+  Even more type information can be printed by setting 
+  @{ML_ind show_all_types} to @{ML true}. We obtain
+*}
+(*<*)ML %linenos {*show_all_types := true*}
+(*>*)
+text {*
+  @{ML_response_fake [display, gray]
+  "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
+  "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
+
+  Other references that influence printing are @{ML_ind show_brackets} 
+  and @{ML_ind show_sorts}. 
+*}
+(*<*)ML %linenos {*show_types := false; show_all_types := false*}
+(*>*)
+text {*
   A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 
@@ -321,6 +353,13 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
+  \begin{readmore}
+  The simple conversion functions from Isabelle's main datatypes to 
+  @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 
+  The references that change the printing information are declared in 
+  @{ML_file "Pure/Syntax/printer.ML"}.
+  \end{readmore}
+
   Note that when printing out several ``parcels'' of information that
   semantically belong together, like a warning message consisting of 
   a term and its type, you should try to keep this information together in a
@@ -1303,7 +1342,7 @@
 
   \begin{conventions}
   \begin{itemize}
-  \item Print messages that belong together as a single string.
+  \item Print messages that belong together in a single string.
   \item Do not use references in Isabelle code.
   \end{itemize}
   \end{conventions}

--- a/ProgTutorial/Tactical.thy	Sun Nov 01 10:49:25 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Mon Nov 02 12:47:00 2009 +0100
@@ -1253,12 +1253,12 @@
 
 text {*
   \begin{exercise}\label{ex:dyckhoff}
-  Dyckhoff presents in \cite{Dyckhoff92} inference rules for a sequent
+  Dyckhoff presents in \cite{Dyckhoff92} inference rules of a sequent
   calculus, called G4ip, for intuitionistic propositional logic. The
   interesting feature of this calculus is that no contraction rule is needed
-  in order to be complete. As a result applying the rules exhaustively leads
-  to simple decision procedure for propositional intuitionistic logic. The task
-  is to implement this decision procedure as a tactic. His rules are
+  in order to be complete. As a result the rules can be applied exhaustively, which
+  in turn leads to simple decision procedure for propositional intuitionistic logic. 
+  The task is to implement this decision procedure as a tactic. His rules are
 
   \begin{center}
   \def\arraystretch{2.3}
@@ -1298,17 +1298,19 @@
   \end{tabular}
   \end{center}
 
-  Note that in Isabelle the left-rules need to be implemented as elimination
-  rules. You need to prove separate lemmas corresponding to
-  $\longrightarrow_{L_{1..4}}$. The tactic should explore all possibilites of
-  applying these rules to a propositional formula until a goal state is
-  reached in which all subgoals are discharged. For this you can use the tactic 
-  combinator @{ML_ind DEPTH_SOLVE in Search}. 
+  Note that in Isabelle right rules need to be implemented as
+  introduction rule, the left rules as elimination rules. You have to to
+  prove separate theorems corresponding to $\longrightarrow_{L_{1..4}}$. The
+  tactic should explore all possibilites of applying these rules to a
+  propositional formula until a goal state is reached in which all subgoals
+  are discharged. For this you can use the tactic combinator @{ML_ind
+  DEPTH_SOLVE in Search} in the structure @{ML_struct Search}.
   \end{exercise}
 
   \begin{exercise}
-  Add to the previous exercise also rules for equality and run your tactic on 
-  the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
+  Add to the sequent calculus from the previous exercise also rules for 
+  equality and run your tactic on  the de Bruijn formulae discussed 
+  in Exercise~\ref{ex:debruijn}.
   \end{exercise}
 *}
 
@@ -1316,8 +1318,8 @@
 
 text {*
   A lot of convenience in reasoning with Isabelle derives from its
-  powerful simplifier. We will describe it in this section, whereby 
-  we can, however, only scratch the surface due to its complexity. 
+  powerful simplifier. We will describe it in this section. However,
+  due to its complexity, we can mostly only scratch the surface. 
 
   The power of the simplifier is a strength and a weakness at the same time,
   because you can easily make the simplifier run into a loop and in general
@@ -1338,7 +1340,7 @@
   \end{center}
   \end{isabelle}
 
-  All of the tactics take a simpset and an integer as argument (the latter as usual 
+  All these tactics take a simpset and an integer as argument (the latter as usual 
   to specify  the goal to be analysed). So the proof
 *}
 
@@ -1386,17 +1388,20 @@
   with @{text "constr"} being a constant, like @{const "If"}, @{const "Let"}
   and so on. Every simpset contains only one congruence rule for each
   term-constructor, which however can be overwritten. The user can declare
-  lemmas to be congruence rules using the attribute @{text "[cong]"}. In HOL,
-  the user usually states these lemmas as equations, which are then internally
-  transformed into meta-equations.
+  lemmas to be congruence rules using the attribute @{text "[cong]"}. Note that 
+  in HOL these congruence theorems are usually stated as equations, which are 
+  then internally transformed into meta-equations.
 
   The rewriting with theorems involving premises requires what is in Isabelle
   called a subgoaler, a solver and a looper. These can be arbitrary tactics
   that can be installed in a simpset and which are executed at various stages
-  during simplification. However, simpsets also include simprocs, which can
-  produce rewrite rules on demand (see next section). Another component are
-  split-rules, which can simplify for example the ``then'' and ``else''
-  branches of if-statements under the corresponding preconditions.
+  during simplification. 
+
+  Simpsets can also include simprocs, which produce rewrite rules on
+  demand according to a pattern (see next section for a detailed description
+  of simpsets). Another component are split-rules, which can simplify for
+  example the ``then'' and ``else'' branches of if-statements under the
+  corresponding preconditions.
 
   \begin{readmore}
   For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
@@ -1408,10 +1413,10 @@
   \footnote{\bf FIXME: Find the right place to mention this: Discrimination 
   nets are implemented in @{ML_file "Pure/net.ML"}.}
 
-  The most common combinators to modify simpsets are:
+  The most common combinators for modifying simpsets are:
 
   \begin{isabelle}
-  \begin{tabular}{ll}
+  \begin{tabular}{l@ {\hspace{10mm}}l}
   @{ML_ind addsimps in MetaSimplifier}    & @{ML_ind delsimps in MetaSimplifier}\\
   @{ML_ind addcongs in MetaSimplifier}    & @{ML_ind delcongs in MetaSimplifier}\\
   @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
@@ -1497,9 +1502,10 @@
 Simproc patterns:"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
-  expects this form of the simplification and congruence rules. However, even 
+  expects this form of the simplification and congruence rules. This is
+  different, if we use for example the simpset @{ML HOL_basic_ss} (see below), 
+  where rules are usually added as equation. However, even 
   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
-
   In the context of HOL, the first really useful simpset is @{ML_ind
   HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 
@@ -1509,7 +1515,7 @@
 Congruences rules:
 Simproc patterns:"}
 
-  also produces ``nothing'', the printout is misleading. In fact
+  also produces ``nothing'', the printout is somewhat misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
   form  
 
@@ -1565,7 +1571,7 @@
 definition "MyTrue \<equiv> True"
 
 text {*
-  then we can use this tactic to unfold the definition of the constant.
+  then we can use this tactic to unfold the definition of this constant.
 *}
 
 lemma 
@@ -1578,7 +1584,7 @@
 (*<*)oops(*>*)
 
 text {*
-  If you want to unfold definitions in \emph{all} subgoals not just one, 
+  If you want to unfold definitions in \emph{all} subgoals, not just one, 
   then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
 *}
 

Binary file progtutorial.pdf has changed