hierarchically inclusive named theorem collections

--- a/src/HOL/Eisbach/method_closure.ML	Tue Apr 16 19:50:21 2019 +0000
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Apr 16 19:50:30 2019 +0000
@@ -182,7 +182,7 @@
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
       |> fold setup_local_method methods
-      |> fold_map (fn b => Named_Theorems.declare b "") uses;
+      |> fold_map (fn b => Named_Theorems.declare b [] "") uses;
 
     val (term_args, lthy2) = lthy1
       |> add_fixes vars |-> fold_map Proof_Context.inferred_param |>> map Free;

--- a/src/Pure/Pure.thy	Tue Apr 16 19:50:21 2019 +0000
+++ b/src/Pure/Pure.thy	Tue Apr 16 19:50:30 2019 +0000
@@ -545,8 +545,9 @@
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>named_theorems\<close>
     "declare named collection of theorems"
-    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
-      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
+    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text ""
+      -- Scan.optional (\<^keyword>\<open>includes\<close> |-- Scan.repeat1 Parse.text) []) >>
+      fold (fn ((b, descr), extends) => snd o Named_Theorems.declare b extends descr));
 
 in end\<close>
 

--- a/src/Pure/Tools/named_theorems.ML	Tue Apr 16 19:50:21 2019 +0000
+++ b/src/Pure/Tools/named_theorems.ML	Tue Apr 16 19:50:30 2019 +0000
@@ -14,7 +14,8 @@
   val add: string -> attribute
   val del: string -> attribute
   val check: Proof.context -> string * Position.T -> string
-  val declare: binding -> string -> local_theory -> string * local_theory
+  val declare: binding -> string list -> string ->
+    local_theory -> string * local_theory
 end;
 
 structure Named_Theorems: NAMED_THEOREMS =
@@ -87,15 +88,17 @@
 
 (* declaration *)
 
-fun declare binding descr lthy =
+fun declare binding raw_extends descr lthy =
   let
     val name = Local_Theory.full_name lthy binding;
+    val extends = map (fn s => check lthy (s, Position.none)) raw_extends;
     val description =
       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     val lthy' = lthy
       |> Local_Theory.background_theory (Context.theory_map (new_entry name))
       |> Local_Theory.map_contexts (K (Context.proof_map (new_entry name)))
-      |> Local_Theory.add_thms_dynamic (binding, fn context => content context name)
+      |> Local_Theory.add_thms_dynamic (binding,
+           fn context => maps (content context) (extends @ [name]))
       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
   in (name, lthy') end;
 

--- a/src/Tools/atomize_elim.ML	Tue Apr 16 19:50:21 2019 +0000
+++ b/src/Tools/atomize_elim.ML	Tue Apr 16 19:50:30 2019 +0000
@@ -19,7 +19,7 @@
 val named_theorems =
   Context.>>> (Context.map_theory_result
    (Named_Target.theory_init #>
-    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> "atomize_elim rewrite rule" ##>
+    Named_Theorems.declare \<^binding>\<open>atomize_elim\<close> [] "atomize_elim rewrite rule" ##>
     Local_Theory.exit_global));