1.1 --- a/src/Tools/isac/Interpret/derive.sml Sun Apr 18 22:27:43 2021 +0200
1.2 +++ b/src/Tools/isac/Interpret/derive.sml Sun Apr 18 23:37:59 2021 +0200
1.3 @@ -21,13 +21,11 @@
1.4 val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
1.5 bool * derivation
1.6 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
1.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.8 - (* NONE *)
1.9 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.10 +\<^isac_test>\<open>
1.11 val trtas2str : (term * Rule.rule * (term * term list)) list -> string
1.12 val deriv2str : (term * Rule.rule * (term * term list)) list -> string
1.13 val rev_deriv' : 'a * Rule.rule * ('b * 'c) -> 'b * Rule.rule * ('a * 'c)
1.14 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.15 +\<close>
1.16 end
1.17
1.18 (**)