equal
deleted
inserted
replaced
1 open Lift; |
1 (* Title: HOLCF/Lift.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller |
|
4 Copyright 1997 Technische Universitaet Muenchen |
|
5 |
|
6 Theorems for Lift.thy |
|
7 *) |
|
8 |
2 |
9 |
3 (* ---------------------------------------------------------- *) |
10 (* ---------------------------------------------------------- *) |
4 section"Continuity Proofs for flift1, flift2, if"; |
11 section"Continuity Proofs for flift1, flift2, if"; |
|
12 (* ---------------------------------------------------------- *) |
5 (* need the instance into flat *) |
13 (* need the instance into flat *) |
6 (* ---------------------------------------------------------- *) |
|
7 |
14 |
8 |
15 |
9 (* flift1 is continuous in its argument itself*) |
16 (* flift1 is continuous in its argument itself*) |
10 goal thy "cont (lift_case UU f)"; |
17 goal thy "cont (lift_case UU f)"; |
11 by (rtac flatdom_strict2cont 1); |
18 by (rtac flatdom_strict2cont 1); |