neuper@42081: 
neuper@42081: theory Test_SUM imports Isac begin
neuper@42081: 
neuper@42164: section {*trials with implicit function, probably required*}
neuper@42160: ML {*
neuper@42160: @{term "(%n :: nat. n) 2"};
neuper@42160: @{term "(%n. n) 2"};
neuper@42160: @{term "2"};
neuper@42160: *}
neuper@42160: ML {*
neuper@42160: @{term "(%n. n+n)"};
neuper@42160: @{term "(%n. n+n) a"};
neuper@42160: @{term "a+a"};
neuper@42160: *}
neuper@42164: section {*sums*}
neuper@42160: ML {*
jan@42276: val x = @{term "(SUM i = 0..< k. f i)"};
jan@42276: term2str x
neuper@42164: *}
neuper@42164: ML {*
neuper@42081: *}
neuper@42081: ML {*
neuper@42081: *}
neuper@42081: ML {*
neuper@42081: *}
neuper@42081: 
neuper@42081: end
neuper@42081: