src/HOL/Library/Lattice_Algebras.thy
changeset 61546 53bb4172c7f7
parent 60698 29e8bdc41f90
child 65151 a7394aa4d21c
     1.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Mon Nov 02 18:09:14 2015 +0100
     1.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Nov 02 18:30:25 2015 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Author: Steven Obua, TU Muenchen *)
     1.5 +(*  Author:     Steven Obua, TU Muenchen *)
     1.6  
     1.7  section \<open>Various algebraic structures combined with a lattice\<close>
     1.8  
     1.9 @@ -224,7 +224,7 @@
    1.10    proof -
    1.11      from that have a: "inf (a + a) 0 = 0"
    1.12        by (simp add: inf_commute inf_absorb1)
    1.13 -    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
    1.14 +    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l = _")
    1.15        by (simp add: add_sup_inf_distribs inf_aci)
    1.16      then have "?l = 0 + inf a 0"
    1.17        by (simp add: a, simp add: inf_commute)
    1.18 @@ -619,4 +619,3 @@
    1.19  qed
    1.20  
    1.21  end
    1.22 -