| 2015-04-30 |
paulson |
2015-04-30 |
tidying some messy proofs
|
file | diff | annotate |
| 2015-04-28 |
paulson |
2015-04-28 |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file | diff | annotate |
| 2015-04-11 |
paulson |
2015-04-11 |
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
|
file | diff | annotate |
| 2015-01-20 |
hoelzl |
2015-01-20 |
generalized sum_diff_distrib to setsum_subtractf_nat
|
file | diff | annotate |
| 2014-11-13 |
hoelzl |
2014-11-13 |
import general theorems from AFP/Markov_Models
|
file | diff | annotate |
| 2014-11-11 |
noschinl |
2014-11-11 |
add forgotten lemma
|
file | diff | annotate |
| 2014-11-02 |
wenzelm |
2014-11-02 |
modernized header uniformly as section;
|
file | diff | annotate |
| 2014-07-05 |
haftmann |
2014-07-05 |
prefer ac_simps collections over separate name bindings for add and mult
|
file | diff | annotate |
| 2014-07-04 |
haftmann |
2014-07-04 |
reduced name variants for assoc and commute on plus and mult
|
file | diff | annotate |
| 2014-06-30 |
hoelzl |
2014-06-30 |
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
|
file | diff | annotate |
| 2014-06-30 |
hoelzl |
2014-06-30 |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file | diff | annotate |
| 2014-06-28 |
haftmann |
2014-06-28 |
fact consolidation
|
file | diff | annotate |
| 2014-05-30 |
hoelzl |
2014-05-30 |
introduce more powerful reindexing rules for big operators
|
file | diff | annotate |
| 2014-05-29 |
paulson |
2014-05-29 |
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
|
file | diff | annotate |
| 2014-05-13 |
hoelzl |
2014-05-13 |
clean up Lebesgue integration
|
file | diff | annotate |
| 2014-04-09 |
hoelzl |
2014-04-09 |
field_simps: better support for negation and division, and power
|
file | diff | annotate |
| 2014-03-31 |
hoelzl |
2014-03-31 |
add rules about infinity of intervals
|
file | diff | annotate |
| 2014-03-21 |
paulson |
2014-03-21 |
a few new lemmas and generalisations of old ones
|
file | diff | annotate |
| 2014-03-19 |
paulson |
2014-03-19 |
New complex analysis material
|
file | diff | annotate |
| 2014-03-18 |
hoelzl |
2014-03-18 |
fix HOL-NSA; move lemmas
|
file | diff | annotate |
| 2014-03-18 |
hoelzl |
2014-03-18 |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file | diff | annotate |
| 2014-02-24 |
paulson |
2014-02-24 |
Lemmas about Reals, norm, etc., and cleaner variants of existing ones
|
file | diff | annotate |
| 2014-02-24 |
paulson |
2014-02-24 |
A few lemmas about summations, etc.
|
file | diff | annotate |
| 2014-02-02 |
paulson |
2014-02-02 |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file | diff | annotate |
| 2014-01-25 |
wenzelm |
2014-01-25 |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file | diff | annotate |
| 2014-01-20 |
blanchet |
2014-01-20 |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
file | diff | annotate |
| 2014-01-20 |
blanchet |
2014-01-20 |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
|
file | diff | annotate |
| 2013-11-28 |
blanchet |
2013-11-28 |
cleaned up indirect dependency
|
file | diff | annotate |
| 2013-10-18 |
blanchet |
2013-10-18 |
killed most "no_atp", to make Sledgehammer more complete
|
file | diff | annotate |
| 2013-09-03 |
wenzelm |
2013-09-03 |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file | diff | annotate |
| 2013-08-27 |
hoelzl |
2013-08-27 |
renamed inner_dense_linorder to dense_linorder
|
file | diff | annotate |
| 2013-07-25 |
haftmann |
2013-07-25 |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file | diff | annotate |
| 2013-06-15 |
haftmann |
2013-06-15 |
lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd
|
file | diff | annotate |
| 2013-03-05 |
nipkow |
2013-03-05 |
more lemmas about intervals
|
file | diff | annotate |
| 2013-02-20 |
hoelzl |
2013-02-20 |
split dense into inner_dense_order and no_top/no_bot
|
file | diff | annotate |
| 2013-02-20 |
hoelzl |
2013-02-20 |
move auxiliary lemmas from Library/Extended_Reals to HOL image
|
file | diff | annotate |
| 2013-02-15 |
Andreas Lochbihler |
2013-02-15 |
added lemma
|
file | diff | annotate |
| 2013-01-31 |
hoelzl |
2013-01-31 |
introduce order topology
|
file | diff | annotate |
| 2012-12-07 |
hoelzl |
2012-12-07 |
add Int_atMost
|
file | diff | annotate |
| 2012-05-24 |
wenzelm |
2012-05-24 |
tuned proofs;
|
file | diff | annotate |
| 2012-04-03 |
huffman |
2012-04-03 |
modernized obsolete old-style theory name with proper new-style underscore
|
file | diff | annotate | base |