# 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 (\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?]: "(\a. a \ A \ x \ a) \ x \ \A" @@ -93,8 +93,8 @@ lemma is_Sup_Join [intro?]: "is_Sup A (\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?]: "(\a. a \ A \ a \ x) \ \A \ 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 \ 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 \ x \ z \ y \ z \ x \ y" @@ -85,8 +85,8 @@ lemma is_sup_join [intro?]: "is_sup x y (x \ 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 \ z \ y \ z \ x \ y \ z"