Fri, 23 Apr 2010 15:18:00 +0200 | haftmann | separated instantiation of division_by_zero | changeset | files |
Fri, 23 Apr 2010 15:17:59 +0200 | haftmann | dequalified fact name | changeset | files |
Fri, 23 Apr 2010 15:17:59 +0200 | haftmann | less special treatment of times_divide_eq [simp] | changeset | files |
Fri, 23 Apr 2010 15:17:59 +0200 | haftmann | sharpened constraint (c.f. 4e7f5b22dd7d) | changeset | files |
Fri, 23 Apr 2010 13:58:15 +0200 | haftmann | more localization; tuned proofs | changeset | files |
Fri, 23 Apr 2010 13:58:14 +0200 | haftmann | more localization; factored out lemmas for division_ring | changeset | files |
Fri, 23 Apr 2010 13:58:14 +0200 | haftmann | modernized abstract algebra theories | changeset | files |
Fri, 23 Apr 2010 10:50:17 +0200 | haftmann | merged | changeset | files |