src/HOL/HOL.ML
changeset 11451 8abfb4f7bd02
parent 10433 6c5659d461dd
child 11588 d792570a04b1
     1.1 --- a/src/HOL/HOL.ML	Tue Jul 24 11:25:54 2001 +0200
     1.2 +++ b/src/HOL/HOL.ML	Wed Jul 25 13:13:01 2001 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    val refl = refl;
     1.5    val subst = subst;
     1.6    val ext = ext;
     1.7 -  val someI = someI;
     1.8    val impI = impI;
     1.9    val mp = mp;
    1.10    val True_def = True_def;
    1.11 @@ -31,6 +30,6 @@
    1.12  end;
    1.13  
    1.14  AddXIs [equal_intr_rule, disjI1, disjI2, ext];
    1.15 -AddXEs [ex1_implies_ex, someI_ex, sym];
    1.16 +AddXEs [ex1_implies_ex, sym];
    1.17  
    1.18  open HOL;