# HG changeset patch
# User haftmann
# Date 1370889797 -7200
# Node ID 3bed446c305b6c2e77654092767fc36cb4eef6e0
# Parent  41d7946e25951cbcf06f204514623c5c46764727
tuned whitespace

diff -r 41d7946e2595 -r 3bed446c305b src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon Jun 10 20:30:23 2013 +0200
+++ b/src/HOL/Big_Operators.thy	Mon Jun 10 20:43:17 2013 +0200
@@ -1707,7 +1707,7 @@
   and "semilattice_set.F max = Max"
 proof -
   show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
-  then interpret Min!: semilattice_order_set min less_eq less.
+  then interpret Min!: semilattice_order_set min less_eq less .
   show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   then interpret Max!: semilattice_order_set max greater_eq greater .
   from Min_def show "semilattice_set.F min = Min" by rule
@@ -1754,7 +1754,7 @@
   "semilattice_set.F inf = Inf_fin"
 proof -
   show "semilattice_order_set inf less_eq less" ..
-  then interpret Inf_fin!: semilattice_order_set inf less_eq less.
+  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
 qed