src/HOL/Topological_Spaces.thy
changeset 55938 f20d1db5aa3c
parent 55775 1557a391a858
child 55942 c2d96043de4b
     1.1 --- a/src/HOL/Topological_Spaces.thy	Thu Mar 06 14:25:55 2014 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Mar 06 14:57:14 2014 +0100
     1.3 @@ -2497,19 +2497,19 @@
     1.4  by(fastforce simp add: filter_rel_eventually[abs_def] eventually_sup dest: fun_relD)
     1.5  
     1.6  lemma Sup_filter_parametric [transfer_rule]:
     1.7 -  "(set_rel (filter_rel A) ===> filter_rel A) Sup Sup"
     1.8 +  "(rel_set (filter_rel A) ===> filter_rel A) Sup Sup"
     1.9  proof(rule fun_relI)
    1.10    fix S T
    1.11 -  assume [transfer_rule]: "set_rel (filter_rel A) S T"
    1.12 +  assume [transfer_rule]: "rel_set (filter_rel A) S T"
    1.13    show "filter_rel A (Sup S) (Sup T)"
    1.14      by(simp add: filter_rel_eventually eventually_Sup) transfer_prover
    1.15  qed
    1.16  
    1.17  lemma principal_parametric [transfer_rule]:
    1.18 -  "(set_rel A ===> filter_rel A) principal principal"
    1.19 +  "(rel_set A ===> filter_rel A) principal principal"
    1.20  proof(rule fun_relI)
    1.21    fix S S'
    1.22 -  assume [transfer_rule]: "set_rel A S S'"
    1.23 +  assume [transfer_rule]: "rel_set A S S'"
    1.24    show "filter_rel A (principal S) (principal S')"
    1.25      by(simp add: filter_rel_eventually eventually_principal) transfer_prover
    1.26  qed
    1.27 @@ -2532,7 +2532,7 @@
    1.28  begin
    1.29  
    1.30  lemma Inf_filter_parametric [transfer_rule]:
    1.31 -  "(set_rel (filter_rel A) ===> filter_rel A) Inf Inf"
    1.32 +  "(rel_set (filter_rel A) ===> filter_rel A) Inf Inf"
    1.33  unfolding Inf_filter_def[abs_def] by transfer_prover
    1.34  
    1.35  lemma inf_filter_parametric [transfer_rule]: