diff -r 5fc2fb34c323 -r dc76ba24e81b ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri Jan 08 21:31:45 2010 +0100
+++ b/ProgTutorial/Essential.thy	Thu Jan 14 22:10:04 2010 +0100
@@ -1156,19 +1156,24 @@
   @{text i} in the next line. In Lines 5 and 6 we destruct the resulting 
   environments using the function @{ML_ind dest in Vartab}. Finally, we need 
   to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective 
-  environments (Line 8). As a simple example we instantiate the 
-  @{thm [source] conjI}-rule as follows
-
-  @{ML_response_fake [gray,display] 
+  environments (Line 8). As a simple example we instantiate the
+  @{thm [source] spec} rule so that its conclusion is of the form 
+  @{term "Q True"}. 
+ 
+
+  @{ML_response_fake [gray,display,linenos] 
   "let  
   val pat = Logic.strip_imp_concl (prop_of @{thm spec})
-  val trm = @{term \"Trueprop (P True)\"}
+  val trm = @{term \"Trueprop (Q True)\"}
   val inst = matcher_inst @{theory} pat trm 1
 in
-  Drule.instantiate inst @{thm conjI}
+  Drule.instantiate inst @{thm spec}
 end"
-  "\<forall>x. P x \<Longrightarrow> P True"}
-
+  "\<forall>x. Q x \<Longrightarrow> Q True"}
+
+  Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the 
+  conclusion of @{thm [source] spec} contains one.
+ 
   \begin{readmore}
   Unification and matching of higher-order patterns is implemented in 
   @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
@@ -1263,8 +1268,6 @@
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 
-  \footnote{\bf FIXME: say something about sorts.}
-  \footnote{\bf FIXME: give a ``readmore''.}
 
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
@@ -1380,7 +1383,7 @@
   The corresponding ML-code is as follows:
 *}
 
-ML{*val my_thm = 
+ML %linenosgray{*val my_thm = 
 let
   val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
   val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
@@ -1397,6 +1400,9 @@
 end*}
 
 text {*
+  Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which
+  inserts necessary @{text "Trueprop"}s.
+
   If we print out the value of @{ML my_thm} then we see only the 
   final statement of the theorem.
 
@@ -1424,7 +1430,7 @@
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
   by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
-  to the section about local-setup is given earlier.}
+  to the section about local-setup is given here.}
 *}
 
 local_setup %gray {*
@@ -1468,8 +1474,9 @@
 
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "my_thm"}\isanewline
-   @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+  \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
+  @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\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. Otherwise the 
@@ -1544,7 +1551,7 @@
   we still obtain the same list. The reason is that we used the function @{ML_ind
   add_thm in Thm} in our update function. This is a dedicated function which
   tests whether the theorem is already in the list.  This test is done
-  according to alpha-equivalence of the proposition behind the theorem. The
+  according to alpha-equivalence of the proposition of the theorem. The
   corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
   Suppose you proved the following three theorems.
 *}
@@ -1603,7 +1610,9 @@
 Premises: 
 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 
-  Note that in the second case, there is no premise.
+  Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}
+  separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication
+  from HOL, which just constructs a formula.
 
   \begin{readmore}
   The basic functions for theorems are defined in
@@ -1714,6 +1723,12 @@
   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
   "True = False"}
 
+  \begin{readmore}
+  Functions that setup goal states and prove theorems are implemented in 
+  @{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
+  skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.
+  \end{readmore}
+
   Theorems also contain auxiliary data, such as the name of the theorem, its
   kind, the names for cases and so on. This data is stored in a string-string
   list and can be retrieved with the function @{ML_ind get_tags in