author | kleing |
Sat, 01 Mar 2003 16:45:51 +0100 | |
changeset 13840 | 399c8103a98f |
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