theory NamedThms

imports Base

begin

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

text {*

  {\bf 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.\smallskip

  {\bf Solution:} This can be achieved using 

  *}

ML {*

  structure FooRules = NamedThmsFun(

    val name = "foo" 

    val description = "Rules for foo"

  );

*}

setup FooRules.setup

text {*

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

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

  to adding and deleting theorems) and an internal ML interface to retrieve and 

  modify the theorems.

  Furthermore, the facts are made available on the user level under the dynamic 

  fact name @{text foo}. For example:

*}

lemma rule1[foo]: "A" sorry

lemma rule2[foo]: "B" sorry

declare rule1[foo del]

thm foo

text {* 

  In an ML-context the rules marked with @{ML_text "foo"} an be retrieved

  using

*}

ML {* FooRules.get @{context} *}

text {* 

  \begin{readmore}

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

  \end{readmore}

 *}

text {*

  (FIXME: maybe add a comment about the case when the theorems 

  to be added need to satisfy certain properties)

*}

end