Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned whitespace;
authorwenzelm
Sun, 03 Nov 2019 16:20:05 +0100
changeset 71013 bfa1017b4553
parent 71012 73f14e0b7151
child 71014 58022ee70b35
tuned whitespace;
src/HOL/Lattices.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle