Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
authorpaulson
Fri Jun 16 13:15:40 2000 +0200 (2000-06-16)
changeset 9075e8521ed7f35b
parent 9074 2313ddc415a1
child 9076 108ec332625d
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Fri Jun 16 13:15:04 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Jun 16 13:15:40 2000 +0200
     1.3 @@ -212,10 +212,7 @@
     1.4  by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
     1.5  qed "equalityE";
     1.6  
     1.7 -(*This could be tried.  Most things build fine with it.  However, some proofs
     1.8 -  become very slow or even fail.
     1.9 -  AddEs [equalityE];
    1.10 -*)
    1.11 +AddEs [equalityE];
    1.12  
    1.13  val major::prems = Goal
    1.14      "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
    1.15 @@ -295,9 +292,6 @@
    1.16  by (Blast_tac 1) ;
    1.17  qed "equals0D";
    1.18  
    1.19 -(* [| A = {};  a : A |] ==> R *)
    1.20 -AddDs [equals0D, sym RS equals0D];
    1.21 -
    1.22  Goalw [Ball_def] "Ball {} P = True";
    1.23  by (Simp_tac 1);
    1.24  qed "ball_empty";