2014-06-18 wenzelm 2014-06-18 added screenshot;
2014-06-18 wenzelm 2014-06-18 tuned;
2014-06-18 wenzelm 2014-06-18 misc tuning;
2014-06-17 wenzelm 2014-06-17 added screenshot;
2014-06-17 wenzelm 2014-06-17 misc tuning;
2014-06-16 wenzelm 2014-06-16 formal check of jEdit actions;
2014-06-16 wenzelm 2014-06-16 more on "Completion";
2014-06-16 wenzelm 2014-06-16 more on "Completion";
2014-06-16 wenzelm 2014-06-16 tuned;
2014-06-16 wenzelm 2014-06-16 clarified role of old user interfaces as misc tools;
2014-06-16 wenzelm 2014-06-16 added Index;
2014-06-14 wenzelm 2014-06-14 more on "Completion";
2014-06-13 wenzelm 2014-06-13 more on "Completion";
2014-06-13 wenzelm 2014-06-13 tuned;
2014-06-13 wenzelm 2014-06-13 more on "Completion";
2014-06-12 wenzelm 2014-06-12 more on "Completion";
2014-06-11 wenzelm 2014-06-11 more on "Auxiliary files";
2014-06-11 wenzelm 2014-06-11 more on "Document model";
2014-06-09 wenzelm 2014-06-09 suppress index;
2014-06-09 wenzelm 2014-06-09 more on command-line invocation -- moved material from system manual;
2014-06-09 wenzelm 2014-06-09 clarified section structure;
2014-06-09 wenzelm 2014-06-09 clarified section structure;
2014-06-09 wenzelm 2014-06-09 clarified section structure;
2014-06-09 wenzelm 2014-06-09 more on dockable windows;
2014-06-09 wenzelm 2014-06-09 clarified section structure;
2014-06-06 wenzelm 2014-06-06 tuned;
2014-06-06 wenzelm 2014-06-06 more on Query panel;
2014-06-06 wenzelm 2014-06-06 updated screenshots;
2014-06-05 wenzelm 2014-06-05 more on Query panel -- updated Find Theorems;
2014-06-04 wenzelm 2014-06-04 misc tuning and updates;
2014-06-25 Andreas Lochbihler 2014-06-25 merged
2014-06-24 Andreas Lochbihler 2014-06-24 add lemma
2014-06-24 blanchet 2014-06-24 tuning
2014-06-24 blanchet 2014-06-24 optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
2014-06-24 blanchet 2014-06-24 minor table access optimization
2014-06-24 desharna 2014-06-24 document property 'rel_coinduct'
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct' theorem for codatatypes
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct0' theorem for codatatypes
2014-06-24 blanchet 2014-06-24 added parentheses around type arguments in THF
2014-06-24 blanchet 2014-06-24 optimize log
2014-06-24 blanchet 2014-06-24 enable TF-IDF
2014-06-24 blanchet 2014-06-24 added another experimental engine
2014-06-24 blanchet 2014-06-24 tweaked experimental setup
2014-06-24 blanchet 2014-06-24 changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
2014-06-24 blanchet 2014-06-24 use strings to communicate with external process, to ease debugging
2014-06-24 blanchet 2014-06-24 added 'dummy_thf_ml' prover for experiments with HOLyHammer
2014-06-24 blanchet 2014-06-24 phantoms may also occur in THF1
2014-06-24 blanchet 2014-06-24 added experimental MaSh engine
2014-06-24 blanchet 2014-06-24 move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
2014-06-24 blanchet 2014-06-24 help reconstruction of Z3 skolemization by weakening formulas a bit
2014-06-24 blanchet 2014-06-24 supports gradual skolemization (cf. Z3) by threading context through correctly
2014-06-24 blanchet 2014-06-24 given two one-liners, only show the best of the two
2014-06-24 blanchet 2014-06-24 don't generate Isar proof skeleton for what amounts to a one-line proof
2014-06-24 blanchet 2014-06-24 don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
2014-06-22 nipkow 2014-06-22 r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
2014-06-21 nipkow 2014-06-21 added [simp]
2014-06-21 ballarin 2014-06-21 Two basic lemmas on bij_betw.
2014-06-20 blanchet 2014-06-20 changed default MaSh parameters based on (in vitro) evaluation
2014-06-20 blanchet 2014-06-20 made 'tptp_graph' more liberal (why reject TFF?)