src/HOL/Algebra/poly/PolyHomo.thy
changeset 17479 68a7acb5f22e
parent 13936 d3671b878828
child 21423 6cdd0589aa73
     1.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Sat Sep 17 20:16:35 2005 +0200
     1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Sat Sep 17 20:49:14 2005 +0200
     1.3 @@ -4,15 +4,15 @@
     1.4      Author: Clemens Ballarin, started 15 April 1997
     1.5  *)
     1.6  
     1.7 -PolyHomo = UnivPoly2 +
     1.8 +theory PolyHomo imports UnivPoly2 begin
     1.9  
    1.10  consts
    1.11    EVAL2	:: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
    1.12    EVAL	:: "['a::ring, 'a up] => 'a"
    1.13  
    1.14  defs
    1.15 -  EVAL2_def	"EVAL2 phi a p ==
    1.16 +  EVAL2_def:	"EVAL2 phi a p ==
    1.17                   setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
    1.18 -  EVAL_def	"EVAL == EVAL2 (%x. x)"
    1.19 +  EVAL_def:	"EVAL == EVAL2 (%x. x)"
    1.20  
    1.21  end