equal
deleted
inserted
replaced
264 ML{*fun string_of_thms ctxt thms = |
264 ML{*fun string_of_thms ctxt thms = |
265 commas (map (string_of_thm ctxt) thms) |
265 commas (map (string_of_thm ctxt) thms) |
266 |
266 |
267 fun string_of_thms_no_vars ctxt thms = |
267 fun string_of_thms_no_vars ctxt thms = |
268 commas (map (string_of_thm_no_vars ctxt) thms) *} |
268 commas (map (string_of_thm_no_vars ctxt) thms) *} |
|
269 |
|
270 text {* |
|
271 When printing out several `parcels' of information that belong |
|
272 together you should try to keep this information together. For |
|
273 this you can use the function @{ML [index] cat_lines}, which |
|
274 concatenates a list of strings and inserts newlines. |
|
275 |
|
276 @{ML_response [display, gray] |
|
277 "cat_lines [\"foo\", \"bar\"]" |
|
278 "\"foo\\nbar\""} |
|
279 *} |
|
280 |
269 |
281 |
270 section {* Combinators\label{sec:combinators} *} |
282 section {* Combinators\label{sec:combinators} *} |
271 |
283 |
272 text {* |
284 text {* |
273 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
285 For beginners perhaps the most puzzling parts in the existing code of Isabelle are |
744 "let |
756 "let |
745 val v1 = Var ((\"x\", 3), @{typ bool}) |
757 val v1 = Var ((\"x\", 3), @{typ bool}) |
746 val v2 = Var ((\"x1\", 3), @{typ bool}) |
758 val v2 = Var ((\"x1\", 3), @{typ bool}) |
747 val v3 = Free (\"x\", @{typ bool}) |
759 val v3 = Free (\"x\", @{typ bool}) |
748 in |
760 in |
749 tracing (Syntax.string_of_term @{context} v1); |
761 map (Syntax.string_of_term @{context}) [v1, v2, v3] |
750 tracing (Syntax.string_of_term @{context} v2); |
762 |> cat_lines |
751 tracing (Syntax.string_of_term @{context} v3) |
763 |> tracing |
752 end" |
764 end" |
753 "?x3 |
765 "?x3 |
754 ?x1.3 |
766 ?x1.3 |
755 x"} |
767 x"} |
756 |
768 |