Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed bug that caused proof of induction theorem to fail if
authorberghofe
Tue, 15 May 2007 18:20:07 +0200
changeset 22980 1226d861eefb
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 file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Tue May 15 08:10:31 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue May 15 18:20:07 2007 +0200
@@ -550,7 +550,8 @@
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
-           (inductive_conj_def :: rec_preds_defs) prem, conjI, refl] 1)) prems)]);
+             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
+           conjI, refl] 1)) prems)]);
 
     val lemma = SkipProof.prove ctxt'' [] []
       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
isabelle