src/HOL/Transitive_Closure.thy

--- a/src/HOL/Transitive_Closure.thy	Wed Jan 24 13:15:16 2007 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Jan 24 17:10:50 2007 +0100
@@ -259,6 +259,10 @@
   thus ?thesis by iprover
 qed
 
+lemmas trancl_induct2 =
+  trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
+                 consumes 1, case_names base step]
+
 lemma trancl_trans_induct:
   assumes major: "(x,y) : r^+"
     and cases: "!!x y. (x,y) : r ==> P x y"