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

bash wrapper: terminate only in exceptional case, keep background processes running (e.g. 'thy_deps' or 'display_drafts');
2010-12-03, by wenzelm
updated latex dependencies (cf. 7d88ebdce380);
2010-12-03, by wenzelm
tuned README;
2010-12-03, by wenzelm
isabellesym.sty: eliminated dependency on latin1, to allow documents using utf8 instead;
2010-12-02, by wenzelm
proper theory name (cf. e84f82418e09);
2010-12-02, by wenzelm
merged;
2010-12-02, by wenzelm
merged
2010-12-02, by huffman
tuned cpodef code
2010-12-01, by huffman
reformulate lemma preorder.ex_ideal, and use it for typedefs
2010-12-01, by huffman
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
2010-12-02, by hoelzl
merged
2010-12-02, by haftmann
adapted expected value to more idiomatic numeral representation
2010-12-02, by haftmann
corrected representation for code_numeral numerals
2010-12-02, by haftmann
separate term_of function for integers -- more canonical representation of negative integers
2010-12-02, by haftmann
merged
2010-12-02, by hoelzl
Use coercions in Approximation (by Dmitriy Traytel).
2010-12-02, by hoelzl
more antiquotations;
2010-12-02, by wenzelm
configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02, by wenzelm
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-12-02, by wenzelm
merged
2010-12-02, by wenzelm
merged
2010-12-02, by hoelzl
generalized simple_functionD
2010-12-02, by hoelzl
Moved theorems to appropriate place.
2010-12-02, by hoelzl
Shorter definition for positive_integral.
2010-12-02, by hoelzl
Move SUP_commute, SUP_less_iff to HOL image;
2010-12-02, by hoelzl
Generalized simple_functionD and less_SUP_iff.
2010-12-01, by hoelzl
Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01, by hoelzl
Replace algebra_eqI by algebra.equality;
2010-12-01, by hoelzl
give the Isabelle proof the benefice of the doubt when the Isabelle theorem has fewer literals than the Metis one -- this makes a difference on lemma "Let (x::'a, y::'a) (inv_image (r::'b * 'b => bool) (f::'a => 'b)) = ((f x, f y) : r)" apply (metis in_inv_image mem_def)
2010-12-02, by blanchet
merged
2010-12-02, by wenzelm
coercions
2010-12-02, by nipkow
merged
2010-12-01, by nipkow
moved activation of coercion inference into RealDef and declared function real a coercion.
2010-12-01, by nipkow
Corrected IsaMakefile
2010-12-01, by hoelzl
merged
2010-12-01, by hoelzl
Updated NEWS
2010-12-01, by hoelzl
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01, by hoelzl
Support product spaces on sigma finite measures.
2010-12-01, by hoelzl
merged
2010-12-01, by haftmann
use type constructor as name for variable
2010-12-01, by haftmann
optional explicit prefix for type mapper theorems
2010-12-01, by haftmann
file for package tool type_mapper carries the same name as its Isar command
2010-12-01, by haftmann
merged
2010-12-01, by huffman
domain package generates non-authentic syntax rules for parsing only
2010-12-01, by huffman
builtin time bounds (again);
2010-12-02, by wenzelm
tuned;
2010-12-02, by wenzelm
more abstract handling of Time properties;
2010-12-01, by wenzelm
store tooltip-dismiss-delay as Double(seconds);
2010-12-01, by wenzelm
more abstract/uniform handling of time, preferring seconds as Double;
2010-12-01, by wenzelm
merged
2010-12-01, by wenzelm
NEWS
2010-12-01, by haftmann
just one HOLogic.mk_comp;
2010-12-01, by wenzelm
more direct use of binder_types/body_type;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
simplified HOL.eq simproc matching;
2010-12-01, by wenzelm
tuned;
2010-12-01, by wenzelm
just one Term.dest_funT;
2010-12-01, by wenzelm
activate subtyping/coercions in theory Complex_Main;
2010-12-01, by wenzelm
simplified equality on pairs of types;
2010-12-01, by wenzelm
more precise dependencies;
2010-12-01, by wenzelm

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

isabelle