Mon, 25 Feb 2008 12:04:09 +0100 | chaieb | Pocklington's Primality criterion | changeset | files |
Mon, 25 Feb 2008 11:59:57 +0100 | chaieb | More primality theorems | changeset | files |
Mon, 25 Feb 2008 11:27:27 +0100 | chaieb | A library for univariate polynomials -- generalizes old Hyperreal/Poly.thy from reals to locales | changeset | files |
Mon, 25 Feb 2008 11:27:25 +0100 | chaieb | A proof a the fundamental theorem of algebra | changeset | files |
Mon, 25 Feb 2008 11:27:08 +0100 | chaieb | Uses Univ_Poly.thy | changeset | files |
Mon, 25 Feb 2008 11:27:07 +0100 | chaieb | Does not import Poly anymore | changeset | files |
Mon, 25 Feb 2008 11:27:05 +0100 | chaieb | Includes the derivates of polynomials -- reals specific content of Poly | changeset | files |
Mon, 25 Feb 2008 11:27:03 +0100 | chaieb | Two simple theorems about cmod moved to Complex.thy | changeset | files |