# HG changeset patch
# User wenzelm
# Date 970788077 -7200
# Node ID 00fdd5c330eac2cd7144e27c2c30d0e25ba32007
# Parent  6d3987f3aad93801fe56cbec810349023e5c2cc8
tuned;

diff -r 6d3987f3aad9 -r 00fdd5c330ea src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Fri Oct 06 01:04:56 2000 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Fri Oct 06 01:21:17 2000 +0200
@@ -384,7 +384,7 @@
 
 text {*
   The class of lattices is closed under direct binary products (cf.\
-  also \S\ref{sec:prod-order}).
+  \S\ref{sec:prod-order}).
 *}
 
 lemma is_inf_prod: "is_inf p q (fst p \<sqinter> fst q, snd p \<sqinter> snd q)"
@@ -472,7 +472,7 @@
 
 text {*
   The class of lattices is closed under general products (function
-  spaces) as well (cf.\ also \S\ref{sec:fun-order}).
+  spaces) as well (cf.\ \S\ref{sec:fun-order}).
 *}
 
 lemma is_inf_fun: "is_inf f g (\<lambda>x. f x \<sqinter> g x)"