| changeset 2355 | ee9bdbe2ac8a |
| parent 1461 | 6bcb44e4d6e5 |
| child 3661 | 1ea4a45b9412 |
| 2354:b4a1e3306aa0 | 2355:ee9bdbe2ac8a |
|---|---|
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 open HOLCF; |
7 open HOLCF; |
8 |
8 |
9 Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr |
|
10 @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms); |
|
11 |
|
12 val HOLCF_ss = !simpset; |
9 val HOLCF_ss = !simpset; |