20 ML {*

    20 ML {*

    21 structure FooRules = NamedThmsFun (

    21 structure FooRules = NamedThmsFun (

    22   val name = "foo" 

    22   val name = "foo" 

    23   val description = "Rules for foo");

    23   val description = "Rules for foo");

    24 *}

    24 *}

    26 

    25 

    27 text {*

    26 text {*

    28   and the command

    27   and the command

    29 

    29 

    31 

    31 

    32   This code declares a context data slot where the theorems are stored,

    33   This code declares a context data slot where the theorems are stored,

    33   an attribute @{text foo} (with the usual @{text add} and @{text del} options

    34   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 

    35   for adding and deleting theorems) and an internal ML interface to retrieve and 

    35   modify the theorems.

    36   modify the theorems.

    36 

    37