--- a/ProgTutorial/General.thy	Thu Oct 08 21:49:11 2009 +0200
+++ b/ProgTutorial/General.thy	Fri Oct 09 10:34:38 2009 +0200
@@ -745,24 +745,34 @@
 
 text {*
   The corresponding ML-code is as follows:
+*}
 
-@{ML_response_fake [display,gray]
-"let
-  val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
-  val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
+ML{*val my_thm = let
+  val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
+  val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
 
   val Pt_implies_Qt = 
         assume assm1
-        |> forall_elim @{cterm \"t::nat\"};
+        |> forall_elim @{cterm "t::nat"}
   
-  val Qt = implies_elim Pt_implies_Qt (assume assm2);
+  val Qt = implies_elim Pt_implies_Qt (assume assm2)
 in
   Qt 
   |> implies_intr assm2
   |> implies_intr assm1
-end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+end*}
+
+text {* 
+  If we print out the value of @{ML my_thm} then we see only the 
+  final statement of the theorem.
 
-  This code-snippet constructs the following proof:
+  @{ML_response_fake [display, gray]
+  "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 
+  proof.
 
   \[
   \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
@@ -777,14 +787,33 @@
     }
   \]
 
-  However, while we obtained a theorem as result, this theorem is not
+  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. How to store theorems will be explained in Section~\ref{sec:storing}.
+  on. One way to store it is 
+*}
+
+local_setup %gray{*
+  LocalTheory.note Thm.theoremK
+     ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+
+text {*
+  Now it can be referenced with the \isacommand{thm}-command on the user-level 
+  of Isabelle
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "my_thm"}\isanewline
+   @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+  \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.
+
 
   \begin{readmore}
   For the functions @{text "assume"}, @{text "forall_elim"} etc 
   see \isccite{sec:thms}. The basic functions for theorems are defined in
-  @{ML_file "Pure/thm.ML"}. 
+  @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
   (FIXME: handy functions working on theorems, like @{ML_ind  rulify in ObjectLogic} and so on) 

Binary file progtutorial.pdf has changed