src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
changeset 62311 73bebf642d3b
parent 62127 d8e7738bd2e9
child 62390 842917225d56
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Sun Feb 14 14:33:32 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Sun Feb 14 16:29:30 2016 +0100
     1.3 @@ -58,30 +58,30 @@
     1.4    \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
     1.5      fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
     1.6        [
     1.7 -        (@{thm bounded_linear.has_derivative}, "Deriv.derivative_intros"),
     1.8 -        (@{thm bounded_linear.tendsto}, "Topological_Spaces.tendsto_intros"),
     1.9 -        (@{thm bounded_linear.continuous}, "Topological_Spaces.continuous_intros"),
    1.10 -        (@{thm bounded_linear.continuous_on}, "Topological_Spaces.continuous_intros"),
    1.11 -        (@{thm bounded_linear.uniformly_continuous_on}, "Topological_Spaces.continuous_intros"),
    1.12 -        (@{thm bounded_linear_compose}, "Bounded_Linear_Function.bounded_linear_intros")
    1.13 +        (@{thm bounded_linear.has_derivative}, @{named_theorems derivative_intros}),
    1.14 +        (@{thm bounded_linear.tendsto}, @{named_theorems tendsto_intros}),
    1.15 +        (@{thm bounded_linear.continuous}, @{named_theorems continuous_intros}),
    1.16 +        (@{thm bounded_linear.continuous_on}, @{named_theorems continuous_intros}),
    1.17 +        (@{thm bounded_linear.uniformly_continuous_on}, @{named_theorems continuous_intros}),
    1.18 +        (@{thm bounded_linear_compose}, @{named_theorems bounded_linear_intros})
    1.19        ]))\<close>
    1.20  
    1.21  attribute_setup bounded_bilinear =
    1.22    \<open>Scan.succeed (Thm.declaration_attribute (fn thm =>
    1.23      fold (fn (r, s) => Named_Theorems.add_thm s (thm RS r))
    1.24        [
    1.25 -        (@{thm bounded_bilinear.FDERIV}, "Deriv.derivative_intros"),
    1.26 -        (@{thm bounded_bilinear.tendsto}, "Topological_Spaces.tendsto_intros"),
    1.27 -        (@{thm bounded_bilinear.continuous}, "Topological_Spaces.continuous_intros"),
    1.28 -        (@{thm bounded_bilinear.continuous_on}, "Topological_Spaces.continuous_intros"),
    1.29 +        (@{thm bounded_bilinear.FDERIV}, @{named_theorems derivative_intros}),
    1.30 +        (@{thm bounded_bilinear.tendsto}, @{named_theorems tendsto_intros}),
    1.31 +        (@{thm bounded_bilinear.continuous}, @{named_theorems continuous_intros}),
    1.32 +        (@{thm bounded_bilinear.continuous_on}, @{named_theorems continuous_intros}),
    1.33          (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_left]},
    1.34 -          "Bounded_Linear_Function.bounded_linear_intros"),
    1.35 +          @{named_theorems bounded_linear_intros}),
    1.36          (@{thm bounded_linear_compose[OF bounded_bilinear.bounded_linear_right]},
    1.37 -          "Bounded_Linear_Function.bounded_linear_intros"),
    1.38 +          @{named_theorems bounded_linear_intros}),
    1.39          (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_left]},
    1.40 -          "Topological_Spaces.continuous_intros"),
    1.41 +          @{named_theorems continuous_intros}),
    1.42          (@{thm bounded_linear.uniformly_continuous_on[OF bounded_bilinear.bounded_linear_right]},
    1.43 -          "Topological_Spaces.continuous_intros")
    1.44 +          @{named_theorems continuous_intros})
    1.45        ]))\<close>
    1.46  
    1.47