| changeset 243 | c22b85994e17 |
| 242:8fe3e66abf0c | 243:c22b85994e17 |
|---|---|
1 (* Title: HOLCF/HOLCF.ML |
|
2 ID: $Id$ |
|
3 Author: Franz Regensburger |
|
4 Copyright 1993 Technische Universitaet Muenchen |
|
5 *) |
|
6 |
|
7 open HOLCF; |
|
8 |
|
9 val HOLCF_ss = ccc1_ss |
|
10 addsimps one_when |
|
11 addsimps dist_less_one |
|
12 addsimps dist_eq_one |
|
13 addsimps dist_less_tr |
|
14 addsimps dist_eq_tr |
|
15 addsimps tr_when |
|
16 addsimps andalso_thms |
|
17 addsimps orelse_thms |
|
18 addsimps ifte_thms; |
|
19 |
|
20 |