author | wenzelm |
Mon, 11 Feb 2002 10:56:33 +0100 | |
changeset 12873 | d7f8dfaad46d |
parent 5078 | 7b5ea59c0275 |
permissions | -rw-r--r-- |
(* Title: HOL/Integ/Ring.thy ID: $Id$ Author: Tobias Nipkow Copyright 1996 TU Muenchen Bits of rings. Main output: a simplification tactic for commutative rings. *) Ring = Group + (* Ring *) axclass ring < add_agroup, times times_assoc "(x*y)*z = x*(y*z)" distribL "x*(y+z) = x*y + x*z" distribR "(x+y)*z = x*z + y*z" (* Commutative ring *) axclass cring < ring times_commute "x*y = y*x" end