src/HOL/Algebra/poly/ProtoPoly.thy
author nipkow
Mon, 13 May 2002 15:27:28 +0200
changeset 13145 59bc43b51aa2
parent 11093 62c2e0af1d30
permissions -rw-r--r--
*** empty log message ***

(*
    Prepearing definitions for polynomials
    $Id$
    Author: Clemens Ballarin, started 9 December 1996
*)

ProtoPoly = Abstract +

consts
  bound :: [nat, nat => 'a::ringS] => bool

defs
  bound_def  "bound n f == ALL i. n<i --> f i = 0"

end