src/HOL/Lifting_Sum.thy
changeset 56519 c1048f5bbb45
parent 56518 beb3b6851665
child 56520 3373f5d1e074
--- a/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:14 2014 +0200
+++ b/src/HOL/Lifting_Sum.thy	Thu Apr 10 17:48:15 2014 +0200
@@ -50,9 +50,9 @@
   "bi_unique R1 \<Longrightarrow> bi_unique R2 \<Longrightarrow> bi_unique (rel_sum R1 R2)"
   using assms unfolding bi_unique_def split_sum_all by simp
 
-lemma sum_invariant_commute [invariant_commute]: 
-  "rel_sum (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (sum_pred P1 P2)"
-  by (auto simp add: fun_eq_iff Lifting.invariant_def rel_sum_def split: sum.split)
+lemma sum_relator_eq_onp [relator_eq_onp]: 
+  "rel_sum (eq_onp P1) (eq_onp P2) = eq_onp (sum_pred P1 P2)"
+  by (auto simp add: fun_eq_iff eq_onp_def rel_sum_def split: sum.split)
 
 subsection {* Quotient theorem for the Lifting package *}