| Sun, 17 Jun 2007 13:39:34 +0200 | chaieb | Tuned error messages; tuned; | changeset | files |
| Sun, 17 Jun 2007 13:39:32 +0200 | chaieb | normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord) | changeset | files |
| Sun, 17 Jun 2007 13:39:29 +0200 | chaieb | added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub | changeset | files |
| Sun, 17 Jun 2007 13:39:27 +0200 | chaieb | moved lemma all_not_ex to HOL.thy ; tuned proofs | changeset | files |
| Sun, 17 Jun 2007 13:39:25 +0200 | chaieb | Tuned instantiation of Groebner bases to fields | changeset | files |
| Sun, 17 Jun 2007 13:39:22 +0200 | chaieb | added Theorem all_not_ex | changeset | files |
| Sun, 17 Jun 2007 08:56:13 +0200 | nipkow | renamed vars in zle_trans for compatibility | changeset | files |