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 @{attribute foo} (with the usual @{text add} and @{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 @{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+
−
  +
−
+
−
+
−
+
−