src/HOL/Lifting_Set.thy
changeset 56212 3253aaf73a01
parent 56166 9a241bc276cd
child 56218 1c3f1f2431f9
     1.1 --- a/src/HOL/Lifting_Set.thy	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/src/HOL/Lifting_Set.thy	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -149,14 +149,14 @@
     1.4      rel_set rel_set"
     1.5    unfolding rel_fun_def rel_set_def by fast
     1.6  
     1.7 -lemma SUPR_parametric [transfer_rule]:
     1.8 +lemma SUP_parametric [transfer_rule]:
     1.9    "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
    1.10  proof(rule rel_funI)+
    1.11    fix A B f and g :: "'b \<Rightarrow> 'c"
    1.12    assume AB: "rel_set R A B"
    1.13      and fg: "(R ===> op =) f g"
    1.14    show "SUPR A f = SUPR B g"
    1.15 -    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
    1.16 +    by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
    1.17  qed
    1.18  
    1.19  lemma bind_transfer [transfer_rule]: