equal
deleted
inserted
replaced
1 (* Title: HOLCF/Fun2.thy |
1 (* Title: HOLCF/Fun2.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
|
6 Class Instance =>::(term,po)po |
|
7 *) |
5 *) |
8 |
6 |
9 Fun2 = Fun1 + |
7 Fun2 = Fun1 + |
10 |
8 |
11 (* default class is still term !*) |
9 (* default class is still type!*) |
12 |
10 |
13 instance fun :: (term,po)po (refl_less_fun,antisym_less_fun,trans_less_fun) |
11 instance fun :: (type, po) po (refl_less_fun,antisym_less_fun,trans_less_fun) |
14 |
12 |
15 end |
13 end |
16 |
14 |
17 |
15 |
18 |
16 |