src/HOL/Set.ML
changeset 9186 7b2f4e6538b4
parent 9161 cee6d5aee7c8
child 9338 fcf7f29a3447
     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. *)