Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lattice/CompleteLattice.thy
changeset 10175 76646fc8b1bf
parent 10157 6d3987f3aad9
child 10176 2e38e3c94990 
--- a/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 14:10:55 2000 +0200
@@ -81,7 +81,7 @@
 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 ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -94,7 +94,7 @@
 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 ex_someI)
+    by (rule someI_ex)
 qed
 
 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
isabelle