changeset 11588 | d792570a04b1 |
parent 11451 | 8abfb4f7bd02 |
child 11749 | fc8afdc58b26 |
--- a/src/HOL/HOL.ML Thu Sep 27 15:42:30 2001 +0200 +++ b/src/HOL/HOL.ML Thu Sep 27 16:04:11 2001 +0200 @@ -29,7 +29,7 @@ val arbitrary_def = arbitrary_def; end; -AddXIs [equal_intr_rule, disjI1, disjI2, ext]; -AddXEs [ex1_implies_ex, sym]; +AddXIs [equal_intr_rule, ext]; +AddXEs [disjI1, disjI2, ex1_implies_ex, sym]; open HOL;