author wenzelm Sat Aug 16 14:42:35 2014 +0200 (2014-08-16) changeset 57953 69728243a614 parent 57952 1a9a6dfc255f child 57954 c52223cd1003
updated to named_theorems;
 src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Deriv.thy	Sat Aug 16 14:32:26 2014 +0200
1.2 +++ b/src/HOL/Deriv.thy	Sat Aug 16 14:42:35 2014 +0200
1.3 @@ -50,24 +50,17 @@
1.4  lemma has_vector_derivative_eq_rhs: "(f has_vector_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_vector_derivative Y) F"
1.5    by simp
1.6
1.7 -ML {*
1.8 -
1.9 -structure Derivative_Intros = Named_Thms
1.10 -(
1.11 -  val name = @{binding derivative_intros}
1.12 -  val description = "structural introduction rules for derivatives"
1.13 -)
1.14 -
1.15 -*}
1.16 -
1.17 +named_theorems derivative_intros "structural introduction rules for derivatives"
1.18  setup {*
1.19    let
1.20 -    val eq_thms = [@{thm has_derivative_eq_rhs}, @{thm DERIV_cong}, @{thm has_vector_derivative_eq_rhs}]
1.21 +    val eq_thms = @{thms has_derivative_eq_rhs DERIV_cong has_vector_derivative_eq_rhs}
1.22      fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
1.23    in
1.24 -    Derivative_Intros.setup #>
1.25      Global_Theory.add_thms_dynamic
1.26 -      (@{binding derivative_eq_intros}, map_filter eq_rule o Derivative_Intros.get o Context.proof_of)
1.27 +      (@{binding derivative_eq_intros},
1.28 +        fn context =>
1.29 +          Named_Theorems.get (Context.proof_of context) @{named_theorems derivative_intros}
1.30 +          |> map_filter eq_rule)
1.31    end;
1.32  *}
1.33
```
```     2.1 --- a/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:32:26 2014 +0200
2.2 +++ b/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:42:35 2014 +0200
2.3 @@ -9,17 +9,8 @@
2.4  imports Main Conditionally_Complete_Lattices
2.5  begin
2.6
2.7 -ML {*
2.8 -
2.9 -structure Continuous_Intros = Named_Thms
2.10 -(
2.11 -  val name = @{binding continuous_intros}
2.12 -  val description = "Structural introduction rules for continuity"
2.13 -)
2.14 -
2.15 -*}
2.16 -
2.17 -setup Continuous_Intros.setup
2.18 +named_theorems continuous_intros "structural introduction rules for continuity"
2.19 +
2.20
2.21  subsection {* Topological space *}
2.22
2.23 @@ -1100,20 +1091,12 @@
2.24  lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
2.25    by simp
2.26
2.27 -ML {*
2.28 -
2.29 -structure Tendsto_Intros = Named_Thms
2.30 -(
2.31 -  val name = @{binding tendsto_intros}
2.32 -  val description = "introduction rules for tendsto"
2.33 -)
2.34 -
2.35 -*}
2.36 -
2.37 +named_theorems tendsto_intros "introduction rules for tendsto"
2.38  setup {*
2.39 -  Tendsto_Intros.setup #>
2.40    Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
2.41 -    map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
2.42 +    fn context =>
2.43 +      Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
2.44 +      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
2.45  *}
2.46
2.47  lemma (in topological_space) tendsto_def:
```