| Tue, 24 May 2016 17:42:14 +0200 |
eberlm |
Deleted problematic code equation in Codegenerator_Test
|
changeset |
files
|
| Tue, 24 May 2016 15:16:15 +0100 |
paulson |
Merge
|
changeset |
files
|
| Tue, 24 May 2016 15:08:33 +0100 |
paulson |
New theory for Homeomorphisms
|
changeset |
files
|
| Tue, 24 May 2016 15:08:07 +0100 |
paulson |
Merge
|
changeset |
files
|
| Tue, 24 May 2016 13:57:34 +0100 |
paulson |
renamings and new material
|
changeset |
files
|
| Tue, 24 May 2016 13:57:04 +0100 |
paulson |
new theorem
|
changeset |
files
|
| Mon, 23 May 2016 16:03:29 +0100 |
paulson |
deleted stray thm command
|
changeset |
files
|
| Mon, 23 May 2016 16:02:46 +0100 |
paulson |
deleted needless comment
|
changeset |
files
|
| Tue, 24 May 2016 15:44:10 +0200 |
eberlm |
Resolved cyclic dependency of theories
|
changeset |
files
|
| Tue, 24 May 2016 15:05:59 +0200 |
eberlm |
Merged
|
changeset |
files
|
| Tue, 24 May 2016 15:05:41 +0200 |
eberlm |
Added set permutations/random permutations
|
changeset |
files
|
| Tue, 24 May 2016 11:39:26 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 23 May 2016 21:30:30 +0200 |
wenzelm |
embedded content may be delimited via cartouches;
|
changeset |
files
|
| Mon, 23 May 2016 20:45:10 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 23 May 2016 22:43:22 +0200 |
nipkow |
merged
|
changeset |
files
|
| Mon, 23 May 2016 22:43:11 +0200 |
nipkow |
renamed prefix* in Library/Sublist
|
changeset |
files
|
| Mon, 23 May 2016 18:04:45 +0200 |
blanchet |
generate Vampire 4.0 compatible output
|
changeset |
files
|
| Mon, 23 May 2016 15:46:30 +0100 |
paulson |
Merge
|
changeset |
files
|
| Mon, 23 May 2016 15:33:24 +0100 |
paulson |
Lots of new material for multivariate analysis
|
changeset |
files
|
| Mon, 23 May 2016 15:30:13 +0200 |
wenzelm |
removed odd cases rule (see also 8cb42cd97579);
|
changeset |
files
|
| Mon, 23 May 2016 15:29:38 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 23 May 2016 14:56:48 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Mon, 23 May 2016 14:43:14 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Mon, 23 May 2016 12:48:24 +0200 |
wenzelm |
proper document source;
|
changeset |
files
|
| Mon, 23 May 2016 12:18:16 +0200 |
wenzelm |
misc tuning and modernization;
|
changeset |
files
|
| Sat, 21 May 2016 07:08:59 +0200 |
nipkow |
merged
|
changeset |
files
|
| Sat, 21 May 2016 07:08:46 +0200 |
nipkow |
added timing lemmas
|
changeset |
files
|
| Fri, 20 May 2016 22:01:42 +0200 |
immler |
uniformly continuous function extended continuously on closure
|
changeset |
files
|
| Fri, 20 May 2016 21:21:28 +0200 |
immler |
reduce isUCont to uniformly_continuous_on
|
changeset |
files
|
| Fri, 20 May 2016 22:01:39 +0200 |
immler |
removed smt proof
|
changeset |
files
|
| Fri, 20 May 2016 07:54:54 +0200 |
fleury |
better handling of veriT's 'unknown' status
|
changeset |
files
|
| Wed, 18 May 2016 12:24:33 +0200 |
Manuel Eberl |
Resolved name clash
|
changeset |
files
|
| Tue, 17 May 2016 19:27:42 +0200 |
eberlm |
Merged
|
changeset |
files
|
| Tue, 17 May 2016 17:05:35 +0200 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
changeset |
files
|
| Tue, 17 May 2016 11:16:39 +0200 |
hoelzl |
Library: add partition_on
|
changeset |
files
|
| Tue, 17 May 2016 08:40:24 +0200 |
blanchet |
proper consideration of chained facts in 'try0' minimization
|
changeset |
files
|
| Sat, 14 May 2016 22:00:44 +0200 |
wenzelm |
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
|
changeset |
files
|
| Sat, 14 May 2016 19:59:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 14 May 2016 19:49:10 +0200 |
wenzelm |
toplevel theorem statements support 'if'/'for' eigen-context;
|
changeset |
files
|
| Sat, 14 May 2016 13:52:01 +0200 |
wenzelm |
reverted accidental commit;
|
changeset |
files
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
changeset |
files
|
| Fri, 13 May 2016 20:22:02 +0200 |
wenzelm |
more complete theories;
|
changeset |
files
|
| Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
changeset |
files
|
| Thu, 12 May 2016 14:38:53 +0200 |
haftmann |
clarified heading
|
changeset |
files
|
| Thu, 12 May 2016 09:34:07 +0200 |
haftmann |
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
|
changeset |
files
|
| Thu, 12 May 2016 11:34:19 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 12 May 2016 10:57:09 +0200 |
wenzelm |
avoid spurious fact index, notably in "context begin" (via Bundle.context);
|
changeset |
files
|
| Thu, 12 May 2016 10:21:59 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 12 May 2016 10:16:52 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 12 May 2016 10:03:17 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 12 May 2016 10:31:25 +0200 |
Lars Hupel |
expose Sessions.Info in Build.Results
|
changeset |
files
|
| Wed, 11 May 2016 16:13:17 +0200 |
immler |
introduced class topological_group between topological_monoid and real_normed_vector
|
changeset |
files
|
| Tue, 10 May 2016 22:25:06 +0200 |
wenzelm |
find dynamic facts as well, but static ones are preferred;
|
changeset |
files
|
| Tue, 10 May 2016 15:48:37 +0200 |
immler |
some slight generalizations
|
changeset |
files
|
| Tue, 10 May 2016 14:04:44 +0100 |
paulson |
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
|
changeset |
files
|
| Tue, 10 May 2016 11:56:23 +0100 |
paulson |
two new lemmas about segments
|
changeset |
files
|
| Mon, 09 May 2016 17:32:26 +0100 |
paulson |
Merge
|
changeset |
files
|
| Mon, 09 May 2016 17:23:19 +0100 |
paulson |
lemmas about dimension, hyperplanes, span, etc.
|
changeset |
files
|
| Mon, 09 May 2016 17:22:32 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 09 May 2016 14:37:47 +0200 |
wenzelm |
clarified context, notably for internal use of Simplifier;
|
changeset |
files
|