--- a/src/HOL/Set.ML Thu Jun 29 12:14:04 2000 +0200
+++ b/src/HOL/Set.ML Thu Jun 29 12:14:45 2000 +0200
@@ -210,14 +210,14 @@
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
qed "equalityE";
-AddEs [equalityE];
-
val major::prems = Goal
"[| A = B; [| c:A; c:B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P";
by (rtac (major RS equalityE) 1);
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
qed "equalityCE";
+AddEs [equalityCE];
+
(*Lemma for creating induction formulae -- for "pattern matching" on p
To make the induction hypotheses usable, apply "spec" or "bspec" to
put universal quantifiers over the free variables in p. *)