--- a/ProgTutorial/General.thy	Fri Oct 09 10:34:38 2009 +0200
+++ b/ProgTutorial/General.thy	Sat Oct 10 15:16:44 2009 +0200
@@ -747,7 +747,8 @@
   The corresponding ML-code is as follows:
 *}
 
-ML{*val my_thm = let
+ML{*val my_thm = 
+let
   val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
   val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
 
@@ -767,8 +768,7 @@
   final statement of the theorem.
 
   @{ML_response_fake [display, gray]
-  "string_of_thm @{context} my_thm 
- |> tracing"
+  "string_of_thm @{context} my_thm |> tracing"
   "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
   However, internally the code-snippet constructs the following 
@@ -787,12 +787,13 @@
     }
   \]
 
-  While we obtained a theorem as result, this theorem is not
-  yet stored in Isabelle's theorem database. So it cannot be referenced later
-  on. One way to store it is 
+  While we obtained a theorem as the 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}.
 *}
 
-local_setup %gray{*
+local_setup %gray {*
   LocalTheory.note Thm.theoremK
      ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 
@@ -806,9 +807,59 @@
   \end{isabelle}
 
   or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
-  theorem does not have the meta-variables that would be present if we stated
-  this theorem on the user-level.
+  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.
+
+  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 
+  facts.
+*}
+
+lemma
+  shows thm1: "\<forall>x. P x" 
+  and   thm2: "\<forall>y. P y" 
+  and   thm3: "\<forall>y. Q y" sorry
+
+text {*
+  Testing for equality using the function @{ML_ind eq_thm in Thm} produces:
+
+  @{ML_response [display,gray]
+"(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
+ 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.
 
+  @{ML_response_fake [display,gray]
+  "let
+  val eq = @{thm True_def}
+in
+  (Thm.lhs_of eq, Thm.rhs_of eq) 
+  |> pairself (tracing o string_of_cterm @{context})
+end"
+  "True
+(\<lambda>x. x) = (\<lambda>x. x)"}
+
+  Other function produce immediately a term that can be pattern-matched. 
+  Suppose the following theorem.
+*}
+
+lemma foo_test: 
+  shows "A \<Longrightarrow> B \<Longrightarrow> C" sorry
+
+text {*
+ @{ML_response_fake [display,gray]
+"let
+  val thm = @{thm foo_test}
+in
+  (Thm.prems_of thm, [Thm.concl_of thm]) 
+  |> pairself (tracing o string_of_terms @{context})
+end"
+"?A, ?B
+?C"}
 
   \begin{readmore}
   For the functions @{text "assume"}, @{text "forall_elim"} etc