src/HOL/Wellfounded.thy
changeset 36664 6302f9ad7047
parent 36635 080b755377c0
child 37407 61dd8c145da7
     1.1 --- a/src/HOL/Wellfounded.thy	Tue May 04 13:11:15 2010 -0700
     1.2 +++ b/src/HOL/Wellfounded.thy	Wed May 05 00:59:59 2010 +0200
     1.3 @@ -667,7 +667,7 @@
     1.4  apply blast
     1.5  done
     1.6  
     1.7 -text {* Measure Datatypes into @{typ nat} *}
     1.8 +text {* Measure functions into @{typ nat} *}
     1.9  
    1.10  definition measure :: "('a => nat) => ('a * 'a)set"
    1.11  where "measure == inv_image less_than"
    1.12 @@ -707,7 +707,7 @@
    1.13      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
    1.14  by (unfold trans_def lex_prod_def, blast) 
    1.15  
    1.16 -text {* lexicographic combinations with measure Datatypes *}
    1.17 +text {* lexicographic combinations with measure functions *}
    1.18  
    1.19  definition 
    1.20    mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)