| Wed, 04 May 2011 15:37:39 +0200 |
wenzelm |
proper case_names for int_cases, int_of_nat_induct;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 15:58:09 +0100 |
haftmann |
adapted proofs to slightly changed definitions of congruent(2)
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Tue, 11 May 2010 08:36:02 +0200 |
haftmann |
renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution
|
file |
diff |
annotate
|
| Mon, 10 May 2010 14:55:04 +0200 |
haftmann |
moved int induction lemma to theory Int as int_bidirectional_induct
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:51:55 +0200 |
haftmann |
moved lemma zdvd_period to theory Int
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:56 +0200 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| Thu, 06 May 2010 18:16:07 +0200 |
haftmann |
moved generic lemmas to appropriate places
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 12:20:09 +0200 |
haftmann |
got rid of [simplified]
|
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, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Tue, 06 Apr 2010 10:46:28 +0200 |
boehmes |
added missing mult_1_left to linarith simp rules
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 13:14:54 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:55:07 +0100 |
boehmes |
tuned proofs (to avoid linarith error message caused by bootstrapping of HOL)
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 08:40:38 -0800 |
huffman |
add more simp rules for Ints
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Sat, 13 Feb 2010 23:24:57 +0100 |
wenzelm |
modernized structures;
|
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
|
| Mon, 08 Feb 2010 14:06:41 +0100 |
haftmann |
separate library theory for type classes combining lattices with various algebraic structures
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 17:34:18 +0000 |
paulson |
streamlined proofs
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Sun, 08 Nov 2009 19:15:37 +0100 |
wenzelm |
modernized structure Reorient_Proc;
|
file |
diff |
annotate
|