src/HOL/Wellfounded.thy
changeset 31775 2b04504fcb69
parent 30989 1f39aea228b0
child 32205 49db434c157f
     1.1 --- a/src/HOL/Wellfounded.thy	Tue Jun 23 12:09:14 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Tue Jun 23 12:09:30 2009 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  theory Wellfounded
     1.6  imports Finite_Set Transitive_Closure
     1.7 -uses ("Tools/function_package/size.ML")
     1.8 +uses ("Tools/Function/size.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Basic Definitions *}
    1.12 @@ -693,7 +693,7 @@
    1.13  lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
    1.14    by (auto simp:inv_image_def)
    1.15  
    1.16 -text {* Measure functions into @{typ nat} *}
    1.17 +text {* Measure Datatypes into @{typ nat} *}
    1.18  
    1.19  definition measure :: "('a => nat) => ('a * 'a)set"
    1.20  where "measure == inv_image less_than"
    1.21 @@ -733,7 +733,7 @@
    1.22      "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
    1.23  by (unfold trans_def lex_prod_def, blast) 
    1.24  
    1.25 -text {* lexicographic combinations with measure functions *}
    1.26 +text {* lexicographic combinations with measure Datatypes *}
    1.27  
    1.28  definition 
    1.29    mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
    1.30 @@ -948,7 +948,7 @@
    1.31  
    1.32  subsection {* size of a datatype value *}
    1.33  
    1.34 -use "Tools/function_package/size.ML"
    1.35 +use "Tools/Function/size.ML"
    1.36  
    1.37  setup Size.setup
    1.38