AddXEs [disjI1, disjI2];
authorwenzelm
Thu Sep 27 16:04:11 2001 +0200 (2001-09-27)
changeset 11588d792570a04b1
parent 11587 cf448586f26a
child 11589 9a6d4511bb3c
AddXEs [disjI1, disjI2];
src/FOL/FOL.ML
src/HOL/HOL.ML
     1.1 --- a/src/FOL/FOL.ML	Thu Sep 27 15:42:30 2001 +0200
     1.2 +++ b/src/FOL/FOL.ML	Thu Sep 27 16:04:11 2001 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4    val classical = classical;
     1.5  end;
     1.6  
     1.7 -AddXIs [equal_intr_rule, disjI1, disjI2];
     1.8 +AddXIs [equal_intr_rule];
     1.9 +AddXEs [disjI1, disjI2];
    1.10  
    1.11  open FOL;
     2.1 --- a/src/HOL/HOL.ML	Thu Sep 27 15:42:30 2001 +0200
     2.2 +++ b/src/HOL/HOL.ML	Thu Sep 27 16:04:11 2001 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4    val arbitrary_def = arbitrary_def;
     2.5  end;
     2.6  
     2.7 -AddXIs [equal_intr_rule, disjI1, disjI2, ext];
     2.8 -AddXEs [ex1_implies_ex, sym];
     2.9 +AddXIs [equal_intr_rule, ext];
    2.10 +AddXEs [disjI1, disjI2, ex1_implies_ex, sym];
    2.11  
    2.12  open HOL;