changeset 69 | 19106a9975c1 |
parent 68 | e7519207c2b7 |
child 72 | 7b8c4fe235aa |
68:e7519207c2b7 | 69:19106a9975c1 |
---|---|
15 |
15 |
16 Named theorem lists can be set up using the code |
16 Named theorem lists can be set up using the code |
17 |
17 |
18 *} |
18 *} |
19 |
19 |
20 ML {* |
20 ML{*structure FooRules = NamedThmsFun ( |
21 structure FooRules = NamedThmsFun ( |
|
22 val name = "foo" |
21 val name = "foo" |
23 val description = "Rules for foo"); |
22 val description = "Rules for foo"); *} |
24 *} |
|
25 |
23 |
26 text {* |
24 text {* |
27 and the command |
25 and the command |
28 *} |
26 *} |
29 |
27 |