updated to named_theorems;
authorwenzelm
Sat Aug 16 14:42:35 2014 +0200 (2014-08-16)
changeset 5795369728243a614
parent 57952 1a9a6dfc255f
child 57954 c52223cd1003
updated to named_theorems;
src/HOL/Deriv.thy
src/HOL/Topological_Spaces.thy
     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: