| author | wenzelm |
| Sat Nov 03 01:41:26 2001 +0100 (2001-11-03) | |
| changeset 12030 | 46d57d0290a2 |
| parent 2838 | 2e908f29bc3d |
| child 12338 | de0f4a63baa5 |
| permissions | -rw-r--r-- |
1 (* Title: HOLCF/Fun3.thy
2 ID: $Id$
3 Author: Franz Regensburger
4 License: GPL (GNU GENERAL PUBLIC LICENSE)
6 Class instance of => (fun) for class pcpo
7 *)
9 Fun3 = Fun2 +
11 (* default class is still term *)
13 instance fun :: (term,cpo)cpo (cpo_fun)
14 instance fun :: (term,pcpo)pcpo (least_fun)
16 end