Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
file |
diff |
annotate
|
Mon, 29 Sep 2008 12:31:59 +0200 |
haftmann |
clarified dependencies between arith tools
|
file |
diff |
annotate
|
Mon, 21 Jul 2008 13:36:39 +0200 |
chaieb |
Relevant rules added to algebra's context
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 19:43:54 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
Tue, 18 Mar 2008 20:33:28 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
Wed, 05 Mar 2008 21:24:03 +0100 |
wenzelm |
explicit referencing of background facts;
|
file |
diff |
annotate
|
Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
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)
|
file |
diff |
annotate
|
Thu, 05 Jul 2007 00:06:10 +0200 |
wenzelm |
common normalizer_funs, avoid cterm_of;
|
file |
diff |
annotate
|
Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
Thu, 21 Jun 2007 15:42:12 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Tue, 12 Jun 2007 10:15:32 +0200 |
chaieb |
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 18:28:16 +0200 |
chaieb |
Conversion for computation on constants now depends on the context
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 16:23:17 +0200 |
chaieb |
Added instantiation of algebra method to fields
|
file |
diff |
annotate
|
Mon, 11 Jun 2007 11:05:57 +0200 |
chaieb |
explicitely depends on file groebner.ML
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 22:46:53 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 18:36:07 +0200 |
wenzelm |
renamed locale ring/semiring to gb_ring/gb_semiring to avoid clash with Ring_and_Field versions;
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 16:26:04 +0200 |
wenzelm |
Semiring normalization and Groebner Bases.
|
file |
diff |
annotate
|