changeset 305 | 2ac9dc1a95b4 |
parent 301 | 2728e8daebc0 |
child 315 | de49d5780f57 |
--- a/ProgTutorial/Package/Ind_Code.thy Wed Aug 05 08:58:28 2009 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Wed Aug 05 09:24:18 2009 +0200 @@ -615,8 +615,7 @@ @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) in - s |> separate "\n" - |> implode + s |> cat_lines |> tracing end*} text_raw{*