--- a/ProgTutorial/General.thy	Sat Oct 10 18:25:43 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 10 20:27:51 2009 +0200
@@ -801,20 +801,35 @@
   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 
+  name under which we store the theorem or theorems. The third can contain 
   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.
+  the theorem 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 *}
-
-
+     ((@{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
+  Note that we have to use another name for the theorem, since Isabelle does
+  not allow to add another theorem under the same name.  The attribute can be
+  given @{ML_ind internal in Attrib}. If we use the function @{ML
+  get_thm_names_from_ss} from the previous chapter, we can check whether the
+  theorem has been added.
+
+  @{ML_response [display,gray]
+  "let
+  fun pred s = match_string \"my_thm_simp\" s
+in
+  exists pred (get_thm_names_from_ss @{simpset})
+end"
+  "true"}
+
+  Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can 
+  also be referenced  with the \isacommand{thm}-command on the user-level of 
+  Isabelle
 
   \begin{isabelle}
   \isacommand{thm}~@{text "my_thm"}\isanewline
@@ -823,8 +838,8 @@
 
   or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
   theorem does not have any meta-variables that would be present if we proved
-  this theorem on the user-level. As we shall see later on, we have to provide
-  this information explicitly.
+  this theorem on the user-level. As we shall see later on, we have to construct
+  meta-variables explicitly.
 
   There is a multitude of functions that manage or manipulate theorems. For example 
   we can test theorems for (alpha) equality. Suppose you proved the following three 
@@ -844,9 +859,9 @@
  Thm.eq_thm (@{thm thm2}, @{thm thm3}))"
 "(true, false)"}
 
-  Many functions destruct a theorem into a @{ML_type cterm}. For example
-  @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return the left and
-  righ-hand side, respectively, of a meta-equality.
+  Many functions destruct theorems into @{ML_type cterm}s. For example
+  the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 
+  the left and right-hand side, respectively, of a meta-equality.
 
   @{ML_response_fake [display,gray]
   "let
@@ -858,7 +873,7 @@
   "True
 (\<lambda>x. x) = (\<lambda>x. x)"}
 
-  Other function produce immediately a term that can be pattern-matched. 
+  Other function produce terms that can be pattern-matched. 
   Suppose the following theorem.
 *}
 
@@ -866,6 +881,8 @@
   shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry
 
 text {*
+  We can deconstruct it into premises and conclusion. 
+
  @{ML_response_fake [display,gray]
 "let
   val thm = @{thm foo_test}
@@ -882,6 +899,8 @@
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
+  TBD below.
+
   (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 
 
   (FIXME: @{ML_ind prove in Goal})