# HG changeset patch
# User wenzelm
# Date 1004487598 -3600
# Node ID 8340fb1726077612d0f224703eed9847d8abce74
# Parent  bf31b35949ce67ac39ac8513f9b013d3426318a8
induct_impliesI;

diff -r bf31b35949ce -r 8340fb172607 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Oct 30 17:37:25 2001 +0100
+++ b/src/FOL/FOL.thy	Wed Oct 31 01:19:58 2001 +0100
@@ -58,6 +58,9 @@
 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
   by (simp only: atomize_eq induct_equal_def)
 
+lemma induct_impliesI: "(A ==> B) ==> induct_implies(A, B)"
+  by (simp add: induct_implies_def)
+
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq
 lemmas induct_rulify1 = induct_atomize [symmetric, standard]
 lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def
@@ -72,6 +75,7 @@
   (struct
     val dest_concls = FOLogic.dest_concls;
     val cases_default = thm "case_split";
+    val local_impI = thm "induct_impliesI";
     val conjI = thm "conjI";
     val atomize = thms "induct_atomize";
     val rulify1 = thms "induct_rulify1";