# HG changeset patch
# User nipkow
# Date 1515162297 -3600
# Node ID 150d40a2562272cb997dca6690489123ddaf156f
# Parent  d91b9d22305b1df07569f9eff25cb2e4cc17cbcd
tuned op

diff -r d91b9d22305b -r 150d40a25622 src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Thu Jan 04 18:18:57 2018 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Fri Jan 05 15:24:57 2018 +0100
@@ -1171,7 +1171,7 @@
 subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
 
 theorem powerset_is_complete_lattice:
-  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
+  "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = (op \<subseteq>)\<rparr>"
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"