equal
deleted
inserted
replaced
1 (* Title: HOLCF/Porder0.ML |
1 (* Title: HOLCF/Porder0.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Oscar Slotosch |
3 Author: Oscar Slotosch |
4 Copyright 1997 Technische Universitaet Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 derive the characteristic axioms for the characteristic constants |
6 derive the characteristic axioms for the characteristic constants |
7 *) |
7 *) |
8 |
8 |
9 AddIffs [refl_less]; |
9 AddIffs [refl_less]; |
10 |
10 |
11 (* ------------------------------------------------------------------------ *) |
11 (* ------------------------------------------------------------------------ *) |