equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 open Denotation; |
7 open Denotation; |
8 |
8 |
9 (**** Rewrite Rules for A,B,C ****) |
9 (**** Rewrite Rules for A,B,C ****) |
10 |
|
11 val A_simps = |
|
12 [A_nat,A_loc,A_op1,A_op2]; |
|
13 |
10 |
14 val B_simps = map (fn t => t RS eq_reflection) |
11 val B_simps = map (fn t => t RS eq_reflection) |
15 [B_true,B_false,B_op,B_not,B_and,B_or] |
12 [B_true,B_false,B_op,B_not,B_and,B_or] |
16 |
13 |
17 val C_simps = map (fn t => t RS eq_reflection) |
14 val C_simps = map (fn t => t RS eq_reflection) |