--- a/src/HOL/Lattice/Lattice.thy Tue Oct 10 23:43:23 2000 +0200
+++ b/src/HOL/Lattice/Lattice.thy Tue Oct 10 23:43:47 2000 +0200
@@ -69,8 +69,8 @@
lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
proof (unfold meet_def)
- from ex_inf show "is_inf x y (SOME inf. is_inf x y inf)"
- by (rule someI_ex)
+ from ex_inf
+ show "is_inf x y (SOME inf. is_inf x y inf)" ..
qed
lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -85,8 +85,8 @@
lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
proof (unfold join_def)
- from ex_sup show "is_sup x y (SOME sup. is_sup x y sup)"
- by (rule someI_ex)
+ from ex_sup
+ show "is_sup x y (SOME sup. is_sup x y sup)" ..
qed
lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"