# HG changeset patch
# User paulson
# Date 1032515315 -7200
# Node ID d76a798281f44d1f4eb2f259fd272aa3146a9a1b
# Parent  0d6a0dce3ba3c4928378b38e8a3a8533e4416238
less use of x-symbols

diff -r 0d6a0dce3ba3 -r d76a798281f4 src/HOL/Finite_Set.thy
--- 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 .