--- 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