# HG changeset patch
# User wenzelm
# Date 1408183836 -7200
# Node ID 6a26aa5fa65e3aa6366910019c1c29babe02ae07
# Parent  cacb00a569e0d27d7cee63862abbfc4c51719605
updated documentation concerning 'named_theorems';

diff -r cacb00a569e0 -r 6a26aa5fa65e NEWS
--- a/NEWS	Sat Aug 16 11:35:33 2014 +0200
+++ b/NEWS	Sat Aug 16 12:10:36 2014 +0200
@@ -9,6 +9,11 @@
 * Commands 'method_setup' and 'attribute_setup' now work within a
 local theory context.
 
+* Command 'named_theorems' declares a dynamic fact within the context,
+together with an attribute to maintain the content incrementally.
+This supersedes functor Named_Thms, but with a subtle change of
+semantics due to external visual order vs. internal reverse order.
+
 
 *** HOL ***
 
diff -r cacb00a569e0 -r 6a26aa5fa65e src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Sat Aug 16 11:35:33 2014 +0200
+++ b/src/Doc/Implementation/Isar.thy	Sat Aug 16 12:10:36 2014 +0200
@@ -436,32 +436,25 @@
 end
 
 text {* \medskip Apart from explicit arguments, common proof methods
-  typically work with a default configuration provided by the context.
-  As a shortcut to rule management we use a cheap solution via the
-  functor @{ML_functor Named_Thms} (see also @{file
-  "~~/src/Pure/Tools/named_thms.ML"}).  *}
+  typically work with a default configuration provided by the context. As a
+  shortcut to rule management we use a cheap solution via the @{command
+  named_theorems} command to declare a dynamic fact in the context. *}
 
-ML {*
-  structure My_Simps =
-    Named_Thms(
-      val name = @{binding my_simp}
-      val description = "my_simp rule"
-    )
-*}
-setup My_Simps.setup
+named_theorems my_simp
 
-text {* This provides ML access to a list of theorems in canonical
-  declaration order via @{ML My_Simps.get}.  The user can add or
-  delete rules via the attribute @{attribute my_simp}.  The actual
-  proof method is now defined as before, but we append the explicit
-  arguments and the rules from the context.  *}
+text {* The proof method is now defined as before, but we append the
+  explicit arguments and the rules from the context. *}
 
 method_setup my_simp' =
   \<open>Attrib.thms >> (fn thms => fn ctxt =>
-    SIMPLE_METHOD' (fn i =>
-      CHANGED (asm_full_simp_tac
-        (put_simpset HOL_basic_ss ctxt
-          addsimps (thms @ My_Simps.get ctxt)) i)))\<close>
+    let
+      val my_simps = Named_Theorems.get ctxt @{named_theorems my_simp}
+    in
+      SIMPLE_METHOD' (fn i =>
+        CHANGED (asm_full_simp_tac
+          (put_simpset HOL_basic_ss ctxt
+            addsimps (thms @ my_simps)) i))
+    end)\<close>
   "rewrite subgoal by given rules and my_simp rules from the context"
 
 text {*
@@ -500,7 +493,7 @@
   theory library, for example.
 
   This is an inherent limitation of the simplistic rule management via
-  functor @{ML_functor Named_Thms}, because it lacks tool-specific
+  @{command named_theorems}, because it lacks tool-specific
   storage and retrieval.  More realistic applications require
   efficient index-structures that organize theorems in a customized
   manner, such as a discrimination net that is indexed by the
diff -r cacb00a569e0 -r 6a26aa5fa65e src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 11:35:33 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Aug 16 12:10:36 2014 +0200
@@ -1305,12 +1305,16 @@
   \begin{matharray}{rcll}
     @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   @{rail \<open>
     (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
       (@{syntax thmdef}? @{syntax thmrefs} + @'and')
       (@'for' (@{syntax vars} + @'and'))?
+    ;
+    @@{command named_theorems} @{syntax target}?
+      @{syntax name} @{syntax text}?
   \<close>}
 
   \begin{description}
@@ -1324,6 +1328,12 @@
   \item @{command "theorems"} is the same as @{command "lemmas"}, but
   marks the result as a different kind of facts.
 
+  \item @{command "named_theorems"}~@{text "name description"} declares a
+  dynamic fact within the context. The same @{text name} is used to define
+  an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
+  \secref{sec:simp-rules}) to maintain the content incrementally, in
+  canonical declaration order of the text structure.
+
   \end{description}
 *}