| Fri, 07 Nov 2014 15:19:30 +0100 |
wenzelm |
more accurate keywords;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 14:40:14 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Sun, 26 Oct 2014 19:11:16 +0100 |
haftmann |
eliminated redundancies;
|
file |
diff |
annotate
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:53:58 +0200 |
blanchet |
added 'satx' proof method to Try0
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
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, 03 Apr 2012 15:15:00 +0200 |
huffman |
modernized obsolete old-style theory name with proper new-style underscore
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 19:21:05 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 17:08:40 +0100 |
wenzelm |
avoid inconsistent sort constraints;
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Mon, 10 May 2010 15:00:53 +0200 |
haftmann |
shorten names
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:57:04 +0200 |
haftmann |
updated references to ML files
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:55:06 +0200 |
haftmann |
only one module fpr presburger method
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:18:41 +0200 |
haftmann |
tuned theory text; dropped unused lemma
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:11:50 +0200 |
haftmann |
one structure is better than three
|
file |
diff |
annotate
|
| Mon, 10 May 2010 13:58:18 +0200 |
haftmann |
less complex organization of cooper source code
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:51:55 +0200 |
haftmann |
moved lemma zdvd_period to theory Int
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
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, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Thu, 10 Sep 2009 14:07:58 +0200 |
haftmann |
cleanedup theorems all_nat ex_nat
|
file |
diff |
annotate
|