src/HOL/Lifting_Set.thy
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56524 f4ba736040fa
     1.1 --- a/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:15 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -45,9 +45,8 @@
     1.4    done
     1.5  
     1.6  lemma Domainp_set[relator_domain]:
     1.7 -  assumes "Domainp T = R"
     1.8 -  shows "Domainp (rel_set T) = (\<lambda>A. Ball A R)"
     1.9 -using assms unfolding rel_set_def Domainp_iff[abs_def]
    1.10 +  "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"
    1.11 +unfolding rel_set_def Domainp_iff[abs_def]
    1.12  apply (intro ext)
    1.13  apply (rule iffI) 
    1.14  apply blast