equal
deleted
inserted
replaced
16 |
16 |
17 val ID_bnf: BNF_Def.bnf |
17 val ID_bnf: BNF_Def.bnf |
18 val DEADID_bnf: BNF_Def.bnf |
18 val DEADID_bnf: BNF_Def.bnf |
19 |
19 |
20 type comp_cache |
20 type comp_cache |
21 type unfold_set |
21 type unfold_set = |
|
22 {map_unfolds: thm list, |
|
23 set_unfoldss: thm list list, |
|
24 rel_unfolds: thm list} |
22 |
25 |
23 val empty_comp_cache: comp_cache |
26 val empty_comp_cache: comp_cache |
24 val empty_unfolds: unfold_set |
27 val empty_unfolds: unfold_set |
25 |
28 |
26 exception BAD_DEAD of typ * typ |
29 exception BAD_DEAD of typ * typ |