961 names for cases etc. This data is stored in a string-string list and can |
961 names for cases etc. This data is stored in a string-string list and can |
962 be retrieved with the function @{ML_ind get_tags in Thm}. Assume the |
962 be retrieved with the function @{ML_ind get_tags in Thm}. Assume the |
963 following lemma. |
963 following lemma. |
964 *} |
964 *} |
965 |
965 |
966 lemma foo_data: "P \<Longrightarrow> P" by assumption |
966 lemma foo_data: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
967 |
967 |
968 text {* |
968 text {* |
969 The auxiliary data of this lemma is as follows. |
969 The auxiliary data of this lemma is as follows. |
970 |
970 |
971 @{ML_response_fake [display,gray] |
971 @{ML_response_fake [display,gray] |
972 "Thm.get_tags @{thm foo_data}" |
972 "Thm.get_tags @{thm foo_data}" |
973 " [(\"name\", \"FirstSteps.foo_data\"), (\"kind\", \"lemma\")]"} |
973 "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"} |
974 *} |
974 |
975 |
975 We can extend the data associated with this lemma by attaching case names. |
976 |
976 *} |
977 local_setup {* |
977 |
978 LocalTheory.note Thm.theoremK |
978 local_setup %gray {* |
979 ((@{binding "rr2"}, []), [(RuleCases.name ["a"] @{thm foo_data})]) #> snd *} |
979 LocalTheory.note Thm.lemmaK |
980 |
980 ((@{binding "foo_data'"}, []), |
981 ML {* Thm.get_tags @{thm rr2} *} |
981 [(RuleCases.name ["foo_case1", "foo_case2"] |
|
982 @{thm foo_data})]) #> snd *} |
|
983 |
|
984 text {* |
|
985 The date of the theorem @{thm [source] foo_data'} is as follows: |
|
986 |
|
987 @{ML_response_fake [display,gray] |
|
988 "Thm.get_tags @{thm foo_data'}" |
|
989 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), |
|
990 (\"case_names\", \"foo_case1;foo_case2\")]"} |
|
991 *} |
982 |
992 |
983 lemma |
993 lemma |
984 "Q \<Longrightarrow> Q" |
994 "Q \<Longrightarrow> Q \<Longrightarrow> Q" |
985 proof (induct rule: rr2) |
995 proof (induct rule: foo_data') |
986 oops |
996 (*<*)oops(*>*) |
987 |
997 |
988 text {* |
998 text {* |
989 TBD below. |
999 TBD below |
990 |
|
991 |
|
992 (FIXME: how to add case-names to goal states - maybe in the |
|
993 next section) |
|
994 |
1000 |
995 (FIXME: example for how to add theorem styles) |
1001 (FIXME: example for how to add theorem styles) |
996 *} |
1002 *} |
997 |
1003 |
998 ML {* |
1004 ML {* |