src/HOL/Fun.thy
changeset 47488 be6dd389639d
parent 46950 d0181abdbdac
child 47579 28f6f4ad69bf
     1.1 --- a/src/HOL/Fun.thy	Sun Apr 15 20:41:46 2012 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sun Apr 15 20:51:07 2012 +0200
     1.3 @@ -803,4 +803,11 @@
     1.4  
     1.5  use "Tools/enriched_type.ML"
     1.6  
     1.7 +enriched_type map_fun: map_fun
     1.8 +  by (simp_all add: fun_eq_iff)
     1.9 +
    1.10 +enriched_type vimage
    1.11 +  by (simp_all add: fun_eq_iff vimage_compose)
    1.12 +
    1.13  end
    1.14 +