src/HOL/Finite_Set.thy
changeset 13571 d76a798281f4
parent 13490 44bdc150211b
child 13595 7e6cdcd113a2
--- a/src/HOL/Finite_Set.thy	Thu Sep 19 16:09:16 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Sep 20 11:48:35 2002 +0200
@@ -744,16 +744,16 @@
     thus ?case by simp
   next
     case (insert F x)
-    have "fold (f \<circ> g) e (insert x F \<union> B) = fold (f \<circ> g) e (insert x (F \<union> B))"
+    have "fold (f o g) e (insert x F \<union> B) = fold (f o g) e (insert x (F \<union> B))"
       by simp
-    also have "... = (f \<circ> g) x (fold (f \<circ> g) e (F \<union> B))"
+    also have "... = (f o g) x (fold (f o g) e (F \<union> B))"
       by (rule LC.fold_insert [OF LC.intro])
         (insert b insert, auto simp add: left_commute)
-    also from insert have "fold (f \<circ> g) e (F \<union> B) =
-      fold (f \<circ> g) e F \<cdot> fold (f \<circ> g) e B" by blast
-    also have "(f \<circ> g) x ... = (f \<circ> g) x (fold (f \<circ> g) e F) \<cdot> fold (f \<circ> g) e B"
+    also from insert have "fold (f o g) e (F \<union> B) =
+      fold (f o g) e F \<cdot> fold (f o g) e B" by blast
+    also have "(f o g) x ... = (f o g) x (fold (f o g) e F) \<cdot> fold (f o g) e B"
       by (simp add: AC)
-    also have "(f \<circ> g) x (fold (f \<circ> g) e F) = fold (f \<circ> g) e (insert x F)"
+    also have "(f o g) x (fold (f o g) e F) = fold (f o g) e (insert x F)"
       by (rule LC.fold_insert [OF LC.intro, symmetric]) (insert b insert,
 	auto simp add: left_commute)
     finally show ?case .