--- 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^+; \