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