equal
deleted
inserted
replaced
10 Class instance of => (fun) for class pcpo |
10 Class instance of => (fun) for class pcpo |
11 *) |
11 *) |
12 |
12 |
13 header {* Class instances for the type of all functions *} |
13 header {* Class instances for the type of all functions *} |
14 |
14 |
15 theory FunCpo = Pcpo: |
15 theory FunCpo |
|
16 imports Pcpo |
|
17 begin |
16 |
18 |
17 (* to make << defineable: *) |
19 (* to make << defineable: *) |
18 |
20 |
19 instance fun :: (type, sq_ord) sq_ord .. |
21 instance fun :: (type, sq_ord) sq_ord .. |
20 |
22 |