| 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
|
| 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
|
| Mon, 02 Feb 2009 13:56:22 +0100 |
haftmann |
dropped Id
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 21:50:36 -0800 |
huffman |
enable eq_bin_simps for simplifying equalities on numerals
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:31:59 +0200 |
haftmann |
clarified dependencies between arith tools
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Mon, 21 Jul 2008 13:36:59 +0200 |
chaieb |
Tuned and simplified proofs
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Fri, 11 Jul 2008 09:02:22 +0200 |
haftmann |
separate class dvd for divisibility predicate
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:27 +0200 |
haftmann |
moved some code lemmas for Numerals to other theories
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 14:39:50 +0100 |
chaieb |
loads Tools/Qelim/qelim.ML
|
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
|
| Sat, 16 Feb 2008 02:01:13 +0100 |
huffman |
added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 08:45:54 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 17:13:42 +0200 |
chaieb |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:25 +0200 |
wenzelm |
proper context for cooper_tac within arith;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:43 +0200 |
haftmann |
code lemma for of_int
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:11 +0200 |
haftmann |
moved lemma zdvd_period here
|
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 23:49:26 +0200 |
huffman |
section headings
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:47 +0200 |
wenzelm |
moved Presburger setup back to Presburger.thy;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 15:42:14 +0200 |
wenzelm |
adapted tool setup;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 17:28:55 +0200 |
huffman |
remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
|
file |
diff |
annotate
|