src/HOL/Wellfounded.thy

 apply (erule allE)
 apply (erule (1) notE impE)
 apply blast
 done
 
-text {* Measure Datatypes into @{typ nat} *}
+text {* Measure functions into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"
 where "measure == inv_image less_than"
 
 lemma in_measure[simp]: "((x,y) : measure f) = (f x < f y)"

 
 lemma trans_lex_prod [intro!]: 
     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
 by (unfold trans_def lex_prod_def, blast) 
 
-text {* lexicographic combinations with measure Datatypes *}
+text {* lexicographic combinations with measure functions *}
 
 definition 
   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
 where
   "f <*mlex*> R = inv_image (less_than <*lex*> R) (%x. (f x, x))"