| 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
|
| Fri, 02 Sep 2011 14:27:55 -0700 |
huffman |
remove unused, unnecessary lemmas
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Tue, 18 May 2010 19:00:55 -0700 |
huffman |
remove several redundant lemmas about floor and ceiling
|
file |
diff |
annotate
|
| Tue, 11 May 2010 09:10:31 -0700 |
huffman |
move floor lemmas from RealPow.thy to RComplete.thy
|
file |
diff |
annotate
|
| Mon, 10 May 2010 12:12:58 -0700 |
huffman |
new construction of real numbers using Cauchy sequences
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 17:28:45 +0100 |
hoelzl |
Added natfloor and floor rules for multiplication and power.
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2009 13:47:28 +0100 |
paulson |
New lemmas involving the real numbers, especially limits and series
|
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
|
| Thu, 26 Feb 2009 20:56:59 +0100 |
wenzelm |
standard headers;
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 06:21:31 -0800 |
huffman |
disable floor_minus and ceiling_minus [simp]
|
file |
diff |
annotate
|
| Wed, 25 Feb 2009 11:29:59 -0800 |
huffman |
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
|
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 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|