src/Tools/isac/Interpret/solve-step.sml
changeset 60509 2e0b7ca391dc
parent 60506 145e45cd7a0f
child 60527 ff2da703f546
equal deleted inserted replaced
60508:ce09935439b3 60509:2e0b7ca391dc
    15     Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
    15     Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
    16   val add_hard:
    16   val add_hard:
    17     theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
    17     theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Test_Out.T
    18 
    18 
    19   val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
    19   val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
    20     string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
    20     string * ThyC.id * Rewrite_Ord.id * Rule_Def.rule_set * bool
    21   val get_eval: string -> Pos.pos ->Ctree.ctree ->
    21   val get_eval: string -> Pos.pos ->Ctree.ctree ->
    22     string * ThyC.id * (string * Rule_Def.eval_fn)
    22     string * ThyC.id * (string * Rule_Def.eval_fn)
    23 \<^isac_test>\<open>
    23 \<^isac_test>\<open>
    24   val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
    24   val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
    25 \<close>
    25 \<close>