equal
deleted
inserted
replaced
1 (* Title: Modal/S4 |
1 (* Title: Modal/S4.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin Coen |
3 Author: Martin Coen |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 *) |
5 *) |
6 |
6 |
7 local open Modal0_rls S4 |
7 local open Modal0_rls |
8 in structure MP_Rule : MODAL_PROVER_RULE = |
8 in structure MP_Rule : MODAL_PROVER_RULE = |
9 struct |
9 struct |
10 val rewrite_rls = rewrite_rls |
10 val rewrite_rls = rewrite_rls |
11 val safe_rls = safe_rls |
11 val safe_rls = safe_rls |
12 val unsafe_rls = unsafe_rls @ [boxR,diaL] |
12 val unsafe_rls = unsafe_rls @ [boxR,diaL] |