Fixed bug that caused proof of induction theorem to fail if
authorberghofe
Tue May 15 18:20:07 2007 +0200 (2007-05-15)
changeset 229801226d861eefb
parent 22979 d95580341be5
child 22981 cf071f3fc4ae
Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue May 15 08:10:31 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue May 15 18:20:07 2007 +0200
     1.3 @@ -550,7 +550,8 @@
     1.4           REPEAT (FIRSTGOAL
     1.5             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
     1.6           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
     1.7 -           (inductive_conj_def :: rec_preds_defs) prem, conjI, refl] 1)) prems)]);
     1.8 +             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
     1.9 +           conjI, refl] 1)) prems)]);
    1.10  
    1.11      val lemma = SkipProof.prove ctxt'' [] []
    1.12        (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY