equal
deleted
inserted
replaced
10 |
10 |
11 instance |
11 instance |
12 up :: (domain) domain (up_one_not_zero, up_integral) |
12 up :: (domain) domain (up_one_not_zero, up_integral) |
13 |
13 |
14 consts |
14 consts |
15 EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS |
15 EVAL2 :: "('a::ring => 'b) => 'b => 'a up => 'b::ring" |
16 EVAL :: 'a::ringS => 'a up => 'a |
16 EVAL :: "'a::ring => 'a up => 'a" |
17 |
17 |
18 defs |
18 defs |
19 EVAL2_def "EVAL2 phi a p == |
19 EVAL2_def "EVAL2 phi a p == |
20 setsum (%i. phi (coeff i p) * a ^ i) {..deg p}" |
20 setsum (%i. phi (coeff i p) * a ^ i) {..deg p}" |
21 EVAL_def "EVAL == EVAL2 (%x. x)" |
21 EVAL_def "EVAL == EVAL2 (%x. x)" |