# HG changeset patch
# User wenzelm
# Date 1455463770 -3600
# Node ID 73bebf642d3ba65665fa0c2549c1428eb0437b26
# Parent  ab836dc7410e3236cf314d16a80f3f3e94748c08
more antiquotations;

diff -r ab836dc7410e -r 73bebf642d3b src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Sun Feb 14 14:33:32 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Sun Feb 14 16:29:30 2016 +0100
@@ -58,30 +58,30 @@
   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
       [
-        (@{thm bounded_linear.has_derivative}, "Deriv.derivative_intros"),
-        (@{thm bounded_linear.tendsto}, "Topological_Spaces.tendsto_intros"),
-        (@{thm bounded_linear.continuous}, "Topological_Spaces.continuous_intros"),
-        (@{thm bounded_linear.continuous_on}, "Topological_Spaces.continuous_intros"),
-        (@{thm bounded_linear.uniformly_continuous_on}, "Topological_Spaces.continuous_intros"),
-        (@{thm bounded_linear_compose}, "Bounded_Linear_Function.bounded_linear_intros")
+        (@{thm bounded_linear.has_derivative}, @{named_theorems derivative_intros}),
+        (@{thm bounded_linear.tendsto}, @{named_theorems tendsto_intros}),
+        (@{thm bounded_linear.continuous}, @{named_theorems continuous_intros}),
+        (@{thm bounded_linear.continuous_on}, @{named_theorems continuous_intros}),
+        (@{thm bounded_linear.uniformly_continuous_on}, @{named_theorems continuous_intros}),
+        (@{thm bounded_linear_compose}, @{named_theorems bounded_linear_intros})
       ]))\<close>
 
 attribute_setup bounded_bilinear =
   \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
     fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
       [
-        (@{thm bounded_bilinear.FDERIV}, "Deriv.derivative_intros"),
-        (@{thm bounded_bilinear.tendsto}, "Topological_Spaces.tendsto_intros"),
-        (@{thm bounded_bilinear.continuous}, "Topological_Spaces.continuous_intros"),
-        (@{thm bounded_bilinear.continuous_on}, "Topological_Spaces.continuous_intros"),
+        (@{thm bounded_bilinear.FDERIV}, @{named_theorems derivative_intros}),
+        (@{thm bounded_bilinear.tendsto}, @{named_theorems tendsto_intros}),
+        (@{thm bounded_bilinear.continuous}, @{named_theorems continuous_intros}),
+        (@{thm bounded_bilinear.continuous_on}, @{named_theorems continuous_intros}),
         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
-          "Bounded_Linear_Function.bounded_linear_intros"),
+          @{named_theorems bounded_linear_intros}),
         (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
-          "Bounded_Linear_Function.bounded_linear_intros"),
+          @{named_theorems bounded_linear_intros}),
         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
-          "Topological_Spaces.continuous_intros"),
+          @{named_theorems continuous_intros}),
         (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
-          "Topological_Spaces.continuous_intros")
+          @{named_theorems continuous_intros})
       ]))\<close>