| changeset 32463 | 3a0a65ca2261 |
| parent 32462 | c33faa289520 |
| child 32704 | 6f0a56d255f4 |
--- a/src/HOL/Wellfounded.thy Mon Aug 31 20:34:44 2009 +0200 +++ b/src/HOL/Wellfounded.thy Mon Aug 31 20:34:48 2009 +0200 @@ -630,9 +630,6 @@ apply blast done -lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)" - by (auto simp:inv_image_def) - text {* Measure Datatypes into @{typ nat} *} definition measure :: "('a => nat) => ('a * 'a)set"