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.
induct_impliesI;
authorwenzelm
Wed, 31 Oct 2001 01:19:58 +0100
changeset 11988 8340fb172607
parent 11987 bf31b35949ce
child 11989 d4bcba4e080e
induct_impliesI;
src/FOL/FOL.thy file | annotate | diff | comparison | revisions 
--- 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";
isabelle