changeset 13897 | f62f9a75f685 |
parent 13896 | 717bd79b976f |
child 13898 | 9410d2eb9563 |
13896:717bd79b976f | 13897:f62f9a75f685 |
---|---|
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 |