| author | wenzelm |
| Thu, 16 Mar 2000 00:32:55 +0100 | |
| changeset 8488 | 58e37d59c146 |
| parent 7998 | 3d0c34795831 |
| child 10448 | da7d0e28f746 |
| permissions | -rw-r--r-- |
(* Instantiate polynomials to form a ring and prove further properties $Id$ Author: Clemens Ballarin, started 20 January 1997 *) PolyRing = UnivPoly + instance up :: (ring) ring (up_a_assoc, up_l_zero, up_l_neg, up_a_comm, up_m_assoc, up_l_one, up_l_distr, up_m_comm, up_one_not_zero, up_power_def) {| rtac refl 1 |} end