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"