--- 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)
*}