changeset 243 | c22b85994e17 |
242:8fe3e66abf0c | 243:c22b85994e17 |
---|---|
1 (* Title: HOLCF/fun3.thy |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 |
|
6 Class instance of => (fun) for class pcpo |
|
7 |
|
8 *) |
|
9 |
|
10 Fun3 = Fun2 + |
|
11 |
|
12 (* default class is still term *) |
|
13 |
|
14 arities fun :: (term,pcpo)pcpo (* Witness fun2.ML *) |
|
15 |
|
16 rules |
|
17 |
|
18 inst_fun_pcpo "UU::'a=>'b::pcpo = UU_fun" |
|
19 |
|
20 end |
|
21 |
|
22 |
|
23 |