theory NamedThms

imports Main

begin

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

text {*

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

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

  which are then used by some method.

  \paragraph{Solution:}

  *}

ML {*

  structure FooRules = NamedThmsFun(

    val name = "foo" 

    val description = "Rules for foo"

  );

*}

setup FooRules.setup

text {*

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

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

  to declare new rules) and the internal ML interface to retrieve and 

  modify the facts.

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

  @{text foo}:

*}

lemma rule1[foo]: "A" sorry

lemma rule2[foo]: "B" sorry

declare rule1[foo del]

thm foo

ML {* 

  FooRules.get @{context};

*}

text {* 

  \begin{readmore}

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

  \end{readmore}

 *}

end