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