src/HOL/HOL.ML
changeset 9970 dfe4747c8318
parent 9396 a1b31d61f8e1
child 10011 ed5262aee27f
     1.1 --- a/src/HOL/HOL.ML	Fri Sep 15 12:39:57 2000 +0200
     1.2 +++ b/src/HOL/HOL.ML	Fri Sep 15 15:30:50 2000 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4    val refl = refl;
     1.5    val subst = subst;
     1.6    val ext = ext;
     1.7 -  val selectI = selectI;
     1.8 +  val someI = someI;
     1.9    val impI = impI;
    1.10    val mp = mp;
    1.11    val True_def = True_def;