merged
authorhaftmann
Sat Sep 19 07:35:27 2009 +0200 (2009-09-19)
changeset 32611210fa627d767
parent 32609 2f3e7a92b522
parent 32610 c477b0a62ce9
child 32613 0bc4f7e3e2d3
child 32684 139257823133
merged
     1.1 --- a/src/HOL/Tools/inductive.ML	Fri Sep 18 23:08:53 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sat Sep 19 07:35:27 2009 +0200
     1.3 @@ -103,6 +103,7 @@
     1.4        "(P & True) = P" "(True & P) = P"
     1.5      by (fact simp_thms)+};
     1.6  
     1.7 +val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
     1.8  
     1.9  
    1.10  (** context data **)
    1.11 @@ -559,7 +560,7 @@
    1.12          [rewrite_goals_tac [inductive_conj_def],
    1.13           DETERM (rtac raw_fp_induct 1),
    1.14           REPEAT (resolve_tac [le_funI, le_boolI] 1),
    1.15 -         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'),
    1.16 +         rewrite_goals_tac simp_thms'',
    1.17           (*This disjE separates out the introduction rules*)
    1.18           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
    1.19           (*Now break down the individual cases.  No disjE here in case
    1.20 @@ -568,7 +569,7 @@
    1.21           REPEAT (FIRSTGOAL
    1.22             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
    1.23           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
    1.24 -             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
    1.25 +             (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
    1.26             conjI, refl] 1)) prems)]);
    1.27  
    1.28      val lemma = SkipProof.prove ctxt'' [] []