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/BCV/Semilat.ML
changeset 9969 4753185f1dd2
parent 9791 a39e5d43de55
child 10172 3daeda3d3cd0 
--- a/src/HOL/BCV/Semilat.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/BCV/Semilat.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -162,7 +162,7 @@
 
 Goalw [some_lub_def,is_lub_def]
  "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u";
-br selectI2 1;
+br someI2 1;
  ba 1;
 by(blast_tac (claset() addIs [antisymD]
                        addSDs [acyclic_impl_antisym_rtrancl]) 1);
isabelle