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