equal
deleted
inserted
replaced
10 type single |
10 type single |
11 val single_empty : single |
11 val single_empty : single |
12 type T |
12 type T |
13 val to_string : T -> string |
13 val to_string : T -> string |
14 val result : single -> (term * term list) |
14 val result : single -> (term * term list) |
15 val make_single: Rewrite_Ord.rew_ord' * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> |
15 val make_single: Rewrite_Ord.id * 'a -> Rule_Set.T -> term * Rule.rule * (term * term list) -> |
16 single |
16 single |
17 val insert_pos : Pos.pos -> T -> T |
17 val insert_pos : Pos.pos -> T -> T |
18 end |
18 end |
19 |
19 |
20 (**) |
20 (**) |