author | haftmann |
Thu, 12 May 2011 11:03:48 +0200 | |
changeset 42715 | fe8ee8099b47 |
parent 42714 | fcba668b0839 |
child 42716 | 45eb6829dde2 |
child 42722 | 626e292d22a7 |
--- a/src/HOL/Finite_Set.thy Mon May 09 16:11:20 2011 +0200 +++ b/src/HOL/Finite_Set.thy Thu May 12 11:03:48 2011 +0200 @@ -539,7 +539,7 @@ text{* On a functional level it looks much nicer: *} -lemma fun_comp_comm: "f x \<circ> f y = f y \<circ> f x" +lemma commute_comp: "f y \<circ> f x = f x \<circ> f y" by (simp add: fun_left_comm fun_eq_iff) end