# HG changeset patch
# User wenzelm
# Date 1408192955 -7200
# Node ID 69728243a6140c28941d245fc83bc227a030f62d
# Parent  1a9a6dfc255f829e924285e3b5adfe7eae791e29
updated to named_theorems;

diff -r 1a9a6dfc255f -r 69728243a614 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sat Aug 16 14:32:26 2014 +0200
+++ b/src/HOL/Deriv.thy	Sat Aug 16 14:42:35 2014 +0200
@@ -50,24 +50,17 @@
 lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F"
   by simp
 
-ML {*
-
-structure Derivative_Intros = Named_Thms
-(
-  val name = @{binding derivative_intros}
-  val description = "structural introduction rules for derivatives"
-)
-
-*}
-
+named_theorems derivative_intros "structural introduction rules for derivatives"
 setup {*
   let
-    val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}]
+    val eq_thms = @{thms has_derivative_eq_rhs DERIV_cong has_vector_derivative_eq_rhs}
     fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
   in
-    Derivative_Intros.setup #>
     Global_Theory.add_thms_dynamic
-      (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of)
+      (@{binding derivative_eq_intros},
+        fn context =>
+          Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros}
+          |> map_filter eq_rule)
   end;
 *}
 
diff -r 1a9a6dfc255f -r 69728243a614 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:32:26 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:42:35 2014 +0200
@@ -9,17 +9,8 @@
 imports Main Conditionally_Complete_Lattices
 begin
 
-ML {*
-
-structure Continuous_Intros = Named_Thms
-(
-  val name = @{binding continuous_intros}
-  val description = "Structural introduction rules for continuity"
-)
-
-*}
-
-setup Continuous_Intros.setup
+named_theorems continuous_intros "structural introduction rules for continuity"
+
 
 subsection {* Topological space *}
 
@@ -1100,20 +1091,12 @@
 lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
   by simp
 
-ML {*
-
-structure Tendsto_Intros = Named_Thms
-(
-  val name = @{binding tendsto_intros}
-  val description = "introduction rules for tendsto"
-)
-
-*}
-
+named_theorems tendsto_intros "introduction rules for tendsto"
 setup {*
-  Tendsto_Intros.setup #>
   Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
-    map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
+    fn context =>
+      Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
+      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
 *}
 
 lemma (in topological_space) tendsto_def: