| Fri, 02 Nov 2007 12:35:27 +0100 |
kleing |
Added reference to Jeremy Dawson's paper on the word library.
|
changeset |
files
|
| Fri, 02 Nov 2007 08:59:15 +0100 |
nipkow |
recdef -> fun
|
changeset |
files
|
| Fri, 02 Nov 2007 08:26:01 +0100 |
nipkow |
added Fun
|
changeset |
files
|
| Fri, 02 Nov 2007 08:17:33 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 01 Nov 2007 20:20:19 +0100 |
nipkow |
recdef -> fun
|
changeset |
files
|
| Thu, 01 Nov 2007 13:44:44 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 31 Oct 2007 15:10:34 +0100 |
paulson |
Catch exceptions arising during the abstraction operation.
|
changeset |
files
|
| Wed, 31 Oct 2007 12:19:45 +0100 |
chaieb |
Added example for the ideal membership problem solved by algebra
|
changeset |
files
|
| Wed, 31 Oct 2007 12:19:44 +0100 |
chaieb |
Added field ideal into entry - uses by algebra method to prove the ideal membership problem
|
changeset |
files
|
| Wed, 31 Oct 2007 12:19:43 +0100 |
chaieb |
changed signature according to normalizer_data.ML
|
changeset |
files
|
| Wed, 31 Oct 2007 12:19:41 +0100 |
chaieb |
tuned
|
changeset |
files
|
| 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
|