2014-02-24 paulson 2014-02-24 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
2014-02-24 paulson 2014-02-24 A few lemmas about summations, etc.
2014-02-02 paulson 2014-02-02 Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
2014-01-25 wenzelm 2014-01-25 explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
2014-01-20 blanchet 2014-01-20 moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
2014-01-20 blanchet 2014-01-20 moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
2013-11-28 blanchet 2013-11-28 cleaned up indirect dependency
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-27 hoelzl 2013-08-27 renamed inner_dense_linorder to dense_linorder
2013-07-25 haftmann 2013-07-25 factored syntactic type classes for bot and top (by Alessandro Coglio)
2013-06-15 haftmann 2013-06-15 lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
2013-03-05 nipkow 2013-03-05 more lemmas about intervals
2013-02-20 hoelzl 2013-02-20 split dense into inner_dense_order and no_top/no_bot
2013-02-20 hoelzl 2013-02-20 move auxiliary lemmas from Library/Extended_Reals to HOL image
2013-02-15 Andreas Lochbihler 2013-02-15 added lemma
2013-01-31 hoelzl 2013-01-31 introduce order topology
2012-12-07 hoelzl 2012-12-07 add Int_atMost
2012-05-24 wenzelm 2012-05-24 tuned proofs;
2012-04-03 huffman 2012-04-03 modernized obsolete old-style theory name with proper new-style underscore