src/HOL/HOL.ML
changeset 11588 d792570a04b1
parent 11451 8abfb4f7bd02
child 11749 fc8afdc58b26
     1.1 --- a/src/HOL/HOL.ML	Thu Sep 27 15:42:30 2001 +0200
     1.2 +++ b/src/HOL/HOL.ML	Thu Sep 27 16:04:11 2001 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val arbitrary_def = arbitrary_def;
     1.5  end;
     1.6  
     1.7 -AddXIs [equal_intr_rule, disjI1, disjI2, ext];
     1.8 -AddXEs [ex1_implies_ex, sym];
     1.9 +AddXIs [equal_intr_rule, ext];
    1.10 +AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
    1.11  
    1.12  open HOL;