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