src/HOL/Product_Type.thy
changeset 41505 6d19301074cf
parent 41372 551eb49a6e91
child 41792 ff3cb0c418b7
     1.1 --- a/src/HOL/Product_Type.thy	Mon Jan 10 22:03:24 2011 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jan 11 14:12:37 2011 +0100
     1.3 @@ -834,7 +834,7 @@
     1.4    "map_pair f g (a, b) = (f a, g b)"
     1.5    by (simp add: map_pair_def)
     1.6  
     1.7 -type_lifting map_pair: map_pair
     1.8 +enriched_type map_pair: map_pair
     1.9    by (auto simp add: split_paired_all intro: ext)
    1.10  
    1.11  lemma fst_map_pair [simp]: