diff -r a645a0e6d790 -r 48fdff264eb2 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Jun 26 00:14:10 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Jun 26 10:20:33 2015 +0200
@@ -589,7 +589,7 @@
 lemma (in weak_upper_semilattice) finite_sup_insertI:
   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Squnion> (insert x A))"
+  shows "P (\<Squnion>(insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_sup_least)
@@ -828,7 +828,7 @@
 lemma (in weak_lower_semilattice) finite_inf_insertI:
   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Sqinter> (insert x A))"
+  shows "P (\<Sqinter>(insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
     by (simp add: finite_inf_greatest)
@@ -856,7 +856,7 @@
 
 lemma (in weak_lower_semilattice) inf_of_two_greatest:
   "[| x \<in> carrier L; y \<in> carrier L |] ==>
-  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
+  greatest L (\<Sqinter>{x, y}) (Lower L {x, y})"
 proof (unfold inf_def)
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
@@ -904,8 +904,8 @@
 proof -
   (* FIXME: improved simp, see weak_join_assoc above *)
   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
-  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
-  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
+  also from L have "... .= \<Sqinter>{z, x, y}" by (simp add: weak_meet_assoc_lemma)
+  also from L have "... = \<Sqinter>{x, y, z}" by (simp add: insert_commute)
   also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
   finally show ?thesis by (simp add: L)
 qed
@@ -1286,15 +1286,15 @@
 next
   fix B
   assume "B \<subseteq> carrier ?L"
-  then have "least ?L (\<Union> B) (Upper ?L B)"
+  then have "least ?L (\<Union>B) (Upper ?L B)"
     by (fastforce intro!: least_UpperI simp: Upper_def)
   then show "EX s. least ?L s (Upper ?L B)" ..
 next
   fix B
   assume "B \<subseteq> carrier ?L"
-  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
-    txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
-      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
+  then have "greatest ?L (\<Inter>B \<inter> A) (Lower ?L B)"
+    txt {* @{term "\<Inter>B"} is not the infimum of @{term B}:
+      @{term "\<Inter>{} = UNIV"} which is in general bigger than @{term "A"}! *}
     by (fastforce intro!: greatest_LowerI simp: Lower_def)
   then show "EX i. greatest ?L i (Lower ?L B)" ..
 qed