diff -r 62dea749d5ed -r 930b1308fd96 ProgTutorial/General.thy
--- 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)
 *}