Thu, 10 Jan 2013 21:22:11 +0100 |
noschinl |
added some ereal_of_enat_* lemmas (from $AFP/thys/Girth_Chromatic)
|
file |
diff |
annotate
|
Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Thu, 22 Mar 2012 16:44:19 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Tue, 20 Dec 2011 11:40:56 +0100 |
noschinl |
add simp rules for enat and ereal
|
file |
diff |
annotate
|
Mon, 05 Dec 2011 17:33:57 +0100 |
hoelzl |
real is better supported than real_of_nat, use it in the nat => ereal coercion
|
file |
diff |
annotate
|
Fri, 21 Oct 2011 14:25:38 +0200 |
bulwahn |
replacing metis proofs with facts xt1 by new proof with more readable names
|
file |
diff |
annotate
|
Wed, 21 Sep 2011 08:28:53 -0700 |
huffman |
remove redundant instantiation ereal :: power
|
file |
diff |
annotate
|
Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 16:48:30 -0700 |
huffman |
remove redundant lemma reals_complete2 in favor of complete_real
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 11:56:20 -0700 |
huffman |
remove duplicate simp declaration
|
file |
diff |
annotate
|
Fri, 12 Aug 2011 09:17:24 -0700 |
huffman |
make Multivariate_Analysis work with separate set type
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
Thu, 21 Jul 2011 22:47:13 +0200 |
haftmann |
moved some lemmas
|
file |
diff |
annotate
|
Thu, 21 Jul 2011 18:40:31 +0200 |
haftmann |
ereal is a complete_linorder instance
|
file |
diff |
annotate
|
Wed, 20 Jul 2011 15:42:23 +0200 |
hoelzl |
add code generator setup and tests for ereal
|
file |
diff |
annotate
|
Tue, 19 Jul 2011 14:38:48 +0200 |
hoelzl |
rename Fin to enat
|
file |
diff |
annotate
|
Tue, 19 Jul 2011 14:38:29 +0200 |
hoelzl |
add ereal to typeclass infinity
|
file |
diff |
annotate
|
Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
| base
|