# HG changeset patch
# User haftmann
# Date 1305191028 -7200
# Node ID fe8ee8099b474849bb6fbdeebcf124831652e1f6
# Parent  fcba668b0839b488144210c9489a236770e7f3dd
more uniform naming of lemma

diff -r fcba668b0839 -r fe8ee8099b47 src/HOL/Finite_Set.thy
--- 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