1 

     2 theory NamedThms

     3 imports Main

     4 begin

     5 

     6 text_raw {* 

     7 \newpage

     8 

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

    10 *}

    11 

    12 text {*

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

    14 

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

    16   which are then used by some method.

    17 

    18   \paragraph{Solution:}

    19 

    20   *}

    21 ML {*

    22   structure FooRules = NamedThmsFun(

    23     val name = "foo" 

    24     val description = "Rules for foo"

    25   );

    26 *}

    27 

    28 setup FooRules.setup

    29 

    30 text {*

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

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

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

    34   modify the facts.

    35 

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

    37   @{text foo}:

    38 *}

    39 

    40 lemma rule1[foo]: "A" sorry

    41 lemma rule2[foo]: "B" sorry

    42 

    43 declare rule1[foo del]

    44 

    45 thm foo

    46 

    47 ML {* 

    48   FooRules.get @{context};

    49 *}

    50 

    51 

    52 text {* 

    53   \begin{readmore}

    54   XXX

    55 

    56   \end{readmore}

    57  *}

    58 

    59 

    60 end

    61   

    62 

    63 

    64