diff -r 79e5b6eec425 -r f5d9bceb4dc0 src/Doc/isac/jrocnik/Test_SUM.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/isac/jrocnik/Test_SUM.thy	Sun Jul 14 14:48:14 2013 +0200
@@ -0,0 +1,28 @@
+
+theory Test_SUM imports Isac begin
+
+section {*trials with implicit function, probably required*}
+ML {*
+@{term "(%n :: nat. n) 2"};
+@{term "(%n. n) 2"};
+@{term "2"};
+*}
+ML {*
+@{term "(%n. n+n)"};
+@{term "(%n. n+n) a"};
+@{term "a+a"};
+*}
+section {*sums*}
+ML {*
+val x = @{term "(SUM i = 0..< k. f i)"};
+term2str x
+*}
+ML {*
+*}
+ML {*
+*}
+ML {*
+*}
+
+end
+