src/HOL/simpdata.ML
changeset 4327 2335f6584a1b
parent 4321 2a2956ccb86c
child 4351 36b28f78ed1b
     1.1 --- a/src/HOL/simpdata.ML	Fri Nov 28 10:59:14 1997 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Fri Nov 28 11:00:42 1997 +0100
     1.3 @@ -396,11 +396,14 @@
     1.4    (fn _ => [rtac ext 1, rtac refl 1]);
     1.5  
     1.6  
     1.7 +(*For expand_case_tac*)
     1.8  val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
     1.9  by (case_tac "P" 1);
    1.10  by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
    1.11  val expand_case = result();
    1.12  
    1.13 +(*Used in Auth proofs.  Typically P contains Vars that become instantiated
    1.14 +  during unification.*)
    1.15  fun expand_case_tac P i =
    1.16      res_inst_tac [("P",P)] expand_case i THEN
    1.17      Simp_tac (i+1) THEN