| changeset 12026 | 0b1d80ada4ab |
| parent 12025 | edf306d60e4f |
| child 12027 | 1281e9bf57f6 |
| 12025:edf306d60e4f | 12026:0b1d80ada4ab |
|---|---|
1 (* Title: HOLCF/Lift2.thy |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1996 Technische Universitaet Muenchen |
|
5 |
|
6 Class Instance lift::(term)po |
|
7 *) |
|
8 |
|
9 Lift2 = Lift1 + |
|
10 |
|
11 instance "lift" :: (term)po (refl_less_lift,antisym_less_lift,trans_less_lift) |
|
12 |
|
13 end |
|
14 |
|
15 |