--- a/ProgTutorial/FirstSteps.thy	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Oct 10 18:25:43 2009 +0200
@@ -758,7 +758,7 @@
 end*}
 
 text {*
-  The function @{ML_ind  dest_ss in MetaSimplifier} returns a record containing all
+  The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
   information stored in the simpset, but we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
   The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.

--- a/ProgTutorial/General.thy	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 10 18:25:43 2009 +0200
@@ -787,7 +787,7 @@
     }
   \]
 
-  While we obtained a theorem as the result, this theorem is not
+  While we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced later on. One way to store it in the theorem database is
   by using the function @{ML_ind note in LocalTheory}.
@@ -798,8 +798,23 @@
      ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 
 text {*
-  Now it can be referenced with the \isacommand{thm}-command on the user-level 
-  of Isabelle
+  The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
+  classifies the theorem. For a theorem arising from a definition we should
+  state @{ML_ind definitionK in Thm}, instead. The second argument is the 
+  name under which we stroe the theorem or theorems. The third contains is 
+  a list of (theorem) attributes. Above it is empty, but if we want to store
+  the therem and at the same time add it to the simpset we have to declare.
+*}
+
+local_setup %gray {*
+  LocalTheory.note Thm.theoremK
+     ((@{binding "my_thm_simp"}, [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
+
+
+
+text {*
+  Now @{thm [source] my_thm} can be referenced with the \isacommand{thm}-command 
+  on the user-level of Isabelle
 
   \begin{isabelle}
   \isacommand{thm}~@{text "my_thm"}\isanewline

--- a/ProgTutorial/Tactical.thy	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Oct 10 18:25:43 2009 +0200
@@ -1246,7 +1246,7 @@
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
-  val {simps, congs, procs, ...} = Simplifier.dest_ss ss
+  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
       "  " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm)
@@ -1263,7 +1263,7 @@
 text_raw {* 
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML_ind  dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}

--- a/ProgTutorial/document/root.tex	Sat Oct 10 15:16:44 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sat Oct 10 18:25:43 2009 +0200
@@ -16,8 +16,10 @@
 \usepackage{flafter}
 \usepackage{makeidx}
 \usepackage{tocbibind}
+\usepackage{index}
 \usepackage{pdfsetup}
 
+
 \urlstyle{rm}
 \renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
 \renewcommand{\isastyleminor}{\tt\slshape}%

Binary file progtutorial.pdf has changed