src/HOL/HOL.ML
changeset 10182 5413bcce1482
parent 10062 3b819da9c71a
child 10273 59570adf2d3c
     1.1 --- a/src/HOL/HOL.ML	Tue Oct 10 12:31:00 2000 +0200
     1.2 +++ b/src/HOL/HOL.ML	Tue Oct 10 23:43:23 2000 +0200
     1.3 @@ -32,6 +32,6 @@
     1.4  end;
     1.5  
     1.6  AddXIs [equal_intr_rule, disjI1, disjI2, ext];
     1.7 -AddXEs [ex1_implies_ex];
     1.8 +AddXEs [ex1_implies_ex, someI_ex];
     1.9  
    1.10  open HOL;