equal
deleted
inserted
replaced
4 Copyright 1996 Technische Universitaet Muenchen |
4 Copyright 1996 Technische Universitaet Muenchen |
5 |
5 |
6 Lifting types of class term to flat pcpo's |
6 Lifting types of class term to flat pcpo's |
7 *) |
7 *) |
8 |
8 |
9 Lift1 = Tr2 + |
9 Lift1 = ccc1 + |
10 |
10 |
11 default term |
11 default term |
12 |
12 |
13 datatype 'a lift = Undef | Def 'a |
13 datatype 'a lift = Undef | Def 'a |
14 |
14 |
15 arities "lift" :: (term)term |
|
16 |
|
17 consts less_lift :: "['a lift, 'a lift] => bool" |
|
18 UU_lift :: "'a lift" |
|
19 |
|
20 defs |
15 defs |
21 |
16 |
22 less_lift_def "less_lift x y == (x=y | x=Undef)" |
17 less_lift_def "less x y == (x=y | x=Undef)" |
23 |
|
24 |
18 |
25 end |
19 end |
26 |
|