+
−
theory NamedThms+
−
imports Main+
−
begin+
−
+
−
+
−
chapter {* 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.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+
−
  +
−
+
−
+
−
+
−