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/fun3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of => (fun) for class pcpo
*)
Fun3 = Fun2 +
(* default class is still term *)
arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *)
rules
inst_fun_pcpo "UU::'a=>'b::pcpo = UU_fun"
end