| Thu, 26 May 2016 15:31:04 +0200 |
haftmann |
examples and documentation for code generator time measurements
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
optional timing for code generator conversions
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified internal interfaces
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
delegate inclusion of required dictionaries to user-space instead of half-working magic
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
corrected closure scope of static_conv_thingol;
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified proof context vs. background theory
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified naming conventions and code for code evaluation sandwiches
|
changeset |
files
|
| Thu, 26 May 2016 15:27:50 +0200 |
haftmann |
clarified names of variants
|
changeset |
files
|
| Thu, 26 May 2016 09:05:00 +0200 |
nipkow |
added function "prefixes" and some lemmas
|
changeset |
files
|
| Wed, 25 May 2016 16:52:19 +0100 |
paulson |
Merge
|
changeset |
files
|
| Wed, 25 May 2016 16:47:08 +0100 |
paulson |
Merge
|
changeset |
files
|
| Wed, 25 May 2016 16:39:07 +0100 |
paulson |
moved two theorems
|
changeset |
files
|
| Wed, 25 May 2016 16:38:35 +0100 |
paulson |
updated proof of Residue Theorem (form Wenda Li)
|
changeset |
files
|
| Wed, 25 May 2016 17:41:35 +0200 |
nipkow |
merged
|
changeset |
files
|
| Wed, 25 May 2016 17:40:56 +0200 |
nipkow |
renamed suffix(eq)
|
changeset |
files
|
| Wed, 25 May 2016 16:01:42 +0200 |
wenzelm |
updated 'define';
|
changeset |
files
|
| Wed, 25 May 2016 13:13:35 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 25 May 2016 11:50:58 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
changeset |
files
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
changeset |
files
|
| Wed, 25 May 2016 12:24:00 +0200 |
eberlm |
NEWS: Permutations of a set and randomised folds
|
changeset |
files
|
| Tue, 24 May 2016 22:46:23 +0200 |
Lars Hupel |
new Isabelle component for CI infastructure
|
changeset |
files
|
| Tue, 24 May 2016 19:42:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 24 May 2016 17:51:09 +0200 |
wenzelm |
recovered printing of DIM('a) (cf. 899c9c4e4a4c);
|
changeset |
files
|
| Tue, 24 May 2016 16:24:20 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 24 May 2016 16:13:59 +0200 |
wenzelm |
simplified syntax;
|
changeset |
files
|
| Tue, 24 May 2016 16:03:03 +0200 |
wenzelm |
clarified syntax category names according to Isabelle/ML/Scala;
|
changeset |
files
|
| Tue, 24 May 2016 15:53:16 +0200 |
wenzelm |
simplified syntax: Parse.term corresponds to Args.term etc.;
|
changeset |
files
|
| Tue, 24 May 2016 15:24:32 +0200 |
wenzelm |
clarified syntax categories;
|
changeset |
files
|
| Tue, 24 May 2016 15:16:57 +0200 |
wenzelm |
cartouche abbreviations work both for " as well;
|
changeset |
files
|
| Tue, 24 May 2016 18:48:01 +0200 |
eberlm |
Removed problematic code equation for set_permutations
|
changeset |
files
|
| Tue, 24 May 2016 18:46:51 +0200 |
eberlm |
Backed out changeset 8230358fab88
|
changeset |
files
|
| 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
|
| Mon, 09 May 2016 16:02:23 +0100 |
paulson |
renamings and refinements
|
changeset |
files
|
| Wed, 04 May 2016 10:19:01 +0200 |
hoelzl |
move Stirling numbers from AFP/Discrete_Summation
|
changeset |
files
|
| Sun, 01 May 2016 17:26:27 +0200 |
nipkow |
the standard While-rule
|
changeset |
files
|