Mon, 21 Jul 2008 13:37:05 +0200 | chaieb | Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy | changeset | files |
Mon, 21 Jul 2008 13:36:59 +0200 | chaieb | Tuned and simplified proofs | changeset | files |
Mon, 21 Jul 2008 13:36:44 +0200 | chaieb | Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra | changeset | files |