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/HOL.thy
changeset 9970 dfe4747c8318
parent 9950 879e88b1e552
child 10383 a092ae7bb2a6 
--- a/src/HOL/HOL.thy	Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 15 15:30:50 2000 +0200
@@ -159,7 +159,7 @@
     rule, and similar to the ABS rule of HOL.*)
   ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
 
-  selectI:      "P (x::'a) ==> P (@x. P x)"
+  someI:        "P (x::'a) ==> P (@x. P x)"
 
   impI:         "(P ==> Q) ==> P-->Q"
   mp:           "[| P-->Q;  P |] ==> Q"
isabelle