src/HOL/Lifting_Set.thy
changeset 54257 5c7a3b6b05a9
parent 53952 b2781a3ce958
child 55564 e81ee43ab290
     1.1 --- a/src/HOL/Lifting_Set.thy	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/Lifting_Set.thy	Tue Nov 05 09:44:57 2013 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4    unfolding fun_rel_def set_rel_def by fast
     1.5  
     1.6  lemma SUPR_parametric [transfer_rule]:
     1.7 -  "(set_rel R ===> (R ===> op =) ===> op =) SUPR SUPR"
     1.8 +  "(set_rel R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
     1.9  proof(rule fun_relI)+
    1.10    fix A B f and g :: "'b \<Rightarrow> 'c"
    1.11    assume AB: "set_rel R A B"