--- a/src/HOL/Lattice/Bounds.thy Thu Jun 14 22:59:42 2007 +0200
+++ b/src/HOL/Lattice/Bounds.thy Thu Jun 14 23:04:36 2007 +0200
@@ -193,8 +193,8 @@
show ?thesis
proof
show "x \<sqsubseteq> x" ..
- show "x \<sqsubseteq> y" by assumption
- fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by assumption
+ show "x \<sqsubseteq> y" by fact
+ fix z assume "z \<sqsubseteq> x" and "z \<sqsubseteq> y" show "z \<sqsubseteq> x" by fact
qed
qed
@@ -203,10 +203,10 @@
assume "x \<sqsubseteq> y"
show ?thesis
proof
- show "x \<sqsubseteq> y" by assumption
+ show "x \<sqsubseteq> y" by fact
show "y \<sqsubseteq> y" ..
fix z assume "x \<sqsubseteq> z" and "y \<sqsubseteq> z"
- show "y \<sqsubseteq> z" by assumption
+ show "y \<sqsubseteq> z" by fact
qed
qed