changeset 3661 | 1ea4a45b9412 |
parent 2355 | ee9bdbe2ac8a |
child 4098 | 71e05eb27fb6 |
3660:5c9d3a63e9ff | 3661:1ea4a45b9412 |
---|---|
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 use"adm.ML"; |
|
10 |
|
11 simpset := !simpset addSolver(fn thms => |
|
12 (adm_tac (cut_facts_tac thms THEN' cont_tacRs))); |
|
13 |
|
9 val HOLCF_ss = !simpset; |
14 val HOLCF_ss = !simpset; |