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/cfun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of -> for class pcpo
*)
Cfun3 = Cfun2 +
arities "->" :: (pcpo,pcpo)pcpo (* Witness cfun2.ML *)
consts
Istrictify :: "('a->'b)=>'a=>'b"
strictify :: "('a->'b)->'a->'b"
rules
inst_cfun_pcpo "(UU::'a->'b) = UU_cfun"
defs
Istrictify_def "Istrictify f x == if x=UU then UU else f`x"
strictify_def "strictify == (LAM f x.Istrictify f x)"
end