isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 tip

Merged
2016-05-24, by eberlm
Added set permutations/random permutations
2016-05-24, by eberlm
merged
2016-05-24, by wenzelm
embedded content may be delimited via cartouches;
2016-05-23, by wenzelm
tuned;
2016-05-23, by wenzelm
merged
2016-05-23, by nipkow
renamed prefix* in Library/Sublist
2016-05-23, by nipkow
generate Vampire 4.0 compatible output
2016-05-23, by blanchet
Merge
2016-05-23, by paulson
Lots of new material for multivariate analysis
2016-05-23, by paulson
removed odd cases rule (see also 8cb42cd97579);
2016-05-23, by wenzelm
tuned proofs;
2016-05-23, by wenzelm
tuned document;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
proper document source;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
merged
2016-05-21, by nipkow
added timing lemmas
2016-05-21, by nipkow
uniformly continuous function extended continuously on closure
2016-05-20, by immler
reduce isUCont to uniformly_continuous_on
2016-05-20, by immler
removed smt proof
2016-05-20, by immler
better handling of veriT's 'unknown' status
2016-05-20, by fleury
Resolved name clash
2016-05-18, by Manuel Eberl
Merged
2016-05-17, by eberlm
Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-17, by eberlm
Library: add partition_on
2016-05-17, by hoelzl
proper consideration of chained facts in 'try0' minimization
2016-05-17, by blanchet
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
2016-05-14, by wenzelm
tuned;
2016-05-14, by wenzelm
toplevel theorem statements support 'if'/'for' eigen-context;
2016-05-14, by wenzelm
reverted accidental commit;
2016-05-14, by wenzelm
eliminated use of empty "assms";
2016-05-13, by wenzelm
more complete theories;
2016-05-13, by wenzelm
common entity definitions within a global or local theory context;
2016-05-12, by wenzelm
clarified heading
2016-05-12, by haftmann
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2016-05-12, by haftmann
merged
2016-05-12, by wenzelm
avoid spurious fact index, notably in "context begin" (via Bundle.context);
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
expose Sessions.Info in Build.Results
2016-05-12, by Lars Hupel
introduced class topological_group between topological_monoid and real_normed_vector
2016-05-11, by immler
find dynamic facts as well, but static ones are preferred;
2016-05-10, by wenzelm
some slight generalizations
2016-05-10, by immler
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
2016-05-10, by paulson
two new lemmas about segments
2016-05-10, by paulson
Merge
2016-05-09, by paulson
lemmas about dimension, hyperplanes, span, etc.
2016-05-09, by paulson
merged
2016-05-09, by wenzelm
clarified context, notably for internal use of Simplifier;
2016-05-09, by wenzelm
renamings and refinements
2016-05-09, by paulson
move Stirling numbers from AFP/Discrete_Summation
2016-05-04, by hoelzl
the standard While-rule
2016-05-01, by nipkow
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
2016-04-29, by wenzelm
unfold is subject to unfold_abs_def (still inactive);
2016-04-28, by wenzelm
tuned;
2016-04-28, by wenzelm
NEWS;
2016-04-28, by wenzelm
clarified order: params/prems/concl interchangeable with !!/==> proposition;
2016-04-28, by wenzelm
support 'assumes' in specifications, e.g. 'definition', 'inductive';
2016-04-28, by wenzelm
tuned;
2016-04-27, by wenzelm
merged
2016-04-26, by wenzelm
updated subtle side-conditions;
2016-04-26, by wenzelm
some uses of 'obtain' with structure statement;
2016-04-26, by wenzelm
'obtain' supports structured statements (similar to 'define');
2016-04-26, by wenzelm
more portable: GNU find no longer supports "-perm +mode";
2016-04-26, by wenzelm
more uniform operations for structured statements;
2016-04-26, by wenzelm
defs are closed, which leads to proper auto_bind_facts;
2016-04-26, by wenzelm
tuned notation;
2016-04-26, by wenzelm
misc tuning and modernization;
2016-04-26, by wenzelm
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: alternative representation of linear combination
2016-04-22, by hoelzl
Linear_Algebra: move abstract concepts to front
2016-04-22, by hoelzl
merge
2016-04-25, by blanchet
avoid duplicate mixfix messages in '(co)datatype' type name
2016-04-25, by blanchet
generalize code to avoid making assumptions about type variable names
2016-04-25, by blanchet
intermediate definitions and caching in n2m to keep terms small
2016-04-15, by traytel
n2m operates on (un)folds
2016-04-14, by traytel
clarified rendering;
2016-04-25, by wenzelm
old 'def' is legacy;
2016-04-25, by wenzelm
more rigid check of lhs;
2016-04-25, by wenzelm
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-04-25, by wenzelm
eliminated old 'def';
2016-04-25, by wenzelm
added Isar command 'define';
2016-04-24, by wenzelm
within a proof body context, undeclared frees are like global constants;
2016-04-24, by wenzelm
clarified modules;
2016-04-24, by wenzelm
added "balanced" predicate
2016-04-22, by nipkow
fixed code equation for pdivmod, added improved code equation for pseudo_mod
2016-04-20, by Rene Thiemann
proper latex;
2016-04-20, by wenzelm
merged
2016-04-20, by wenzelm
reactivated other_id reports (see also db929027e701, 8eda56033203);
2016-04-20, by wenzelm
invisible context similar to interpretation;
2016-04-20, by wenzelm
avoid massive multiplication of reports due to interpretation;
2016-04-20, by wenzelm
tuned comments;
2016-04-19, by wenzelm
more thorough update;
2016-04-19, by wenzelm
several updates on polynomial long division and pseudo division
2016-04-15, by Rene Thiemann
fragment of a HOL type class primer
2016-04-18, by haftmann
capitalized GCD and LCM syntax
2016-04-18, by haftmann
environment variable check has become pointless after 771b8ad5c7fc
2016-04-18, by haftmann
unfold internal definitions before emitting a proof obligation
2016-04-19, by traytel
more IDE support for Isabelle/Pure bootstrap;
2016-04-19, by wenzelm
merged
2016-04-18, by wenzelm
tuned signature;
2016-04-18, by wenzelm
prefer internal attribute source;
2016-04-18, by wenzelm
tidying some proofs; getting rid of "nonempty_witness"
2016-04-18, by paulson
Merge
2016-04-18, by paulson
numerous theorems about affine hulls, hyperplanes, etc.
2016-04-18, by paulson
merged
2016-04-18, by wenzelm
proper LaTeX;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
avoid clash with function called "x";
2016-04-18, by wenzelm
new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-18, by paulson
clarified bindings;
2016-04-17, by wenzelm
clarified bindings;
2016-04-17, by wenzelm
prefer binding over base name;
2016-04-17, by wenzelm