equal
deleted
inserted
replaced
5 10 20 30 40 50 60 70 80 |
5 10 20 30 40 50 60 70 80 |
6 *) |
6 *) |
7 |
7 |
8 structure Applicable = (* intermediately to avoid too many "Ctree." *) |
8 structure Applicable = (* intermediately to avoid too many "Ctree." *) |
9 struct |
9 struct |
10 (*open Ctree*) |
10 open Ctree |
11 |
11 |
12 val e_cterm' = empty_cterm'; |
12 val e_cterm' = empty_cterm'; |
13 |
13 |
14 |
14 |
15 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = |
15 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = |