| Sun, 04 May 2014 18:53:58 +0200 |
blanchet |
added 'satx' proof method to Try0
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 13:56:48 +0100 |
haftmann |
eliminated odd dislocation of keyword declaration and implementation (leftover from 318cd8ac1817)
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 13:38:28 +0100 |
blanchet |
added 'algebra' and 'meson' to 'try0'
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 20:10:10 +0100 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:34:36 +0200 |
huffman |
remove duplicate [algebra] declarations
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:34:04 +0200 |
huffman |
generalize more div/mod lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:27:49 +0200 |
huffman |
generalize some theorems about div/mod
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
| Fri, 07 May 2010 16:12:25 +0200 |
haftmann |
delete Groebner_Basis directory -- only one file left
|
file |
diff |
annotate
|
| Fri, 07 May 2010 15:05:52 +0200 |
haftmann |
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
proper sublocales; no free-floating ML sections
|
file |
diff |
annotate
|
| Thu, 06 May 2010 18:16:07 +0200 |
haftmann |
moved generic lemmas to appropriate places
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:59:19 +0200 |
haftmann |
dropped duplicate comp_arith
|
file |
diff |
annotate
|
| Thu, 06 May 2010 17:55:11 +0200 |
haftmann |
avoid references to groebner bases in names which have no references to groebner bases
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:40:02 +0200 |
haftmann |
moved presimplification rules for algebraic methods into named thms functor
|
file |
diff |
annotate
|
| Thu, 06 May 2010 16:32:20 +0200 |
haftmann |
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
|
file |
diff |
annotate
|
| Wed, 05 May 2010 16:53:21 +0200 |
haftmann |
moved nat_arith ot Nat_Numeral: clarified normalizer setup
|
file |
diff |
annotate
|
| Wed, 05 May 2010 16:46:19 +0200 |
haftmann |
dropped unused file
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:37:50 +0200 |
haftmann |
use new classes (linordered_)field_inverse_zero
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:17 +0200 |
haftmann |
class division_ring_inverse_zero
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 15:17:59 +0200 |
haftmann |
dequalified fact name
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
moved constants inverse and divide to Ring.thy
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 14:00:43 +0100 |
haftmann |
combined former theories Divides and IntDiv to one theory Divides
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
stripped class recpower further
|
file |
diff |
annotate
|
| Wed, 15 Apr 2009 15:30:39 +0200 |
haftmann |
theory NatBin now named Nat_Numeral
|
file |
diff |
annotate
|
| Sun, 05 Apr 2009 19:21:51 +0100 |
chaieb |
More precise treatement of rational constants by the normalizer for fields
|
file |
diff |
annotate
|
| Sun, 05 Apr 2009 05:07:10 +0100 |
chaieb |
now deals with devision in fields
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:11 +0100 |
haftmann |
dropped theory Arith_Tools
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 18:24:30 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 16:25:52 -0800 |
huffman |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 23:46:03 +0100 |
nipkow |
Removed redundant lemmas
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 20:50:49 +0100 |
nipkow |
removed subsumed lemmas
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Sun, 14 Dec 2008 18:45:51 +0100 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
file |
diff |
annotate
|
| Fri, 12 Dec 2008 20:10:22 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 18:30:26 +0100 |
ballarin |
Conversion of HOL-Main and ZF to new locales.
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 20:36:20 -0800 |
huffman |
separate neg_simps from rel_simps
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 16:05:45 -0800 |
huffman |
remove duplicated lemmas
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 13:30:09 -0800 |
huffman |
include iszero_simps in lemmas comp_arith
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| 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
|