src/HOL/Datatype.thy
changeset 40969 fb2d3ccda5a7
parent 39302 d7728f65b353
child 41372 551eb49a6e91
     1.1 --- a/src/HOL/Datatype.thy	Mon Dec 06 09:19:10 2010 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Dec 06 09:25:05 2010 +0100
     1.3 @@ -13,6 +13,12 @@
     1.4    ("Tools/Datatype/datatype_realizer.ML")
     1.5  begin
     1.6  
     1.7 +subsection {* Prelude: lifting over function space *}
     1.8 +
     1.9 +type_lifting map_fun
    1.10 +  by (simp_all add: fun_eq_iff)
    1.11 +
    1.12 +
    1.13  subsection {* The datatype universe *}
    1.14  
    1.15  typedef (Node)