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