# HG changeset patch
# User wenzelm
# Date 1572794405 -3600
# Node ID bfa1017b4553059bbab54433d1ac937615c44364
# Parent  73f14e0b715183b9c63fb52122fe35d0c19ed4e2
tuned whitespace;

diff -r 73f14e0b7151 -r bfa1017b4553 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Nov 03 16:01:39 2019 +0100
+++ b/src/HOL/Lattices.thy	Sun Nov 03 16:20:05 2019 +0100
@@ -161,7 +161,7 @@
 
 subsection \<open>Concrete lattices\<close>
 
-class semilattice_inf =  order + inf +
+class semilattice_inf = order + inf +
   assumes inf_le1 [simp]: "x \<sqinter> y \<le> x"
   and inf_le2 [simp]: "x \<sqinter> y \<le> y"
   and inf_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"