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,

  *}

ML {*

*}

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 

*}

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

  \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