equal
deleted
inserted
replaced
1 (* Title: HOLCF/lift2.thy |
1 (* Title: HOLCF/lift2.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 u::(pcpo)po |
6 Class Instance u::(pcpo)po |
7 |
7 |
8 *) |
8 *) |
15 |
15 |
16 rules |
16 rules |
17 |
17 |
18 (* instance of << for type ('a)u *) |
18 (* instance of << for type ('a)u *) |
19 |
19 |
20 inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" |
20 inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" |
21 |
21 |
22 end |
22 end |
23 |
23 |
24 |
24 |
25 |
25 |