equal
deleted
inserted
replaced
26 setup FooRules.setup |
26 setup FooRules.setup |
27 |
27 |
28 text {* |
28 text {* |
29 This declares a context data slot where the theorems are stored, |
29 This declares a context data slot where the theorems are stored, |
30 an attribute @{attribute foo} (with the usual @{text add} and @{text del} options |
30 an attribute @{attribute foo} (with the usual @{text add} and @{text del} options |
31 to declare new rules, and the internal ML interface to retrieve and |
31 to declare new rules) and the internal ML interface to retrieve and |
32 modify the facts. |
32 modify the facts. |
33 |
33 |
34 Furthermore, the facts are made available under the dynamic fact name |
34 Furthermore, the facts are made available under the dynamic fact name |
35 @{text foo}: |
35 @{text foo}: |
36 *} |
36 *} |