src/HOL/Datatype.thy

   ("Tools/Datatype/datatype.ML")
   ("Tools/inductive_realizer.ML")
   ("Tools/Datatype/datatype_realizer.ML")
 begin
 
-subsection {* Prelude: lifting over function space *}
-
-enriched_type map_fun: map_fun
-  by (simp_all add: fun_eq_iff)
-
-
 subsection {* The datatype universe *}
 
 definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
 
 typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"

 
 use "Tools/Datatype/datatype_realizer.ML"
 setup Datatype_Realizer.setup
 
 end
+