| Tue, 11 May 2010 12:05:19 -0700 |
removed lemma real_sq_order; use power2_le_imp_le instead
|
file | diff | annotate |
| Tue, 11 May 2010 09:10:31 -0700 |
move floor lemmas from RealPow.thy to RComplete.thy
|
file | diff | annotate |
| Tue, 11 May 2010 06:30:48 -0700 |
move some theorems from RealPow.thy to Transcendental.thy
|
file | diff | annotate |
| Mon, 10 May 2010 21:27:52 -0700 |
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
|
file | diff | annotate |
| Sun, 09 May 2010 17:47:43 -0700 |
avoid using real-specific versions of generic lemmas
|
file | diff | annotate |
| Sun, 07 Mar 2010 07:29:34 -0800 |
generalize some lemmas, and remove a few unnecessary ones
|
file | diff | annotate |
| Thu, 04 Mar 2010 17:28:45 +0100 |
Added natfloor and floor rules for multiplication and power.
|
file | diff | annotate |
| Wed, 24 Feb 2010 14:13:15 -0800 |
remove redundant lemma real_minus_half_eq
|
file | diff | annotate |
| Tue, 23 Feb 2010 14:44:24 -0800 |
remove redundant lemma realpow_increasing
|
file | diff | annotate |
| Tue, 23 Feb 2010 14:38:06 -0800 |
remove redundant simp rules from RealPow.thy
|
file | diff | annotate |
| Tue, 23 Feb 2010 10:37:25 -0800 |
moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
|
file | diff | annotate |
| Tue, 23 Feb 2010 07:45:54 -0800 |
move float syntax from RealPow to Rational
|
file | diff | annotate |
| Thu, 18 Feb 2010 14:21:44 -0800 |
get rid of many duplicate simp rule warnings
|
file | diff | annotate |
| Sat, 13 Feb 2010 23:24:57 +0100 |
modernized structures;
|
file | diff | annotate |
| Wed, 29 Apr 2009 14:20:26 +0200 |
farewell to class recpower
|
file | diff | annotate |
| Tue, 28 Apr 2009 15:50:29 +0200 |
collected square lemmas in Nat_Numeral
|
file | diff | annotate |
| Wed, 22 Apr 2009 19:09:21 +0200 |
power operation defined generic
|
file | diff | annotate |
| Wed, 04 Mar 2009 17:12:23 -0800 |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file | diff | annotate |
| Tue, 24 Feb 2009 11:12:58 -0800 |
make more proofs work whether or not One_nat_def is a simp rule
|
file | diff | annotate |
| Wed, 28 Jan 2009 16:29:16 +0100 |
Replaced group_ and ring_simps by algebra_simps;
|
file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file | diff | annotate | base |