doc-src/Tutorial/Datatype/tunfoldeddata

renamings: real_of_nat, real_of_int -> (overloaded) real
inf_close -> approx
SReal -> Reals
SNat -> Nats

datatype ('a,'b)term = Var 'a | App 'b (('a,'b)term_list)
and ('a,'b)term_list = Nil | Cons (('a,'b)term) (('a,'b)term_list)