src/HOL/Tools/inductive.ML
changeset 45648 7654f750fb43
parent 45647 96af0578571c
child 45649 2d995773da1a
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 14:20:31 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 14:26:57 2011 +0100
     1.3 @@ -99,9 +99,6 @@
     1.4  val inductive_rulify = @{thms induct_rulify};
     1.5  val inductive_rulify_fallback = @{thms induct_rulify_fallback};
     1.6  
     1.7 -val notTrueE = TrueI RSN (2, notE);
     1.8 -val notFalseI = Seq.hd (atac 1 notI);
     1.9 -
    1.10  val simp_thms' = map mk_meta_eq
    1.11    @{lemma "(~True) = False" "(~False) = True"
    1.12        "(True --> P) = P" "(False --> P) = True"
    1.13 @@ -372,7 +369,7 @@
    1.14        (mono RS (fp_def RS
    1.15          (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
    1.16  
    1.17 -    val rules = [refl, TrueI, notFalseI, exI, conjI];
    1.18 +    val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI];
    1.19  
    1.20      val intrs = map_index (fn (i, intr) =>
    1.21        Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY
    1.22 @@ -403,7 +400,7 @@
    1.23      val intrs = map dest_intr intr_ts ~~ intr_names;
    1.24  
    1.25      val rules1 = [disjE, exE, FalseE];
    1.26 -    val rules2 = [conjE, FalseE, notTrueE];
    1.27 +    val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}];
    1.28  
    1.29      fun prove_elim c =
    1.30        let