src/HOL/Integ/Ring.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2281 e00c13a29eda
permissions -rw-r--r--
added AxClasses test;
     1 (*  Title:      HOL/Integ/Ring.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TU Muenchen
     5 
     6 Bits of rings.
     7 Main output: a simplification tactic for commutative rings.
     8 *)
     9 
    10 Ring = Group +
    11 
    12 (* Ring *)
    13 
    14 axclass  ring < add_agroup, times
    15   times_assoc "(x*y)*z = x*(y*z)"
    16   distribL    "x*(y+z) = x*y + x*z"
    17   distribR    "(x+y)*z = x*z + y*z"
    18 
    19 (* Commutative ring *)
    20 
    21 axclass cring < ring
    22   times_commute "x*y = y*x"
    23 
    24 end