equal
deleted
inserted
replaced
7 |
7 |
8 section {* Accumulate a List of Theorems under a Name *} |
8 section {* Accumulate a List of Theorems under a Name *} |
9 |
9 |
10 |
10 |
11 text {* |
11 text {* |
12 \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules. |
12 {\bf Problem:} |
|
13 Your tool @{text foo} works with special rules, called @{text foo}-rules. |
|
14 Users should be able to declare @{text foo}-rules in the theory, |
|
15 which are then used by some method.\smallskip |
13 |
16 |
14 Users should be able to declare @{text foo}-rules in the theory, |
17 {\bf Solution:} This can be achieved using |
15 which are then used by some method. |
|
16 |
|
17 \paragraph{Solution:} |
|
18 |
18 |
19 *} |
19 *} |
20 ML {* |
20 ML {* |
21 structure FooRules = NamedThmsFun( |
21 structure FooRules = NamedThmsFun( |
22 val name = "foo" |
22 val name = "foo" |
25 *} |
25 *} |
26 |
26 |
27 setup FooRules.setup |
27 setup FooRules.setup |
28 |
28 |
29 text {* |
29 text {* |
30 This declares a context data slot where the theorems are stored, |
30 This code declares a context data slot where the theorems are stored, |
31 an attribute @{attribute foo} (with the usual @{text add} and @{text del} options |
31 an attribute @{attribute foo} (with the usual @{text add} and @{text del} options |
32 to declare new rules) and the internal ML interface to retrieve and |
32 to adding and deleting theorems) and an internal ML interface to retrieve and |
33 modify the facts. |
33 modify the theorems. |
34 |
34 |
35 Furthermore, the facts are made available under the dynamic fact name |
35 Furthermore, the facts are made available on the user level under the dynamic |
36 @{text foo}: |
36 fact name @{text foo}. For example: |
37 *} |
37 *} |
38 |
38 |
39 lemma rule1[foo]: "A" sorry |
39 lemma rule1[foo]: "A" sorry |
40 lemma rule2[foo]: "B" sorry |
40 lemma rule2[foo]: "B" sorry |
41 |
41 |
42 declare rule1[foo del] |
42 declare rule1[foo del] |
43 |
43 |
44 thm foo |
44 thm foo |
45 |
45 |
46 ML {* |
46 text {* |
47 FooRules.get @{context}; |
47 In an ML-context the rules marked with @{text "foo"} an be retrieved |
|
48 using |
48 *} |
49 *} |
|
50 |
|
51 ML {* FooRules.get @{context} *} |
49 |
52 |
50 |
53 |
51 text {* |
54 text {* |
52 \begin{readmore} |
55 \begin{readmore} |
53 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |
56 For more information see @{ML_file "Pure/Tools/named_thms.ML"}. |