# HG changeset patch
# User wenzelm
# Date 1446485425 -3600
# Node ID 53bb4172c7f7611956adbf2dae95c7daa47543fd
# Parent  57000ac6291fecc69a030a19a8882b045312f6dd
tuned whitespace;

diff -r 57000ac6291f -r 53bb4172c7f7 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Mon Nov 02 18:09:14 2015 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Nov 02 18:30:25 2015 +0100
@@ -1,4 +1,4 @@
-(* Author: Steven Obua, TU Muenchen *)
+(*  Author:     Steven Obua, TU Muenchen *)
 
 section \<open>Various algebraic structures combined with a lattice\<close>
 
@@ -224,7 +224,7 @@
   proof -
     from that have a: "inf (a + a) 0 = 0"
       by (simp add: inf_commute inf_absorb1)
-    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
+    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l = _")
       by (simp add: add_sup_inf_distribs inf_aci)
     then have "?l = 0 + inf a 0"
       by (simp add: a, simp add: inf_commute)
@@ -619,4 +619,3 @@
 qed
 
 end
-