# HG changeset patch
# User wenzelm
# Date 971214227 -7200
# Node ID 76f0f0f1c97183869622d6c8b8d5c0c8c843c5a3
# Parent  5413bcce14821d3dc55537d0795085a4b3454fb5
tuned;

diff -r 5413bcce1482 -r 76f0f0f1c971 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Tue Oct 10 23:43:23 2000 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Tue Oct 10 23:43:47 2000 +0200
@@ -80,8 +80,8 @@
 
 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
 proof (unfold Meet_def)
-  from ex_Inf show "is_Inf A (SOME inf. is_Inf A inf)"
-    by (rule someI_ex)
+  from ex_Inf
+  show "is_Inf A (SOME inf. is_Inf A inf)" ..
 qed
 
 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -93,8 +93,8 @@
 
 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
 proof (unfold Join_def)
-  from ex_Sup show "is_Sup A (SOME sup. is_Sup A sup)"
-    by (rule someI_ex)
+  from ex_Sup
+  show "is_Sup A (SOME sup. is_Sup A sup)" ..
 qed
 
 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
diff -r 5413bcce1482 -r 76f0f0f1c971 src/HOL/Lattice/Lattice.thy
--- 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"