New function read_cterms is a combination of read_def_cterm and
read_cterm. It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg. More informative messages can
be printed this way.
(* 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]]
*)