Tue, 26 Mar 2013 12:20:54 +0100 |
hoelzl |
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
|
file |
diff |
annotate
|
Tue, 26 Mar 2013 12:20:53 +0100 |
hoelzl |
remove posreal_complete
|
file |
diff |
annotate
|
Tue, 26 Mar 2013 12:20:52 +0100 |
hoelzl |
separate SupInf into Conditional_Complete_Lattice, move instantiation of real to RealDef
|
file |
diff |
annotate
|
Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
Wed, 18 Apr 2012 14:29:19 +0200 |
hoelzl |
add lemma to equate floor and div
|
file |
diff |
annotate
|
Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
Sat, 25 Feb 2012 09:07:41 +0100 |
bulwahn |
removing unnecessary assumptions in RComplete;
|
file |
diff |
annotate
|
Sat, 24 Dec 2011 15:53:09 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Sun, 04 Sep 2011 06:56:10 -0700 |
huffman |
remove unused assumptions from natceiling lemmas
|
file |
diff |
annotate
|
Sun, 04 Sep 2011 06:27:59 -0700 |
huffman |
move lemmas nat_le_iff and nat_mono into Int.thy
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 11:10:38 -0700 |
huffman |
remove unused assumption from lemma posreal_complete
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 08:01:49 -0700 |
huffman |
shorten some proofs
|
file |
diff |
annotate
|
Fri, 02 Sep 2011 20:58:31 -0700 |
huffman |
remove redundant simp rules ceiling_floor and floor_ceiling
|
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
|
Fri, 02 Sep 2011 15:19:59 -0700 |
huffman |
simplify proof of Rats_dense_in_real;
|
file |
diff |
annotate
|