ring instead of ringS;
authorwenzelm
Mon Oct 15 20:34:26 2001 +0200 (2001-10-15)
changeset 117791aa328cb273a
parent 11778 37efbe093d3c
child 11780 d17ee2241257
ring instead of ringS;
src/HOL/Algebra/poly/PolyHomo.thy
     1.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Mon Oct 15 20:34:12 2001 +0200
     1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Mon Oct 15 20:34:26 2001 +0200
     1.3 @@ -12,8 +12,8 @@
     1.4    up :: (domain) domain (up_one_not_zero, up_integral)
     1.5  
     1.6  consts
     1.7 -  EVAL2	:: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
     1.8 -  EVAL	:: 'a::ringS => 'a up => 'a
     1.9 +  EVAL2	:: "('a::ring => 'b) => 'b => 'a up => 'b::ring"
    1.10 +  EVAL	:: "'a::ring => 'a up => 'a"
    1.11  
    1.12  defs
    1.13    EVAL2_def	"EVAL2 phi a p ==