| 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
|
| Sun, 01 Mar 2009 12:01:57 +0100 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 20:56:59 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 20:53:58 -0800 |
huffman |
add header
|
file |
diff |
annotate
|
| 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:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Tue, 09 Dec 2008 22:13:16 -0800 |
huffman |
move all neg-related lemmas to NatBin; make type of neg specific to int
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 21:50:36 -0800 |
huffman |
enable eq_bin_simps for simplifying equalities on numerals
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 21:00:39 -0800 |
huffman |
fix proofs related to simplification of inequalities on numerals
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|