theory NamedThms
imports Main
uses "antiquote_setup.ML"
     "antiquote_setup_plus.ML"
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}
 *}

text {*
  (FIXME: maybe add a comment about the case when the theorems 
  to be added need to satisfy certain properties)

*}


end