| Thu, 05 Feb 2009 11:45:15 +0100 |
hoelzl |
Added new Float theory and moved old Library/Float.thy to ComputeFloat
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 13:36:11 +0100 |
haftmann |
slightly adapted towards more uniformity with div/mod on nat
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 16:26:47 -0800 |
huffman |
use lemma lists defined in Int.thy
|
file |
diff |
annotate
|
| Sat, 06 Dec 2008 20:25:31 -0800 |
huffman |
fix proofs
|
file |
diff |
annotate
|
| Thu, 04 Dec 2008 18:37:46 -0800 |
huffman |
fix proofs
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:31 +0200 |
haftmann |
proofs adjusted to new situation in Int.thy/Presburger.thy
|
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
|
| Mon, 09 Jul 2007 17:38:40 +0200 |
obua |
added computing oracle support for HOL and numerals
|
file |
diff |
annotate
|