--- a/ProgTutorial/General.thy	Wed Oct 14 12:33:38 2009 +0200
+++ b/ProgTutorial/General.thy	Wed Oct 14 14:56:19 2009 +0200
@@ -857,6 +857,8 @@
   the theorem does not have any meta-variables that would be present if we proved
   this theorem on the user-level. We will see later on that usually we have to 
   construct meta-variables in theorems explicitly.
+
+  \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
 *}
 
 text {*
@@ -963,11 +965,11 @@
   a meta-equation between the given theorem and the theorem transformed
   into the object logic. The result is the theorem with object logic 
   connectives. However, in order to completely transform a theorem
-  such as @{thm [source] list.induct}
+  such as @{thm [source] list.induct}, which is of the form 
 
   @{thm [display] list.induct}
 
-  we have to first abstract over the variables @{text "?P"} and 
+  we have to first abstract over the meta variables @{text "?P"} and 
   @{text "?list"}. For this we can use the function 
   @{ML_ind forall_intr_vars in Drule}. 
 *}
@@ -981,7 +983,7 @@
 end*}
 
 text {*
-  For @{thm [source] list.induct} it produces:
+  For the theorem @{thm [source] list.induct}, this function produces:
 
   @{ML_response_fake [display, gray]
   "atomize_thm @{thm list.induct}"
@@ -989,7 +991,7 @@
 
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achive this is by using the function @{ML_ind prove in Goal}. 
-  For example
+  For example below we prove the term @{term "P \<Longrightarrow> P"}.
   
   @{ML_response_fake [display,gray]
   "let
@@ -1002,8 +1004,9 @@
 
   This function takes as second argument a list of strings. This list specifies
   which variables should be turned into meta-variables once the term is proved.
-  The proof is given in form of a tactic. We explain tactics in 
-  Chapter~\ref{chp:tactical}. 
+  The proof is given in form of a tactic as last argument. We explain tactics in 
+  Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem 
+  by assumption.
 
   Theorems also contain auxiliary data, such their names and kind, but also 
   names for cases etc. This data is stored in a string-string list and can
@@ -1020,7 +1023,8 @@
   "Thm.get_tags @{thm foo_data}"
   "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
 
-  We can extend the data associated with this lemma by attaching case names.  
+  When we store lemmas in the theorem database, we can explicitly extend the data 
+  associated with this lemma by attaching case names.  
 *}
 
 local_setup %gray {*
@@ -1030,22 +1034,42 @@
         @{thm foo_data})]) #> snd *}
 
 text {*
-  The date of the theorem @{thm [source] foo_data'} is as follows:
+  The data of the theorem @{thm [source] foo_data'} is then as follows:
 
   @{ML_response_fake [display,gray]
   "Thm.get_tags @{thm foo_data'}"
   "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
  (\"case_names\", \"foo_case1;foo_case2\")]"}
+
+  You notice the difference when using the proof methods @{ML_text cases} 
+  or @{ML_text induct}. In the proof below
 *}
 
 lemma
   "Q \<Longrightarrow> Q \<Longrightarrow> Q"
-proof (induct rule: foo_data')
+proof (cases rule: foo_data')
+print_cases
+(*<*)oops(*>*)
+
+text {*
+  we can proceed by analysing the cases @{ML_text "foo_case1"} and 
+  @{ML_text "foo_case2"}. While if the theorem has no names, then
+  the cases have standard names @{ML_text 1}, @{ML_text 2} and so 
+  on. This can be seen in the proof below.
+*}
+
+lemma
+  "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+proof (cases rule: foo_data)
+print_cases
 (*<*)oops(*>*)
 
 text {*
   TBD below
 
+  One great feature of Isabelle is its document preparation system where
+  proved theorems can be quoted in the text directly from the formalisation. 
+
   (FIXME: example for how to add theorem styles)
 *}
 
@@ -1068,11 +1092,12 @@
 strip_assums_all ([], @{term "\<And>x y. A x y"})
 *}
 
+(*
 setup %gray {*
   TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
   TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
 *}
-
+*)
 lemma 
   shows "A \<Longrightarrow> B"
   and   "C \<Longrightarrow> D"
@@ -1376,14 +1401,6 @@
 
 section {* Local Theories (TBD) *}
 
-section {* Storing Theorems\label{sec:storing} (TBD) *}
-
-text {* @{ML_ind  add_thms_dynamic in PureThy} *}
-
-local_setup %gray {* 
-  LocalTheory.note Thm.theoremK 
-    ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
-
 
 (*
 setup {*
@@ -1738,5 +1755,15 @@
 
 section {* Managing Name Spaces (TBD) *}
 
+section {* Summary *}
+
+text {*
+  \begin{conventions}
+  \begin{itemize}
+  \item Start with a proper context and then pass it around 
+  through all your functions.
+  \end{itemize}
+  \end{conventions}
+*}
 
 end