2013-03-06 hoelzl 2013-03-06 add tendsto_eq_intros: they add an additional rewriting step at the rhs of --->
2013-03-06 nipkow 2013-03-06 major redesign: order instead of preorder, new definition of intervals as quotients
2013-03-06 nipkow 2013-03-06 added lemma
2013-03-06 nipkow 2013-03-06 extended numerals
2013-03-05 wenzelm 2013-03-05 merged
2013-03-05 wenzelm 2013-03-05 merged
2013-03-05 wenzelm 2013-03-05 removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-05 traytel 2013-03-05 extended stream library a little more
2013-03-05 traytel 2013-03-05 extended stream library
2013-03-05 hoelzl 2013-03-05 generalized lemmas in Extended_Real_Limits
2013-03-05 hoelzl 2013-03-05 eventually nhds represented using sequentially
2013-03-05 hoelzl 2013-03-05 generalized compact_Times to topological_space
2013-03-05 hoelzl 2013-03-05 move lemma Inf to usage point
2013-03-05 hoelzl 2013-03-05 tuned proof of Edelstein fixed point theorem (use continuity of dist and attains_sup)
2013-03-05 hoelzl 2013-03-05 tuned proofs (used continuity of infdist, dist and continuous_attains_sup)
2013-03-05 hoelzl 2013-03-05 generalized continuous/compact_attains_inf/sup from real to linorder_topology
2013-03-05 hoelzl 2013-03-05 continuity of pair operations
2013-03-05 hoelzl 2013-03-05 use generate_topology for second countable topologies, does not require intersection stable basis
2013-03-05 hoelzl 2013-03-05 generalized isGlb_unique
2013-03-05 hoelzl 2013-03-05 complete_linorder is also a complete_distrib_lattice
2013-03-05 hoelzl 2013-03-05 move Liminf / Limsup lemmas on complete_lattices to its own file
2013-03-05 nipkow 2013-03-05 merged
2013-03-05 nipkow 2013-03-05 New theory of infinity-extended types; should replace Extended_xyz eventually
2013-03-05 webertj 2013-03-05 Avoid ML warning about unreferenced identifier.
2013-03-05 blanchet 2013-03-05 polymorphic SPASS is also SPASS
2013-03-05 traytel 2013-03-05 allow more general coercion maps; tuned;
2013-03-05 nipkow 2013-03-05 more lemmas about intervals
2013-03-04 wenzelm 2013-03-04 merged
2013-03-04 wenzelm 2013-03-04 refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones; refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;
2013-03-04 wenzelm 2013-03-04 join all proofs before scheduling present phase (ordered according to weight); tuned;
2013-03-04 wenzelm 2013-03-04 more explicit datatype result;
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-03-04 traytel 2013-03-04 tuned (extend datatype to inline option)
2013-03-03 wenzelm 2013-03-03 prefer more systematic Future.flat;
2013-03-03 wenzelm 2013-03-03 more uniform Future.map: always internalize failure; added Future.flat as fast-path operation;
2013-03-03 wenzelm 2013-03-03 uniform treatment of global/local proofs; tuned;
2013-03-03 wenzelm 2013-03-03 tuned;
2013-03-03 wenzelm 2013-03-03 clarified Toplevel.element_result wrt. Toplevel.is_ignored;
2013-03-03 wenzelm 2013-03-03 more Thy_Syntax.element operations;
2013-03-01 traytel 2013-03-01 coercion-invariant arguments at work
2013-03-01 traytel 2013-03-01 constants with coercion-invariant arguments (possibility to disable/reenable coercions under certain constants, necessary for the forthcoming logically unspecified control structures for case translations)
2013-02-28 wenzelm 2013-02-28 simplified Proof.future_proof;
2013-02-28 wenzelm 2013-02-28 provide explicit dummy names (cf. dfe469293eb4);
2013-02-28 wenzelm 2013-02-28 discontinued empty name bindings in 'axiomatization';
2013-02-28 wenzelm 2013-02-28 provide common HOLogic.conj_conv and HOLogic.eq_conv;
2013-02-28 wenzelm 2013-02-28 just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
2013-02-28 wenzelm 2013-02-28 discontinued obsolete 'axioms' command;
2013-02-28 wenzelm 2013-02-28 more robust build error handling, e.g. missing outer syntax commands;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2013-02-28 wenzelm 2013-02-28 marginalized historic strip_tac;
2013-02-28 wenzelm 2013-02-28 tuned proof;
2013-02-28 wenzelm 2013-02-28 tuned whitespace and indentation;
2013-02-28 wenzelm 2013-02-28 simplified imports;