AddXIs [equal_intr_rule];
authorwenzelm
Fri Sep 22 17:24:36 2000 +0200 (2000-09-22)
changeset 100623b819da9c71a
parent 10061 fe82134773dc
child 10063 947ee8608b90
AddXIs [equal_intr_rule];
src/FOL/FOL.ML
src/HOL/HOL.ML
     1.1 --- a/src/FOL/FOL.ML	Fri Sep 22 16:28:53 2000 +0200
     1.2 +++ b/src/FOL/FOL.ML	Fri Sep 22 17:24:36 2000 +0200
     1.3 @@ -5,6 +5,6 @@
     1.4    val classical = classical;
     1.5  end;
     1.6  
     1.7 -AddXIs [disjI1, disjI2];
     1.8 +AddXIs [equal_intr_rule, disjI1, disjI2];
     1.9  
    1.10  open FOL;
     2.1 --- a/src/HOL/HOL.ML	Fri Sep 22 16:28:53 2000 +0200
     2.2 +++ b/src/HOL/HOL.ML	Fri Sep 22 17:24:36 2000 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4    val arbitrary_def = arbitrary_def;
     2.5  end;
     2.6  
     2.7 -AddXIs [disjI1, disjI2, ext];
     2.8 +AddXIs [equal_intr_rule, disjI1, disjI2, ext];
     2.9 +AddXEs [ex1_implies_ex];
    2.10  
    2.11  open HOL;