src/HOL/Library/Product_Order.thy
changeset 67091 1393c2340eec
parent 63972 c98d1dd7eba1
child 67829 2a6ef5ba4822
--- a/src/HOL/Library/Product_Order.thy	Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Library/Product_Order.thy	Sun Nov 26 21:08:32 2017 +0100
@@ -220,11 +220,11 @@
 of two complete lattices:\<close>
 
 lemma INF_prod_alt_def:
-  "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
+  "INFIMUM A f = (INFIMUM A (fst \<circ> f), INFIMUM A (snd \<circ> f))"
   unfolding Inf_prod_def by simp
 
 lemma SUP_prod_alt_def:
-  "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
+  "SUPREMUM A f = (SUPREMUM A (fst \<circ> f), SUPREMUM A (snd \<circ> f))"
   unfolding Sup_prod_def by simp