# HG changeset patch
# User huffman
# Date 1273032244 25200
# Node ID 1342e3aeceeb8d59c0f83e5f4929a78adc308153
# Parent  16b0a722083afa7490d798f588fab5ff63b0bd7c# Parent  6302f9ad7047d0633aeb88cee5c178987d3c3769
merged

diff -r 16b0a722083a -r 1342e3aeceeb src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue May 04 21:03:50 2010 -0700
+++ b/src/HOL/Product_Type.thy	Tue May 04 21:04:04 2010 -0700
@@ -416,7 +416,7 @@
   by (simp add: split_def id_def)
 
 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
-  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity Datatype. *}
+  -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   by (rule ext) auto
 
 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
@@ -752,7 +752,7 @@
 
 text {*
   @{term prod_fun} --- action of the product functor upon
-  Datatypes.
+  functions.
 *}
 
 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
diff -r 16b0a722083a -r 1342e3aeceeb src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue May 04 21:03:50 2010 -0700
+++ b/src/HOL/Wellfounded.thy	Tue May 04 21:04:04 2010 -0700
@@ -667,7 +667,7 @@
 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"
@@ -707,7 +707,7 @@
     "[| 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)