changeset 13897 | f62f9a75f685 |
parent 13896 | 717bd79b976f |
child 13898 | 9410d2eb9563 |
--- a/src/HOLCF/fun3.thy Sat Apr 05 17:03:38 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* 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 - - -