src/HOL/Transitive_Closure.thy
changeset 22172 e7d6cb237b5e
parent 22080 7bf8868ab3e4
child 22262 96ba62dff413
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 24 13:15:16 2007 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 24 17:10:50 2007 +0100
     1.3 @@ -259,6 +259,10 @@
     1.4    thus ?thesis by iprover
     1.5  qed
     1.6  
     1.7 +lemmas trancl_induct2 =
     1.8 +  trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
     1.9 +                 consumes 1, case_names base step]
    1.10 +
    1.11  lemma trancl_trans_induct:
    1.12    assumes major: "(x,y) : r^+"
    1.13      and cases: "!!x y. (x,y) : r ==> P x y"