src/HOL/Library/FSet.thy
changeset 56519 c1048f5bbb45
parent 56518 beb3b6851665
child 56520 3373f5d1e074
--- a/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:14 2014 +0200
+++ b/src/HOL/Library/FSet.thy	Thu Apr 10 17:48:15 2014 +0200
@@ -853,7 +853,7 @@
 lemma bi_total_rel_fset[transfer_rule]: "bi_total A \<Longrightarrow> bi_total (rel_fset A)"
 by (auto intro: right_total_rel_fset left_total_rel_fset iff: bi_total_iff)
 
-lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
+lemmas fset_relator_eq_onp [relator_eq_onp] = set_relator_eq_onp[Transfer.transferred]
 
 
 subsubsection {* Quotient theorem for the Lifting package *}