| 2016-05-23 |
wenzelm |
2016-05-23 |
misc tuning and modernization;
|
changeset |
files
|
| 2016-05-23 |
wenzelm |
2016-05-23 |
proper document source;
tuned proofs;
|
changeset |
files
|
| 2016-05-23 |
wenzelm |
2016-05-23 |
misc tuning and modernization;
|
changeset |
files
|
| 2016-05-21 |
nipkow |
2016-05-21 |
merged
|
changeset |
files
|
| 2016-05-21 |
nipkow |
2016-05-21 |
added timing lemmas
|
changeset |
files
|
| 2016-05-20 |
immler |
2016-05-20 |
uniformly continuous function extended continuously on closure
|
changeset |
files
|
| 2016-05-20 |
immler |
2016-05-20 |
reduce isUCont to uniformly_continuous_on
|
changeset |
files
|
| 2016-05-20 |
immler |
2016-05-20 |
removed smt proof
|
changeset |
files
|
| 2016-05-20 |
fleury |
2016-05-20 |
better handling of veriT's 'unknown' status
|
changeset |
files
|
| 2016-05-18 |
Manuel Eberl |
2016-05-18 |
Resolved name clash
|
changeset |
files
|
| 2016-05-17 |
eberlm |
2016-05-17 |
Merged
|
changeset |
files
|
| 2016-05-17 |
eberlm |
2016-05-17 |
Moved material from AFP/Randomised_Social_Choice to distribution
|
changeset |
files
|
| 2016-05-17 |
hoelzl |
2016-05-17 |
Library: add partition_on
|
changeset |
files
|
| 2016-05-17 |
blanchet |
2016-05-17 |
proper consideration of chained facts in 'try0' minimization
|
changeset |
files
|
| 2016-05-14 |
wenzelm |
2016-05-14 |
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
|
changeset |
files
|
| 2016-05-14 |
wenzelm |
2016-05-14 |
tuned;
|
changeset |
files
|
| 2016-05-14 |
wenzelm |
2016-05-14 |
toplevel theorem statements support 'if'/'for' eigen-context;
|
changeset |
files
|
| 2016-05-14 |
wenzelm |
2016-05-14 |
reverted accidental commit;
|
changeset |
files
|
| 2016-05-13 |
wenzelm |
2016-05-13 |
eliminated use of empty "assms";
|
changeset |
files
|
| 2016-05-13 |
wenzelm |
2016-05-13 |
more complete theories;
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
common entity definitions within a global or local theory context;
|
changeset |
files
|
| 2016-05-12 |
haftmann |
2016-05-12 |
clarified heading
|
changeset |
files
|
| 2016-05-12 |
haftmann |
2016-05-12 |
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
merged
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
avoid spurious fact index, notably in "context begin" (via Bundle.context);
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
tuned;
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
tuned;
|
changeset |
files
|
| 2016-05-12 |
wenzelm |
2016-05-12 |
tuned;
|
changeset |
files
|
| 2016-05-12 |
Lars Hupel |
2016-05-12 |
expose Sessions.Info in Build.Results
|
changeset |
files
|
| 2016-05-11 |
immler |
2016-05-11 |
introduced class topological_group between topological_monoid and real_normed_vector
|
changeset |
files
|
| 2016-05-10 |
wenzelm |
2016-05-10 |
find dynamic facts as well, but static ones are preferred;
tuned;
|
changeset |
files
|
| 2016-05-10 |
immler |
2016-05-10 |
some slight generalizations
|
changeset |
files
|
| 2016-05-10 |
paulson |
2016-05-10 |
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
Minkowski theorem
|
changeset |
files
|
| 2016-05-10 |
paulson |
2016-05-10 |
two new lemmas about segments
|
changeset |
files
|
| 2016-05-09 |
paulson |
2016-05-09 |
Merge
|
changeset |
files
|
| 2016-05-09 |
paulson |
2016-05-09 |
lemmas about dimension, hyperplanes, span, etc.
|
changeset |
files
|
| 2016-05-09 |
wenzelm |
2016-05-09 |
merged
|
changeset |
files
|
| 2016-05-09 |
wenzelm |
2016-05-09 |
clarified context, notably for internal use of Simplifier;
|
changeset |
files
|
| 2016-05-09 |
paulson |
2016-05-09 |
renamings and refinements
|
changeset |
files
|
| 2016-05-04 |
hoelzl |
2016-05-04 |
move Stirling numbers from AFP/Discrete_Summation
|
changeset |
files
|
| 2016-05-01 |
nipkow |
2016-05-01 |
the standard While-rule
|
changeset |
files
|
| 2016-04-29 |
wenzelm |
2016-04-29 |
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
|
changeset |
files
|
| 2016-04-28 |
wenzelm |
2016-04-28 |
unfold is subject to unfold_abs_def (still inactive);
tuned signature;
|
changeset |
files
|
| 2016-04-28 |
wenzelm |
2016-04-28 |
tuned;
|
changeset |
files
|
| 2016-04-28 |
wenzelm |
2016-04-28 |
NEWS;
|
changeset |
files
|
| 2016-04-28 |
wenzelm |
2016-04-28 |
clarified order: params/prems/concl interchangeable with !!/==> proposition;
|
changeset |
files
|
| 2016-04-28 |
wenzelm |
2016-04-28 |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;
|
changeset |
files
|
| 2016-04-27 |
wenzelm |
2016-04-27 |
tuned;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
merged
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
updated subtle side-conditions;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
some uses of 'obtain' with structure statement;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
'obtain' supports structured statements (similar to 'define');
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
more portable: GNU find no longer supports "-perm +mode";
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
more uniform operations for structured statements;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
defs are closed, which leads to proper auto_bind_facts;
misc tuning;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
tuned notation;
|
changeset |
files
|
| 2016-04-26 |
wenzelm |
2016-04-26 |
misc tuning and modernization;
|
changeset |
files
|
| 2016-04-22 |
hoelzl |
2016-04-22 |
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
|
changeset |
files
|
| 2016-04-22 |
hoelzl |
2016-04-22 |
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
|
changeset |
files
|
| 2016-04-22 |
hoelzl |
2016-04-22 |
Linear_Algebra: alternative representation of linear combination
|
changeset |
files
|