theory NamedThmsimports Mainbeginchapter {* Recipes *}text_raw {* \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.setuptext {* 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" sorrylemma rule2[foo]: "B" sorrydeclare rule1[foo del]thm fooML {* FooRules.get @{context};*}text {* \begin{readmore} For more information see @{ML_file "Pure/Tools/named_thms.ML"}. \end{readmore} *}end