equal
deleted
inserted
replaced
1 (* Lift1.ML *) |
1 (* Title: HOLCF/Lift1.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller, Robert Sandner |
|
4 Copyright 1996 Technische Universitaet Muenchen |
|
5 |
|
6 Theorems for Lift1.thy |
|
7 *) |
|
8 |
2 |
9 |
3 open Lift1; |
10 open Lift1; |
4 |
11 |
5 (* ------------------------------------------------------------------------ *) |
12 (* ------------------------------------------------------------------------ *) |
6 (* less_lift is a partial order on type 'a -> 'b *) |
13 (* less_lift is a partial order on type 'a -> 'b *) |