| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 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
|
| Thu, 23 Oct 2014 19:40:39 +0200 |
haftmann |
further downshift of theory Parity in the hierarchy
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 14:27:41 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| 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
|