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