| Wed, 14 Sep 2005 22:04:37 +0200 | wenzelm | imports Commutative_Ring; | changeset | files |
| Wed, 14 Sep 2005 22:04:36 +0200 | wenzelm | HOL: method comm_ring; | changeset | files |
| Wed, 14 Sep 2005 22:04:35 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 14 Sep 2005 22:04:34 +0200 | wenzelm | no longer prefer xemacs, which fails more often than GNU emacs; | changeset | files |
| Wed, 14 Sep 2005 22:04:33 +0200 | wenzelm | Bernhard Haeupler: comm_ring; | changeset | files |
| Wed, 14 Sep 2005 21:44:27 +0200 | chaieb | tactic and the rest eliminated, just the theory.... | changeset | files |
| Wed, 14 Sep 2005 21:35:46 +0200 | chaieb | use was wrong... | changeset | files |
| Wed, 14 Sep 2005 19:03:16 +0200 | obua | Fixed Importer bug in type_introduction: instantiate type variables in rep-abs theorems exactly as it is done in HOL-light. | changeset | files |