1.1 --- a/doc-src/isac/jrocnik/Test_SUM.thy	Fri Jul 22 10:26:39 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_SUM.thy	Fri Jul 22 12:10:13 2011 +0200
     1.3 @@ -1,13 +1,7 @@
     1.4  
     1.5  theory Test_SUM imports Isac begin
     1.6  
     1.7 -ML{* writeln "**** run the test ***************************************" *}
     1.8 -
     1.9 -use"../../../test/Tools/isac/Interpret/script.sml"
    1.10 -
    1.11 -ML {*
    1.12 -@{term "(SUM i = 0..< k. f i)"}
    1.13 -*}
    1.14 +section {*trials with implicit function, probably required*}
    1.15  ML {*
    1.16  @{term "(%n :: nat. n) 2"};
    1.17  @{term "(%n. n) 2"};
    1.18 @@ -18,8 +12,11 @@
    1.19  @{term "(%n. n+n) a"};
    1.20  @{term "a+a"};
    1.21  *}
    1.22 +section {*sums*}
    1.23  ML {*
    1.24 -@{term "Integral s f k"}
    1.25 +@{term "(SUM i = 0..< k. f i)"}
    1.26 +*}
    1.27 +ML {*
    1.28  *}
    1.29  ML {*
    1.30  *}
    1.31 @@ -28,18 +25,3 @@
    1.32  
    1.33  end
    1.34  
    1.35 -
    1.36 -(*=== inhibit exn ?=============================================================
    1.37 -===== inhibit exn ?===========================================================*)
    1.38 -
    1.39 -
    1.40 -(*========== inhibit exn 110415 ================================================
    1.41 -
    1.42 -"########### testcode inserted vvv ###########################################";
    1.43 -"########### testcode inserted ^^^ ###########################################";
    1.44 -
    1.45 -============ inhibit exn 110415 ==============================================*)
    1.46 -
    1.47 -
    1.48 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.49 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)