1 

     2 theory NamedThms

     3 imports Main

     4 begin

     5 

     6 

     7 section {* Accumulate a List of Theorems under a Name *} 

     8 

     9 

    10 text {*

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

    12 

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

    14   which are then used by some method.

    15 

    16   \paragraph{Solution:}

    17 

    18   *}

    19 ML {*

    20   structure FooRules = NamedThmsFun(

    21     val name = "foo" 

    22     val description = "Rules for foo"

    23   );

    24 *}

    25 

    26 setup FooRules.setup

    27 

    28 text {*

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

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

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

    32   modify the facts.

    33 

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

    35   @{text foo}:

    36 *}

    37 

    38 lemma rule1[foo]: "A" sorry

    39 lemma rule2[foo]: "B" sorry

    40 

    41 declare rule1[foo del]

    42 

    43 thm foo

    44 

    45 ML {* 

    46   FooRules.get @{context};

    47 *}

    48 

    49 

    50 text {* 

    51   \begin{readmore}

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

    53   \end{readmore}

    54  *}

    55 

    56 

    57 end

    58   

    59 

    60 

    61