isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

Added material by David Trachtenherz
2011-02-26, by nipkow
corrected HOLCF dependency on Nat_Infinity
2011-02-26, by nipkow
got rid of lemma upper_bound_finite_set
2011-02-25, by nipkow
merged
2011-02-25, by nipkow
Some cleaning up
2011-02-25, by nipkow
updated generated files
2011-02-25, by krauss
fixed manual (rule no longer exists)
2011-02-25, by krauss
removed support for tail-recursion from function package (now implemented by partial_function)
2011-02-25, by krauss
reactivate time measurement (partly reverting c27b0b37041a);
2011-02-25, by krauss
generalize find_theorems filters to work on raw propositions, too
2011-02-25, by krauss
merged
2011-02-25, by nipkow
added simp lemma nth_Cons_pos to List
2011-02-25, by nipkow
Refactor find_theorems to provide a more general filter_facts method
2011-02-25, by noschinl
removed dead code/unused exports/speculative generality
2011-02-25, by krauss
recdef -> fun(ction)
2011-02-24, by krauss
removed unused lemma
2011-02-24, by krauss
recdef -> fun(ction);
2011-02-24, by krauss
eliminated clones of List.upto
2011-02-24, by krauss
fix non-exhaustive pattern match in find_theorems
2011-02-23, by noschinl
merged
2011-02-23, by hoelzl
add lemma KL_divergence_vimage, mutual_information_generic
2011-02-23, by hoelzl
add lemma RN_deriv_vimage
2011-02-23, by hoelzl
use measure_preserving in ..._vimage lemmas
2011-02-23, by hoelzl
log is borel measurable
2011-02-23, by hoelzl
add name continuous_isCont to unnamed lemma
2011-02-22, by hoelzl
add example for case_product usage
2011-02-23, by noschinl
setup case_product attribute in HOL and FOL
2011-02-23, by noschinl
introduce attribute case_prod for combining case rules
2010-12-08, by noschinl
merged
2011-02-23, by blanchet
remove confusing message
2011-02-23, by blanchet
eliminated remdps in favor of List.remdups
2011-02-23, by krauss
recdef -> fun
2011-02-23, by krauss
recdef -> fun
2011-02-23, by krauss
updated generated file;
2011-02-22, by wenzelm
scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
2011-02-22, by wenzelm
modernized specifications;
2011-02-22, by wenzelm
dropped obsolete FIXMEs
2011-02-22, by krauss
merged, resolving spurious conflicts and giving up Reflected_Multivariate_Polynomial.thy from ab5d2d81f9fb;
2011-02-21, by wenzelm
eliminated global prems
2011-02-21, by krauss
modernized specification; curried
2011-02-21, by krauss
recdef -> fun; curried
2011-02-21, by krauss
recdef -> fun; curried
2011-02-21, by krauss
strengthened polymul.induct
2011-02-21, by krauss
dropped stupid name
2011-02-21, by krauss
removed duplicate declarations
2011-02-21, by krauss
recdef -> function
2011-02-21, by krauss
tuned proofs -- eliminated prems;
2011-02-21, by wenzelm
merged
2011-02-21, by blanchet
adjust example
2011-02-21, by blanchet
document new "preconstr" option
2011-02-21, by blanchet
more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21, by blanchet
more work on "fix_datatype_vals"
2011-02-21, by blanchet
first steps in implementing "fix_datatype_vals" optimization
2011-02-21, by blanchet
better fudge factors for CVC3 and Yices based on Judgment Day
2011-02-21, by blanchet
exit code 127 can mean many things -- not just (and probably not) Perl missing
2011-02-21, by blanchet
modernized specifications;
2011-02-21, by wenzelm
rename Nitpick's (internal) auxiliary lemmas
2011-02-21, by blanchet
updated docs w.r.t. "nitpick_unfold" attribute
2011-02-21, by blanchet
improve optimization
2011-02-21, by blanchet
updated docs
2011-02-21, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle