src/HOL/Topological_Spaces.thy
changeset 57953 69728243a614
parent 57448 159e45728ceb
child 58729 e8ecc79aee43
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:32:26 2014 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Sat Aug 16 14:42:35 2014 +0200
     1.3 @@ -9,17 +9,8 @@
     1.4  imports Main Conditionally_Complete_Lattices
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -
     1.9 -structure Continuous_Intros = Named_Thms
    1.10 -(
    1.11 -  val name = @{binding continuous_intros}
    1.12 -  val description = "Structural introduction rules for continuity"
    1.13 -)
    1.14 -
    1.15 -*}
    1.16 -
    1.17 -setup Continuous_Intros.setup
    1.18 +named_theorems continuous_intros "structural introduction rules for continuity"
    1.19 +
    1.20  
    1.21  subsection {* Topological space *}
    1.22  
    1.23 @@ -1100,20 +1091,12 @@
    1.24  lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
    1.25    by simp
    1.26  
    1.27 -ML {*
    1.28 -
    1.29 -structure Tendsto_Intros = Named_Thms
    1.30 -(
    1.31 -  val name = @{binding tendsto_intros}
    1.32 -  val description = "introduction rules for tendsto"
    1.33 -)
    1.34 -
    1.35 -*}
    1.36 -
    1.37 +named_theorems tendsto_intros "introduction rules for tendsto"
    1.38  setup {*
    1.39 -  Tendsto_Intros.setup #>
    1.40    Global_Theory.add_thms_dynamic (@{binding tendsto_eq_intros},
    1.41 -    map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])) o Tendsto_Intros.get o Context.proof_of);
    1.42 +    fn context =>
    1.43 +      Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
    1.44 +      |> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
    1.45  *}
    1.46  
    1.47  lemma (in topological_space) tendsto_def: