diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/jrocnik/Test_SUM.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/jrocnik/Test_SUM.thy	Tue Sep 17 09:50:52 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
+