equal
deleted
inserted
replaced
1 theory NamedThms |
1 theory NamedThms |
2 imports Base |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Accumulate a List of Theorems under a Name *} |
5 section {* Accumulate a List of Theorems under a Name *} |
6 |
6 |
7 |
7 |
25 (*<*)setup FooRules.setup(*>*) |
25 (*<*)setup FooRules.setup(*>*) |
26 |
26 |
27 text {* |
27 text {* |
28 and the command |
28 and the command |
29 |
29 |
30 @{ML_text [display] "setup FooRules.setup"} |
30 @{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 @{text foo} (with the usual @{text add} and @{text del} options |
34 for 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 three 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} by: |
39 @{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 |
50 text {* and query the remaining ones by: *} |
50 text {* and query the remaining ones by: *} |
51 |
51 |
52 thm foo |
52 thm foo |
53 |
53 |
54 text {* |
54 text {* |
55 On the ML-level the rules marked with @{ML_text "foo"} an be retrieved |
55 On the ML-level the rules marked with @{text "foo"} an be retrieved |
56 using the function @{ML FooRules.get}: |
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} |