# HG changeset patch
# User haftmann
# Date 1312435919 -7200
# Node ID 34abf1f528f39eb0603302bbbe392e0dbf143c9a
# Parent  d01b3f0451118d964e008c1e3632f43cc7a76148
avoid yet unknown fact antiquotation

diff -r d01b3f045111 -r 34abf1f528f3 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Aug 04 07:31:43 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Aug 04 07:31:59 2011 +0200
@@ -405,7 +405,7 @@
   apply (simp_all add: inf_Sup sup_Inf)*)
 
 subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
-  and proof @{fact inf_Sup} and @{fact sup_Inf} from that? *}
+  and proof @{text inf_Sup} and @{text sup_Inf} from that? *}
   fix a b c
   from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
   then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)