2011-09-03 ago haftmann assert Pure equations for theorem references; tuned
2011-09-03 ago haftmann tuned specifications and proofs
2011-09-03 ago wenzelm merged
2011-09-03 ago huffman remove duplicate lemma finite_choice in favor of finite_set_choice
2011-09-03 ago huffman simplify proof
2011-09-03 ago huffman shorten some proofs
2011-09-02 ago huffman remove redundant simp rules ceiling_floor and floor_ceiling
2011-09-03 ago wenzelm misc tuning and simplification of proofs;
2011-09-03 ago wenzelm Document.removed_versions on Scala side;
2011-09-03 ago wenzelm discontinued predefined empty command (obsolete!?);
2011-09-03 ago wenzelm discontinued global execs: store exec value directly within entries;
2011-09-03 ago wenzelm Document.remove_versions on ML side;
2011-09-03 ago wenzelm some support to prune_history;
2011-09-02 ago huffman merged
2011-09-02 ago huffman speed up extremely slow metis proof of Sup_real_iff
2011-09-02 ago huffman remove redundant lemma reals_complete2 in favor of complete_real
2011-09-02 ago huffman simplify proof of Rats_dense_in_real;
2011-09-02 ago huffman remove unused, unnecessary lemmas
2011-09-02 ago huffman remove more duplicate lemmas
2011-09-02 ago wenzelm merged
2011-09-02 ago haftmann merged
2011-09-02 ago haftmann avoid "Code" as structure name
2011-09-02 ago wenzelm more robust chunk painting wrt. hard tabs, when chunk.str == null;
2011-09-02 ago wenzelm raw message function "assign_execs" avoids full overhead of decoding and caching message body;
2011-09-02 ago wenzelm less agressive parsing of commands (priority ~1);
2011-09-02 ago wenzelm tuned;
2011-09-02 ago wenzelm more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
2011-09-02 ago nipkow merged
2011-09-02 ago nipkow Added Abstract Interpretation theories
2011-09-02 ago wenzelm tuned proofs;
2011-09-02 ago wenzelm proper config option linarith_trace;
2011-09-02 ago wenzelm discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
2011-09-02 ago wenzelm merged
2011-09-02 ago blanchet renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
2011-09-02 ago blanchet use new syntax for Pi binder in TFF1 output
2011-09-02 ago blanchet fewer TPTP important messages
2011-09-01 ago huffman simplify some proofs about uniform continuity, and add some new ones;
2011-09-01 ago huffman modernize lemmas about 'continuous' and 'continuous_on';
2011-09-01 ago huffman add lemma tendsto_infnorm
2011-09-02 ago wenzelm more precise iterate_entries_after if start refers to last entry;
2011-09-02 ago wenzelm clarified define_command: store name as structural information;
2011-09-01 ago wenzelm amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
2011-09-01 ago wenzelm more redable Document.Node.toString;
2011-09-01 ago wenzelm sort wrt. theory name;
2011-09-01 ago wenzelm modernized theory name;
2011-09-01 ago wenzelm repaired benchmarks;
2011-09-01 ago wenzelm merged
2011-09-01 ago blanchet tuning
2011-09-01 ago blanchet always measure time for ATPs -- auto minimization relies on it
2011-09-01 ago blanchet added two lemmas about "distinct" to help Sledgehammer
2011-09-01 ago blanchet make "sound" sound and "unsound" more sound, based on evaluation
2011-09-01 ago Cezary Kaliszyk HOL/Import: observe distinction between sets and predicates (where possible)
2011-08-31 ago huffman simplify/generalize some proofs
2011-08-31 ago huffman generalize lemma isCont_vec_nth
2011-08-31 ago huffman convert proof to Isar-style
2011-08-31 ago huffman remove redundant lemma card_enum
2011-08-31 ago huffman move lemmas from Topology_Euclidean_Space to Euclidean_Space
2011-08-31 ago huffman convert to Isar-style proof
2011-08-31 ago blanchet make SML/NJ happy
2011-08-31 ago blanchet more tuning