src/HOL/Lifting_Option.thy
changeset 56519 c1048f5bbb45
parent 56518 beb3b6851665
child 56520 3373f5d1e074
     1.1 --- a/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:14 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Option.thy	Thu Apr 10 17:48:15 2014 +0200
     1.3 @@ -63,9 +63,9 @@
     1.4    "bi_unique R \<Longrightarrow> bi_unique (rel_option R)"
     1.5    unfolding bi_unique_def split_option_all by simp
     1.6  
     1.7 -lemma option_invariant_commute [invariant_commute]:
     1.8 -  "rel_option (Lifting.invariant P) = Lifting.invariant (pred_option P)"
     1.9 -  by (auto simp add: fun_eq_iff Lifting.invariant_def split_option_all)
    1.10 +lemma option_relator_eq_onp [relator_eq_onp]:
    1.11 +  "rel_option (eq_onp P) = eq_onp (pred_option P)"
    1.12 +  by (auto simp add: fun_eq_iff eq_onp_def split_option_all)
    1.13  
    1.14  subsection {* Quotient theorem for the Lifting package *}
    1.15