| 2015-02-14 |
haftmann |
dropped redundancy
|
changeset |
files
|
| 2015-02-14 |
haftmann |
less warnings
|
changeset |
files
|
| 2015-02-13 |
wenzelm |
merged
|
changeset |
files
|
| 2015-02-11 |
wenzelm |
proper context;
|
changeset |
files
|
| 2015-02-11 |
wenzelm |
proper context;
|
changeset |
files
|
| 2015-02-11 |
wenzelm |
proper context;
|
changeset |
files
|
| 2015-02-11 |
wenzelm |
proper context;
|
changeset |
files
|
| 2015-02-11 |
wenzelm |
proper context and method setup;
|
changeset |
files
|
| 2015-02-12 |
paulson |
new lemmas re refinement of one equivalence relation WRT another
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
rel_pmf preserves orders
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
generalise lemma
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
more lemmas
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
merged
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
more transfer rules
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add lemmas about functions on option
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
tuned proof
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add lema about card and vimage
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add more general version of finite_vimageD
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add lemma
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add lemmas about flat_ord
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add parametricity rules for monotone, fun_lub, and fun_ord
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add parametricity rule for Ex1
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add intro and elim rules for right_total
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add monotonicity lemmas for rel_fun
|
changeset |
files
|
| 2015-02-11 |
Andreas Lochbihler |
add lemmas about bind and image
|
changeset |
files
|
| 2015-02-11 |
blanchet |
updated NEWS
|
changeset |
files
|
| 2015-02-11 |
blanchet |
updated Sledgehammer docs
|
changeset |
files
|
| 2015-02-11 |
blanchet |
added CVC4 component (and took out CVC3 from main components)
|
changeset |
files
|
| 2015-02-11 |
blanchet |
tuned default provers
|
changeset |
files
|
| 2015-02-11 |
paulson |
Merge
|
changeset |
files
|
| 2015-02-10 |
paulson |
Not a simprule, as it complicates proofs
|
changeset |
files
|
| 2015-02-10 |
paulson |
Merge
|
changeset |
files
|
| 2015-02-10 |
paulson |
New lemmas and a bit of tidying up.
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
check unused theory;
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
tuned;
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
more accurate context;
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
merged
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
misc tuning;
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
changeset |
files
|
| 2015-02-10 |
wenzelm |
indicate slow proof (approx. 20s);
|
changeset |
files
|
| 2015-02-10 |
hoelzl |
merged
|
changeset |
files
|
| 2015-02-10 |
hoelzl |
add bind_cond_pmf_cancel
|
changeset |
files
|
| 2015-02-10 |
hoelzl |
add cond_map_pmf
|
changeset |
files
|
| 2015-02-10 |
hoelzl |
introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
|
changeset |
files
|
| 2015-02-10 |
Andreas Lochbihler |
tuned proof
|
changeset |
files
|
| 2015-02-10 |
Andreas Lochbihler |
add another lemma to split nn_integral over product count_space
|
changeset |
files
|
| 2015-02-10 |
Andreas Lochbihler |
tune proof
|
changeset |
files
|
| 2015-02-10 |
Andreas Lochbihler |
nn_integral can be split over arbitrary product count_spaces
|
changeset |
files
|
| 2015-02-10 |
Andreas Lochbihler |
add stronger version of lemma
|
changeset |
files
|
| 2015-02-06 |
haftmann |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
changeset |
files
|
| 2015-02-06 |
blanchet |
careful about visibility of facts that have the same 'theory' in optimization
|
changeset |
files
|
| 2015-02-06 |
haftmann |
non-intrusive default code setup for mappings
|
changeset |
files
|
| 2015-02-05 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
changeset |
files
|
| 2015-02-05 |
haftmann |
explicit type annotation avoids problems with Haskell type inference
|
changeset |
files
|
| 2015-02-05 |
haftmann |
more explicit hint on import order
|
changeset |
files
|
| 2015-02-05 |
haftmann |
dropped dead code;
|
changeset |
files
|
| 2015-02-05 |
haftmann |
dropped obsolete external entrance point
|
changeset |
files
|
| 2015-02-05 |
haftmann |
explicit error message for non-existing targets
|
changeset |
files
|
| 2015-02-02 |
blanchet |
fixed typos
|
changeset |
files
|
| 2015-02-02 |
blanchet |
less confusing constant
|
changeset |
files
|