equal
deleted
inserted
replaced
12 sig |
12 sig |
13 type rule_result |
13 type rule_result |
14 type step |
14 type step |
15 type derivation |
15 type derivation |
16 |
16 |
17 val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ -> |
17 val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function -> |
18 term option -> term -> derivation |
18 term option -> term -> derivation |
19 val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ -> |
19 val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rewrite_Ord.function -> |
20 term option -> term -> rule_result list |
20 term option -> term -> rule_result list |
21 val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term -> |
21 val steps : Rewrite_Ord.T -> Rule_Set.T -> Rule.rule list -> term -> term -> |
22 bool * derivation |
22 bool * derivation |
23 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T |
23 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T |
24 \<^isac_test>\<open> |
24 \<^isac_test>\<open> |
25 val trtas2str : (term * Rule.rule * (term * term list)) list -> string |
25 val trtas2str : (term * Rule.rule * (term * term list)) list -> string |
26 val deriv2str : (term * Rule.rule * (term * term list)) list -> string |
26 val deriv2str : (term * Rule.rule * (term * term list)) list -> string |