| Sun, 17 Jun 2007 13:39:50 +0200 | chaieb | moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs | changeset | files |
| Sun, 17 Jun 2007 13:39:48 +0200 | chaieb | Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl | changeset | files |
| Sun, 17 Jun 2007 13:39:45 +0200 | chaieb | gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f; | changeset | files |