--- a/src/HOL/simpdata.ML Fri Nov 28 10:59:14 1997 +0100
+++ b/src/HOL/simpdata.ML Fri Nov 28 11:00:42 1997 +0100
@@ -396,11 +396,14 @@
(fn _ => [rtac ext 1, rtac refl 1]);
+(*For expand_case_tac*)
val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
by (case_tac "P" 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
val expand_case = result();
+(*Used in Auth proofs. Typically P contains Vars that become instantiated
+ during unification.*)
fun expand_case_tac P i =
res_inst_tac [("P",P)] expand_case i THEN
Simp_tac (i+1) THEN