added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
(* Title: HOLCF/dnat2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Additional constants for dnat
*)
Dnat2 = Dnat +
consts
iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
rules
iterator_def "iterator = fix[LAM h n f x.\
\ dnat_when[x][LAM m.f[h[m][f][x]]][n]]"
end
(*
iterator[UU][f][x] = UU
iterator[dzero][f][x] = x
n~=UU --> iterator[dsucc[n]][f][x] = f[iterator[n][f][x]]
*)