280 monom2term((~5,[5]),vs); |
280 monom2term((~5,[5]),vs); |
281 monom2term((~1,[2]),vs); |
281 monom2term((~1,[2]),vs); |
282 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*) |
282 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*) |
283 |
283 |
284 val (i,is) = (~1,[2]); |
284 val (i,is) = (~1,[2]); |
285 val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ |
285 val ttt = Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $ |
286 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $ |
286 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $ |
287 Free ((str_of_int o abs) i, HOLogic.realT)) $ |
287 Free ((str_of_int o abs) i, HOLogic.realT)) $ |
288 powerproduct2term(is, vs); |
288 powerproduct2term(is, vs); |
289 term2str ttt; |
289 term2str ttt; |
290 -------versuche 13.3.03-----*) |
290 -------versuche 13.3.03-----*) |