equal
deleted
inserted
replaced
613 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
613 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
614 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
614 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
615 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
615 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
616 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
616 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
617 in |
617 in |
618 s |> separate "\n" |
618 s |> cat_lines |
619 |> implode |
|
620 |> tracing |
619 |> tracing |
621 end*} |
620 end*} |
622 text_raw{* |
621 text_raw{* |
623 \end{isabelle} |
622 \end{isabelle} |
624 \end{minipage} |
623 \end{minipage} |