--- a/ProgTutorial/General.thy	Thu Nov 12 20:35:14 2009 +0100
+++ b/ProgTutorial/General.thy	Sun Nov 15 13:18:07 2009 +0100
@@ -213,6 +213,22 @@
 
 ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
 
+(*
+classes s
+
+ML {* @{typ "bool \<Rightarrow> ('a::s)"} *}
+
+ML {* 
+fun test ty =
+  case ty of
+    TVar ((v, n), s) => Pretty.block [Pretty.str "TVar "]
+  | TFree (x, s) => Pretty.block [Pretty.str "TFree "]
+  | Type (s, tys) => Pretty.block [Pretty.str "Type "]
+*}
+
+ML {* toplevel_pp ["typ"] "test" *}
+*)
+
 text {*
   Now the type bool is printed out in full detail.
 
@@ -1273,7 +1289,7 @@
 text {*
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
   that can only be built by going through interfaces. As a consequence, every proof 
-  in Isabelle is correct by construction. This follows the tradition of the LCF approach.
+  in Isabelle is correct by construction. This follows the tradition of the LCF-approach.
 
 
   To see theorems in ``action'', let us give a proof on the ML-level for the following 
@@ -1518,7 +1534,9 @@
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
-  The simplifier can be used to unfold definition in theorems. To show
+  Although we will explain the simplifier in more detail as tactic in 
+  Section~\ref{sec:simplifier}, the simplifier 
+  can be used to work directly over theorems, for example to unfold definitions. To show
   this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
   unfold the constant @{term "True"} according to its definition (Line 2).
 
@@ -1585,6 +1603,8 @@
   "atomize_thm @{thm list.induct}"
   "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 
+  \footnote{\bf FIXME: say someting about @{ML_ind standard in Drule}.}
+
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
   in the structure @{ML_struct Goal}. For example below we use this function
@@ -1607,6 +1627,20 @@
   by assumption. As before this code will produce a theorem, but the theorem
   is not yet stored in the theorem database. 
 
+  While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
+  is the function @{ML_ind make_thm in Skip_Proof} in the structure 
+  @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
+  Potentially making the system unsound.  This is sometimes useful for developing 
+  purposes, or when explicit proof construction should be omitted due to performace 
+  reasons. An example of this function is as follows:
+
+  @{ML_response_fake [display, gray]
+  "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
+  "True = False"}
+
+  The function @{ML make_thm in Skip_Proof} however only works if 
+  the ``quick-and-dirty'' mode is switched on. 
+
   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
@@ -2481,7 +2515,13 @@
   @{ML_ind "Binding.name_of"} returns the string without markup
 *}
 
-
+section {* Concurrency (TBD) *}
+
+text {*
+  @{ML_ind prove_future in Goal}
+  @{ML_ind future_result in Goal}
+  @{ML_ind fork_pri in Future}
+*}
 
 section {* Summary *}