now uses equalityCE, which usually is more efficent than equalityE
authorpaulson
Thu Jun 29 12:14:45 2000 +0200 (2000-06-29)
changeset 91867b2f4e6538b4
parent 9185 30d46270a427
child 9187 68ecc04785f1
now uses equalityCE, which usually is more efficent than equalityE
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Thu Jun 29 12:14:04 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Thu Jun 29 12:14:45 2000 +0200
     1.3 @@ -210,14 +210,14 @@
     1.4  by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
     1.5  qed "equalityE";
     1.6  
     1.7 -AddEs [equalityE];
     1.8 -
     1.9  val major::prems = Goal
    1.10      "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
    1.11  by (rtac (major RS equalityE) 1);
    1.12  by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
    1.13  qed "equalityCE";
    1.14  
    1.15 +AddEs [equalityCE];
    1.16 +
    1.17  (*Lemma for creating induction formulae -- for "pattern matching" on p
    1.18    To make the induction hypotheses usable, apply "spec" or "bspec" to
    1.19    put universal quantifiers over the free variables in p. *)