domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
(* Title: HOLCF/cfun2.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class Instance ->::(pcpo,pcpo)po
*)
Cfun2 = Cfun1 +
(* Witness for the above arity axiom is cfun1.ML *)
arities "->" :: (pcpo,pcpo)po
consts
UU_cfun :: "'a->'b"
rules
(* instance of << for type ['a -> 'b] *)
inst_cfun_po "(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
(* definitions *)
(* The least element in type 'a->'b *)
UU_cfun_def "UU_cfun == fabs(% x.UU)"
end
ML
(* ----------------------------------------------------------------------*)
(* unique setup of print translation for fapp *)
(* ----------------------------------------------------------------------*)
val print_translation = [("fapp",fapptr')];