2010-12-02 wenzelm 2010-12-02 proper theory name (cf. e84f82418e09);
2010-12-02 wenzelm 2010-12-02 merged;
2010-12-02 huffman 2010-12-02 merged
2010-12-01 huffman 2010-12-01 tuned cpodef code
2010-12-01 huffman 2010-12-01 reformulate lemma preorder.ex_ideal, and use it for typedefs
2010-12-02 hoelzl 2010-12-02 Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
2010-12-02 haftmann 2010-12-02 merged
2010-12-02 haftmann 2010-12-02 adapted expected value to more idiomatic numeral representation
2010-12-02 haftmann 2010-12-02 corrected representation for code_numeral numerals
2010-12-02 haftmann 2010-12-02 separate term_of function for integers -- more canonical representation of negative integers
2010-12-02 hoelzl 2010-12-02 merged
2010-12-02 hoelzl 2010-12-02 Use coercions in Approximation (by Dmitriy Traytel).
2010-12-02 wenzelm 2010-12-02 more antiquotations; removed some slightly outdated text;
2010-12-02 wenzelm 2010-12-02 configuration option "show_abbrevs" supersedes print mode "no_abbrevs", with inverted meaning;
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-12-02 wenzelm 2010-12-02 merged
2010-12-02 hoelzl 2010-12-02 merged
2010-12-02 hoelzl 2010-12-02 generalized simple_functionD
2010-12-02 hoelzl 2010-12-02 Moved theorems to appropriate place.
2010-12-02 hoelzl 2010-12-02 Shorter definition for positive_integral.
2010-12-02 hoelzl 2010-12-02 Move SUP_commute, SUP_less_iff to HOL image; Cleanup generic complete_lattice lemmas in Positive_Infinite_Real; Cleanup lemma positive_integral_alt;
2010-12-01 hoelzl 2010-12-01 Generalized simple_functionD and less_SUP_iff. Moved theorems to appropriate places.
2010-12-01 hoelzl 2010-12-01 Tuned setup for borel_measurable with min, max and psuminf.
2010-12-01 hoelzl 2010-12-01 Replace algebra_eqI by algebra.equality; Move sets_sigma_subset to Sigma_Algebra;
2010-12-02 blanchet 2010-12-02 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 wenzelm 2010-12-02 merged
2010-12-02 nipkow 2010-12-02 coercions
2010-12-01 nipkow 2010-12-01 merged
2010-12-01 nipkow 2010-12-01 moved activation of coercion inference into RealDef and declared function real a coercion. Made use of it in theory Ln.
2010-12-01 hoelzl 2010-12-01 Corrected IsaMakefile
2010-12-01 hoelzl 2010-12-01 merged
2010-12-01 hoelzl 2010-12-01 Updated NEWS
2010-12-01 hoelzl 2010-12-01 More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
2010-12-01 hoelzl 2010-12-01 Support product spaces on sigma finite measures. Introduce the almost everywhere quantifier. Introduce 'morphism' theorems for most constants. Prove uniqueness of measures on cut stable generators. Prove uniqueness of the Radon-Nikodym derivative. Removed misleading suffix from borel_space and lebesgue_space. Use product spaces to introduce Fubini on the Lebesgue integral. Combine Euclidean_Lebesgue and Lebesgue_Measure. Generalize theorems about mutual information and entropy to arbitrary probability spaces. Remove simproc mult_log as it does not work with interpretations. Introduce completion of measure spaces. Change type of sigma. Introduce dynkin systems.
2010-12-01 haftmann 2010-12-01 merged
2010-12-01 haftmann 2010-12-01 use type constructor as name for variable
2010-12-01 haftmann 2010-12-01 optional explicit prefix for type mapper theorems
2010-12-01 haftmann 2010-12-01 file for package tool type_mapper carries the same name as its Isar command
2010-12-01 huffman 2010-12-01 merged
2010-12-01 huffman 2010-12-01 domain package generates non-authentic syntax rules for parsing only
2010-12-02 wenzelm 2010-12-02 builtin time bounds (again);
2010-12-02 wenzelm 2010-12-02 tuned;
2010-12-01 wenzelm 2010-12-01 more abstract handling of Time properties;
2010-12-01 wenzelm 2010-12-01 store tooltip-dismiss-delay as Double(seconds);
2010-12-01 wenzelm 2010-12-01 more abstract/uniform handling of time, preferring seconds as Double;
2010-12-01 wenzelm 2010-12-01 merged
2010-12-01 haftmann 2010-12-01 NEWS
2010-12-01 wenzelm 2010-12-01 just one HOLogic.mk_comp;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-12-01 wenzelm 2010-12-01 tuned;
2010-12-01 wenzelm 2010-12-01 simplified HOL.eq simproc matching;
2010-12-01 wenzelm 2010-12-01 tuned;
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-12-01 wenzelm 2010-12-01 activate subtyping/coercions in theory Complex_Main;
2010-12-01 wenzelm 2010-12-01 simplified equality on pairs of types;
2010-12-01 wenzelm 2010-12-01 more precise dependencies;
2010-11-29 traytel 2010-11-29 two-staged architecture for subtyping; improved error messages of subtyping (using the new architecture); bugfix: constraint graph consistency check after cycle elimination;
2010-11-30 huffman 2010-11-30 merged
2010-11-30 huffman 2010-11-30 change cpodef-generated cont_Rep rules to cont2cont format
2010-11-30 huffman 2010-11-30 internal domain package proofs use cont2cont simproc instead of a fixed list of cont rules