more uniform naming of lemma
authorhaftmann
Thu, 12 May 2011 11:03:48 +0200
changeset 42715 fe8ee8099b47
parent 42714 fcba668b0839
child 42716 45eb6829dde2
child 42722 626e292d22a7
more uniform naming of lemma
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