1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-isac/jrocnik/Test_SUM.thy Tue Sep 17 09:50:52 2013 +0200
1.3 @@ -0,0 +1,28 @@
1.4 +
1.5 +theory Test_SUM imports Isac begin
1.6 +
1.7 +section {*trials with implicit function, probably required*}
1.8 +ML {*
1.9 +@{term "(%n :: nat. n) 2"};
1.10 +@{term "(%n. n) 2"};
1.11 +@{term "2"};
1.12 +*}
1.13 +ML {*
1.14 +@{term "(%n. n+n)"};
1.15 +@{term "(%n. n+n) a"};
1.16 +@{term "a+a"};
1.17 +*}
1.18 +section {*sums*}
1.19 +ML {*
1.20 +val x = @{term "(SUM i = 0..< k. f i)"};
1.21 +term2str x
1.22 +*}
1.23 +ML {*
1.24 +*}
1.25 +ML {*
1.26 +*}
1.27 +ML {*
1.28 +*}
1.29 +
1.30 +end
1.31 +