29 |
29 |
30 @{ML_text [display] "setup FooRules.setup"} |
30 @{ML_text [display] "setup FooRules.setup"} |
31 |
31 |
32 This code declares a context data slot where the theorems are stored, |
32 This code declares a context data slot where the theorems are stored, |
33 an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options |
33 an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options |
34 to adding and deleting theorems) and an internal ML interface to retrieve and |
34 for adding and deleting theorems) and an internal ML interface to retrieve and |
35 modify the theorems. |
35 modify the theorems. |
36 |
36 |
37 Furthermore, the facts are made available on the user level under the dynamic |
37 Furthermore, the facts are made available on the user level under the dynamic |
38 fact name @{text foo}. For example we can declare two lemmas to be of the kind |
38 fact name @{text foo}. For example we can declare three lemmas to be of the kind |
39 @{ML_text foo}: |
39 @{ML_text foo} by: |
40 *} |
40 *} |
41 |
41 |
42 lemma rule1[foo]: "A" sorry |
42 lemma rule1[foo]: "A" sorry |
43 lemma rule2[foo]: "B" sorry |
43 lemma rule2[foo]: "B" sorry |
44 lemma rule3[foo]: "C" sorry |
44 lemma rule3[foo]: "C" sorry |
45 |
45 |
46 text {* undeclare them: *} |
46 text {* and undeclare the first one by: *} |
47 |
47 |
48 declare rule1[foo del] |
48 declare rule1[foo del] |
49 |
49 |
50 text {* and query them: *} |
50 text {* and query the remaining ones by: *} |
51 |
51 |
52 thm foo |
52 thm foo |
53 |
53 |
54 text {* |
54 text {* |
55 In an ML-context the rules marked with @{ML_text "foo"} an be retrieved |
55 On the ML-level the rules marked with @{ML_text "foo"} an be retrieved |
56 using |
56 using the function @{ML FooRules.get}: |
57 |
57 |
58 @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
58 @{ML_response_fake [display] "FooRules.get @{context}" "[\"?C\",\"?B\"]"} |
59 |
59 |
60 \begin{readmore} |
60 \begin{readmore} |
61 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
61 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |