author | wenzelm |
Mon, 15 Oct 2001 20:34:26 +0200 | |
changeset 11779 | 1aa328cb273a |
parent 11778 | 37efbe093d3c |
child 11780 | d17ee2241257 |
--- a/src/HOL/Algebra/poly/PolyHomo.thy Mon Oct 15 20:34:12 2001 +0200 +++ b/src/HOL/Algebra/poly/PolyHomo.thy Mon Oct 15 20:34:26 2001 +0200 @@ -12,8 +12,8 @@ up :: (domain) domain (up_one_not_zero, up_integral) consts - EVAL2 :: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS - EVAL :: 'a::ringS => 'a up => 'a + EVAL2 :: "('a::ring => 'b) => 'b => 'a up => 'b::ring" + EVAL :: "'a::ring => 'a up => 'a" defs EVAL2_def "EVAL2 phi a p ==