diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/jrocnik/Test_SUM.thy
--- a/src/Doc/isac/jrocnik/Test_SUM.thy	Mon Sep 16 12:27:20 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-
-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
-