--- a/ProgTutorial/General.thy	Sun Oct 11 01:47:15 2009 +0200
+++ b/ProgTutorial/General.thy	Sun Oct 11 16:30:59 2009 +0200
@@ -963,34 +963,40 @@
   following lemma. 
 *}
 
-lemma foo_data: "P \<Longrightarrow> P" by assumption
+lemma foo_data: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
 
 text {*
   The auxiliary data of this lemma is as follows. 
 
   @{ML_response_fake [display,gray]
   "Thm.get_tags @{thm foo_data}"
-  " [(\"name\", \"FirstSteps.foo_data\"), (\"kind\", \"lemma\")]"}
+  "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
+
+  We can extend the data associated with this lemma by attaching case names.  
 *}
 
+local_setup %gray {*
+  LocalTheory.note Thm.lemmaK
+    ((@{binding "foo_data'"}, []), 
+      [(RuleCases.name ["foo_case1", "foo_case2"] 
+        @{thm foo_data})]) #> snd *}
 
-local_setup {*
-  LocalTheory.note Thm.theoremK
-      ((@{binding "rr2"}, []), [(RuleCases.name ["a"] @{thm foo_data})]) #> snd *}
+text {*
+  The date of the theorem @{thm [source] foo_data'} is as follows:
 
-ML {* Thm.get_tags @{thm rr2} *}
+  @{ML_response_fake [display,gray]
+  "Thm.get_tags @{thm foo_data'}"
+  "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
+ (\"case_names\", \"foo_case1;foo_case2\")]"}
+*}
 
 lemma
-  "Q \<Longrightarrow> Q"
-proof (induct rule: rr2)
-oops
+  "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+proof (induct rule: foo_data')
+(*<*)oops(*>*)
 
 text {*
-  TBD below.
-
-
-  (FIXME: how to add case-names to goal states - maybe in the 
-  next section)
+  TBD below
 
   (FIXME: example for how to add theorem styles)
 *}

--- a/ProgTutorial/Package/Ind_Code.thy	Sun Oct 11 01:47:15 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Oct 11 16:30:59 2009 +0200
@@ -37,7 +37,8 @@
   It returns the definition (as a theorem) and the local theory in which the
   definition has been made. In Line 4, @{ML_ind  internalK in Thm} is a flag
   attached to the theorem (other possibile flags are @{ML_ind  definitionK in Thm}
-  and @{ML_ind  axiomK in Thm}). These flags just classify theorems and have no
+  and @{ML_ind  axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.} 
+  These flags just classify theorems and have no
   significant meaning, except for tools that, for example, find theorems in
   the theorem database.\footnote{FIXME: put in the section about theorems.} We
   also use @{ML_ind  empty_binding in Attrib} in Line 3, since the definitions for

--- a/ProgTutorial/document/root.tex	Sun Oct 11 01:47:15 2009 +0200
+++ b/ProgTutorial/document/root.tex	Sun Oct 11 16:30:59 2009 +0200
@@ -15,8 +15,8 @@
 \usepackage{mathpartir}
 \usepackage{flafter}
 \usepackage{makeidx}
+\usepackage{index}
 \usepackage{tocbibind}
-\usepackage{index}
 \usepackage{pdfsetup}
 
 

Binary file progtutorial.pdf has changed