| changeset 37234 | 95bfc649fe19 |
| parent 33640 | 0d82107dc07a |
| child 37678 | 0040bafffdef |
--- a/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 11:13:09 2010 +0200 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Jun 01 11:13:40 2010 +0200 @@ -264,6 +264,7 @@ lemmas [extraction_expand] = conj_assoc listall_cons_eq extract type_NF + lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b" apply (rule iffI) apply (erule rtranclpR.induct)