# HG changeset patch
# User nipkow
# Date 930728836 -7200
# Node ID 0364007b4bb3a70b088d9e7206de62a40a8c7451
# Parent  36de02d1a2573af00bc85205f9196574cf049913
New thm trancl_trans_induct

diff -r 36de02d1a257 -r 0364007b4bb3 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Tue Jun 29 11:58:21 1999 +0200
+++ b/src/HOL/Trancl.ML	Wed Jun 30 09:47:16 1999 +0200
@@ -245,6 +245,15 @@
 by (ALLGOALS (blast_tac (claset() addIs (rtrancl_into_trancl1::prems))));
 qed "trancl_induct";
 
+(*Another induction rule for trancl, incorporating transitivity.*)
+val major::prems = goal thy
+ "[| (x,y) : r^+; \
+\    !!x y. (x,y) : r ==> P x y; \
+\    !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
+\ |] ==> P x y";
+by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
+qed "trancl_trans_induct";
+
 (*elimination of r^+ -- NOT an induction rule*)
 val major::prems = Goal
     "[| (a::'a,b) : r^+;  \