| author | wenzelm |
| Thu Aug 27 20:46:36 1998 +0200 (1998-08-27) | |
| changeset 5400 | 645f46a24c72 |
| parent 243 | c22b85994e17 |
| permissions | -rw-r--r-- |
| nipkow@243 | 1 |
(* Title: HOLCF/fun3.thy |
| nipkow@243 | 2 |
ID: $Id$ |
| nipkow@243 | 3 |
Author: Franz Regensburger |
| nipkow@243 | 4 |
Copyright 1993 Technische Universitaet Muenchen |
| nipkow@243 | 5 |
|
| nipkow@243 | 6 |
Class instance of => (fun) for class pcpo |
| nipkow@243 | 7 |
|
| nipkow@243 | 8 |
*) |
| nipkow@243 | 9 |
|
| nipkow@243 | 10 |
Fun3 = Fun2 + |
| nipkow@243 | 11 |
|
| nipkow@243 | 12 |
(* default class is still term *) |
| nipkow@243 | 13 |
|
| nipkow@243 | 14 |
arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *) |
| nipkow@243 | 15 |
|
| nipkow@243 | 16 |
rules |
| nipkow@243 | 17 |
|
| nipkow@243 | 18 |
inst_fun_pcpo "UU::'a=>'b::pcpo = UU_fun" |
| nipkow@243 | 19 |
|
| nipkow@243 | 20 |
end |
| nipkow@243 | 21 |
|
| nipkow@243 | 22 |
|
| nipkow@243 | 23 |