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. *)