| Wed, 31 Oct 2007 12:19:37 +0100 | chaieb | (1) signatures updated according to normalizer_data.ML (added field ideal in entry); | changeset | files |
| Wed, 31 Oct 2007 12:19:35 +0100 | chaieb | (1) added axiom to ringb and theorems to enable algebra to prove the ideal membership problem; (2) Method algebra now calls algebra_tac which first tries to solve a universal formula, then in case of failure trie to solve the ideal membership problem (see HOL/Tools/Groebner_Basis/groebner.ML) | changeset | files |
| Wed, 31 Oct 2007 12:19:33 +0100 | chaieb | exported field_comp_conv: a numerical conversion over fields | changeset | files |
| Wed, 31 Oct 2007 10:37:14 +0100 | haftmann | dropped AxClass | changeset | files |
| Wed, 31 Oct 2007 10:10:50 +0100 | haftmann | tuned | changeset | files |
| Tue, 30 Oct 2007 17:58:03 +0100 | berghofe | Handle Subscript exception when looking up bound variables. | changeset | files |
| Tue, 30 Oct 2007 17:56:56 +0100 | berghofe | Added well-formedness check to Abst case in function prf_of. | changeset | files |