| changeset 21426 | 87ac12bed1ab |
| parent 21425 | c11ab38b78a7 |
| child 21427 | 7c8f4a331f9b |
| 21425:c11ab38b78a7 | 21426:87ac12bed1ab |
|---|---|
1 (* Title: Modal/T.ML |
|
2 ID: $Id$ |
|
3 Author: Martin Coen |
|
4 Copyright 1991 University of Cambridge |
|
5 *) |
|
6 |
|
7 local open Modal0_rls |
|
8 in structure MP_Rule : MODAL_PROVER_RULE = |
|
9 struct |
|
10 val rewrite_rls = rewrite_rls |
|
11 val safe_rls = safe_rls |
|
12 val unsafe_rls = unsafe_rls @ [boxR,diaL] |
|
13 val bound_rls = bound_rls @ [boxL,diaR] |
|
14 val aside_rls = [lstar0,lstar1,lstar2,rstar0,rstar1,rstar2] |
|
15 end |
|
16 end; |
|
17 structure T_Prover = Modal_ProverFun(MP_Rule); |