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
```