1.1 --- a/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:09 2010 +0200
     1.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Tue Jun 01 11:13:40 2010 +0200
     1.3 @@ -264,6 +264,7 @@
     1.4  lemmas [extraction_expand] = conj_assoc listall_cons_eq
     1.5  
     1.6  extract type_NF
     1.7 +
     1.8  lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
     1.9    apply (rule iffI)
    1.10    apply (erule rtranclpR.induct)