| 2013-08-07 |
wenzelm |
2013-08-07 |
tuned proofs;
|
file | diff | annotate |
| 2012-11-27 |
hoelzl |
2012-11-27 |
add upper bounds for factorial and binomial; add equation for binomial using nat-division (both from AFP/Girth_Chromatic)
|
file | diff | annotate |
| 2012-11-26 |
hoelzl |
2012-11-26 |
add binomial_ge_n_over_k_pow_k
|
file | diff | annotate |
| 2012-08-16 |
wenzelm |
2012-08-16 |
tuned proofs;
|
file | diff | annotate |
| 2012-03-25 |
huffman |
2012-03-25 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| 2012-03-02 |
bulwahn |
2012-03-02 |
removing finiteness goals
|
file | diff | annotate |
| 2012-02-16 |
wenzelm |
2012-02-16 |
tuned proofs;
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-06-08 |
haftmann |
2010-06-08 |
tuned quotes, antiquotations and whitespace
|
file | diff | annotate |
| 2010-04-26 |
haftmann |
2010-04-26 |
dropped group_simps, ring_simps, field_eq_simps
|
file | diff | annotate |
| 2010-04-23 |
haftmann |
2010-04-23 |
epheremal replacement of field_simps by field_eq_simps
|
file | diff | annotate |
| 2010-02-24 |
haftmann |
2010-02-24 |
renamed theory Rational to Rat
|
file | diff | annotate |
| 2009-10-17 |
wenzelm |
2009-10-17 |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
file | diff | annotate |
| 2009-07-23 |
chaieb |
2009-07-23 |
merged
|
file | diff | annotate |
| 2009-07-23 |
chaieb |
2009-07-23 |
More theorems about pochhammer
|
file | diff | annotate |
| 2009-07-15 |
chaieb |
2009-07-15 |
Moved theorem binomial_symmetric from Formal_Power_Series to here
|
file | diff | annotate |
| 2009-07-17 |
avigad |
2009-07-17 |
Changed fact_Suc_nat back to fact_Suc
|
file | diff | annotate |
| 2009-07-14 |
avigad |
2009-07-14 |
Repairs regarding new Fact.thy.
|
file | diff | annotate |
| 2009-05-28 |
huffman |
2009-05-28 |
use class field_char_0
|
file | diff | annotate |
| 2009-05-16 |
nipkow |
2009-05-16 |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
by the new simproc defColl_regroup. More precisely, the simproc pulls an
equation x=t (or t=x) out of a nest of conjunctions to the front where the
simp rule singleton_conj_conv(2) converts to "if".
|
file | diff | annotate |
| 2009-04-29 |
haftmann |
2009-04-29 |
farewell to class recpower
|
file | diff | annotate |
| 2009-04-01 |
nipkow |
2009-04-01 |
cleaned up setprod_zero-related lemmas
|
file | diff | annotate |
| 2009-03-23 |
haftmann |
2009-03-23 |
Main is (Complex_Main) base entry point in library theories
|
file | diff | annotate |
| 2009-03-04 |
huffman |
2009-03-04 |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file | diff | annotate |
| 2009-02-16 |
haftmann |
2009-02-16 |
new primrec
|
file | diff | annotate |
| 2009-02-15 |
nipkow |
2009-02-15 |
more finiteness
|
file | diff | annotate |
| 2009-02-13 |
huffman |
2009-02-13 |
section -> subsection
|
file | diff | annotate |
| 2009-01-30 |
chaieb |
2009-01-30 |
Added a formalization of generalized raising Factorials (Pochhammer's symbol) and binomial coefficients
|
file | diff | annotate |
| 2008-07-07 |
haftmann |
2008-07-07 |
absolute imports of HOL/*.thy theories
|
file | diff | annotate |
| 2008-06-26 |
haftmann |
2008-06-26 |
established Plain theory and image
|
file | diff | annotate |
| 2007-12-18 |
haftmann |
2007-12-18 |
switched from PreList to ATP_Linkup
|
file | diff | annotate |
| 2007-12-10 |
haftmann |
2007-12-10 |
switched import from Main to PreList
|
file | diff | annotate |
| 2007-11-10 |
wenzelm |
2007-11-10 |
tuned document;
|
file | diff | annotate |
| 2007-10-23 |
nipkow |
2007-10-23 |
went back to >0
|
file | diff | annotate |
| 2007-10-21 |
nipkow |
2007-10-21 |
Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.
|
file | diff | annotate |
| 2007-10-20 |
chaieb |
2007-10-20 |
fixed proofs
|
file | diff | annotate |
| 2006-11-09 |
wenzelm |
2006-11-09 |
tuned;
|
file | diff | annotate |
| 2006-11-08 |
wenzelm |
2006-11-08 |
moved theories Parity, GCD, Binomial to Library;
|
file | diff | annotate |