doc-src/isac/jrocnik/Test_SUM.thy
branchdecompose-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  *}