1 

     2 theory NamedThms

     3 imports Main

     4 begin

     5 

     6 

     7 chapter {* Recipes *}

     8 

     9 text_raw {* 

    10 

    11 \section*{Accumulate a list of theorems under a name} 

    12 *}

    13 

    14 text {*

    15   \paragraph{Problem:} Your tool @{text foo} works with special rules, called @{text foo}-rules.

    16 

    17   Users should be able to declare @{text foo}-rules in the theory,

    18   which are then used by some method.

    19 

    20   \paragraph{Solution:}

    21 

    22   *}

    23 ML {*

    24   structure FooRules = NamedThmsFun(

    25     val name = "foo" 

    26     val description = "Rules for foo"

    27   );

    28 *}

    29 

    30 setup FooRules.setup

    31 

    32 text {*

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

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

    35   to declare new rules, and the internal ML interface to retrieve and 

    36   modify the facts.

    37 

    38   Furthermore, the facts are made available under the dynamic fact name

    39   @{text foo}:

    40 *}

    41 

    42 lemma rule1[foo]: "A" sorry

    43 lemma rule2[foo]: "B" sorry

    44 

    45 declare rule1[foo del]

    46 

    47 thm foo

    48 

    49 ML {* 

    50   FooRules.get @{context};

    51 *}

    52 

    53 

    54 text {* 

    55   \begin{readmore}

    56   For more information see @{ML_file "Pure/Tools/named_thms.ML"}.

    57   \end{readmore}

    58  *}

    59 

    60 

    61 end

    62   

    63 

    64 

    65