author | wenzelm |
Fri, 19 Aug 1994 15:39:52 +0200 | |
changeset 560 | 6702a715281d |
parent 442 | 13ac1fd0a14d |
child 1479 | 21eb5e156d91 |
permissions | -rw-r--r-- |
(* 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