equal
deleted
inserted
replaced
23 |
23 |
24 setup FooRules.setup |
24 setup FooRules.setup |
25 |
25 |
26 text {* |
26 text {* |
27 This code declares a context data slot where the theorems are stored, |
27 This code declares a context data slot where the theorems are stored, |
28 an attribute @{attribute foo} (with the usual @{text add} and @{text del} options |
28 an attribute @{ML_text foo} (with the usual @{ML_text add} and @{ML_text del} options |
29 to adding and deleting theorems) and an internal ML interface to retrieve and |
29 to adding and deleting theorems) and an internal ML interface to retrieve and |
30 modify the theorems. |
30 modify the theorems. |
31 |
31 |
32 Furthermore, the facts are made available on the user level under the dynamic |
32 Furthermore, the facts are made available on the user level under the dynamic |
33 fact name @{text foo}. For example: |
33 fact name @{text foo}. For example: |
39 declare rule1[foo del] |
39 declare rule1[foo del] |
40 |
40 |
41 thm foo |
41 thm foo |
42 |
42 |
43 text {* |
43 text {* |
44 In an ML-context the rules marked with @{text "foo"} an be retrieved |
44 In an ML-context the rules marked with @{ML_text "foo"} an be retrieved |
45 using |
45 using |
46 *} |
46 *} |
47 |
47 |
48 ML {* FooRules.get @{context} *} |
48 ML {* FooRules.get @{context} *} |
49 |
49 |