src/HOL/Datatype.thy
changeset 47488 be6dd389639d
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Datatype.thy	Sun Apr 15 20:41:46 2012 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sun Apr 15 20:51:07 2012 +0200
     1.3 @@ -14,12 +14,6 @@
     1.4    ("Tools/Datatype/datatype_realizer.ML")
     1.5  begin
     1.6  
     1.7 -subsection {* Prelude: lifting over function space *}
     1.8 -
     1.9 -enriched_type map_fun: 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  definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    1.16 @@ -532,3 +526,4 @@
    1.17  setup Datatype_Realizer.setup
    1.18  
    1.19  end
    1.20 +