tuned whitespace
authorhaftmann
Mon Jun 10 20:43:17 2013 +0200 (2013-06-10)
changeset 523643bed446c305b
parent 52363 41d7946e2595
child 52365 95186e6e4bf4
tuned whitespace
src/HOL/Big_Operators.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Mon Jun 10 20:30:23 2013 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Mon Jun 10 20:43:17 2013 +0200
     1.3 @@ -1707,7 +1707,7 @@
     1.4    and "semilattice_set.F max = Max"
     1.5  proof -
     1.6    show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
     1.7 -  then interpret Min!: semilattice_order_set min less_eq less.
     1.8 +  then interpret Min!: semilattice_order_set min less_eq less .
     1.9    show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
    1.10    then interpret Max!: semilattice_order_set max greater_eq greater .
    1.11    from Min_def show "semilattice_set.F min = Min" by rule
    1.12 @@ -1754,7 +1754,7 @@
    1.13    "semilattice_set.F inf = Inf_fin"
    1.14  proof -
    1.15    show "semilattice_order_set inf less_eq less" ..
    1.16 -  then interpret Inf_fin!: semilattice_order_set inf less_eq less.
    1.17 +  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
    1.18    from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
    1.19  qed
    1.20