| Fri, 02 Nov 2007 18:53:00 +0100 |
haftmann |
clarified theory target interface
|
changeset |
files
|
| Fri, 02 Nov 2007 18:52:59 +0100 |
haftmann |
more precise treatment of prove_subclass
|
changeset |
files
|
| Fri, 02 Nov 2007 18:52:58 +0100 |
haftmann |
proper reinitialisation after subclass
|
changeset |
files
|
| Fri, 02 Nov 2007 18:52:57 +0100 |
haftmann |
clarified
|
changeset |
files
|
| Fri, 02 Nov 2007 16:38:37 +0100 |
paulson |
tweaked
|
changeset |
files
|
| Fri, 02 Nov 2007 16:38:14 +0100 |
paulson |
recdef to fun
|
changeset |
files
|
| Fri, 02 Nov 2007 15:56:49 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| 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
|
| 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
|