src/HOL/Algebra/poly/ProtoPoly.thy
author paulson
Fri, 05 Nov 1999 11:14:26 +0100
changeset 7998 3d0c34795831
child 11093 62c2e0af1d30
permissions -rw-r--r--
Algebra and Polynomial theories, by Clemens Ballarin
     1 (*
     2     Prepearing definitions for polynomials
     3     $Id$
     4     Author: Clemens Ballarin, started 9 December 1996
     5 *)
     6 
     7 ProtoPoly = Abstract +
     8 
     9 consts
    10   bound :: [nat, nat => 'a::ringS] => bool
    11 
    12 defs
    13   bound_def  "bound n f == ALL i. n<i --> f i = <0>"
    14 
    15 end