src/HOL/Lifting_Option.thy
changeset 56520 3373f5d1e074
parent 56519 c1048f5bbb45
child 56525 b5b6ad5dc2ae
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:15 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -33,10 +33,9 @@
     1.4    "(rel_option A) OO (rel_option B) = rel_option (A OO B)"
     1.5  by (rule ext)+ (auto simp: rel_option_iff OO_def split: option.split)
     1.6  
     1.7 -lemma Domainp_option[relator_domain]:
     1.8 -  assumes "Domainp A = P"
     1.9 -  shows "Domainp (rel_option A) = (pred_option P)"
    1.10 -using assms unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    1.11 +lemma Domainp_option[relator_domain]: 
    1.12 +  "Domainp (rel_option A) = (pred_option (Domainp A))"
    1.13 +unfolding Domainp_iff[abs_def] rel_option_iff[abs_def]
    1.14  by (auto iff: fun_eq_iff split: option.split)
    1.15  
    1.16  lemma left_total_rel_option[transfer_rule]: