branch | decompose-isar |
changeset 42276 | 8d642a598ca3 |
parent 42164 | dc2fe21d2183 |
1.1 --- a/doc-src/isac/jrocnik/Test_SUM.thy Mon Sep 19 08:47:07 2011 +0200 1.2 +++ b/doc-src/isac/jrocnik/Test_SUM.thy Tue Sep 20 10:59:55 2011 +0200 1.3 @@ -14,7 +14,8 @@ 1.4 *} 1.5 section {*sums*} 1.6 ML {* 1.7 -@{term "(SUM i = 0..< k. f i)"} 1.8 +val x = @{term "(SUM i = 0..< k. f i)"}; 1.9 +term2str x 1.10 *} 1.11 ML {* 1.12 *}