| Fri, 23 Apr 2010 16:17:24 +0200 | haftmann | dequalified fact name | changeset | files |
| Fri, 23 Apr 2010 15:18:00 +0200 | haftmann | sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit | changeset | files |
| 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 |