CookBook/Recipes/NamedThms.thy
changeset 69 19106a9975c1
parent 68 e7519207c2b7
child 72 7b8c4fe235aa
equal deleted inserted replaced
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