Mon, 16 Jun 2014 21:26:50 +0200 wenzelm formal check of jEdit actions;
Mon, 16 Jun 2014 20:50:56 +0200 wenzelm more on "Completion";
Mon, 16 Jun 2014 14:04:48 +0200 wenzelm more on "Completion";
Mon, 16 Jun 2014 13:06:31 +0200 wenzelm tuned;
Mon, 16 Jun 2014 12:52:20 +0200 wenzelm clarified role of old user interfaces as misc tools;
Mon, 16 Jun 2014 12:41:51 +0200 wenzelm added Index;
Sat, 14 Jun 2014 12:38:14 +0200 wenzelm more on "Completion";
Fri, 13 Jun 2014 22:15:13 +0200 wenzelm more on "Completion";
Fri, 13 Jun 2014 21:58:12 +0200 wenzelm tuned;
Fri, 13 Jun 2014 20:01:39 +0200 wenzelm more on "Completion";
Thu, 12 Jun 2014 21:21:44 +0200 wenzelm more on "Completion";
Wed, 11 Jun 2014 22:28:24 +0200 wenzelm more on "Auxiliary files";
Wed, 11 Jun 2014 14:01:04 +0200 wenzelm more on "Document model";
Mon, 09 Jun 2014 20:44:13 +0200 wenzelm suppress index;
Mon, 09 Jun 2014 20:41:00 +0200 wenzelm more on command-line invocation -- moved material from system manual;
Mon, 09 Jun 2014 19:55:58 +0200 wenzelm clarified section structure;
Mon, 09 Jun 2014 19:43:54 +0200 wenzelm clarified section structure;
Mon, 09 Jun 2014 19:35:18 +0200 wenzelm clarified section structure;
Mon, 09 Jun 2014 12:15:53 +0200 wenzelm more on dockable windows;
Mon, 09 Jun 2014 11:05:43 +0200 wenzelm clarified section structure;
Fri, 06 Jun 2014 21:42:50 +0200 wenzelm tuned;
Fri, 06 Jun 2014 21:35:23 +0200 wenzelm more on Query panel;
Fri, 06 Jun 2014 12:10:33 +0200 wenzelm updated screenshots;
Thu, 05 Jun 2014 10:54:00 +0200 wenzelm more on Query panel -- updated Find Theorems;
Wed, 04 Jun 2014 18:18:09 +0200 wenzelm misc tuning and updates;
Wed, 25 Jun 2014 07:49:21 +0200 Andreas Lochbihler merged
Tue, 24 Jun 2014 15:05:58 +0200 Andreas Lochbihler add lemma
Tue, 24 Jun 2014 15:49:20 +0200 blanchet tuning
Tue, 24 Jun 2014 15:08:19 +0200 blanchet optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
Tue, 24 Jun 2014 14:56:08 +0200 blanchet minor table access optimization
Tue, 24 Jun 2014 13:48:14 +0200 desharna document property 'rel_coinduct'
Tue, 24 Jun 2014 13:48:14 +0200 desharna tune the implementation of 'rel_coinduct'
Tue, 24 Jun 2014 13:48:14 +0200 desharna generate 'rel_coinduct' theorem for codatatypes
Tue, 24 Jun 2014 13:48:14 +0200 desharna generate 'rel_coinduct0' theorem for codatatypes
Tue, 24 Jun 2014 12:36:45 +0200 blanchet added parentheses around type arguments in THF
Tue, 24 Jun 2014 12:36:45 +0200 blanchet optimize log
Tue, 24 Jun 2014 12:35:57 +0200 blanchet enable TF-IDF
Tue, 24 Jun 2014 12:35:49 +0200 blanchet added another experimental engine
Tue, 24 Jun 2014 12:35:43 +0200 blanchet tweaked experimental setup
Tue, 24 Jun 2014 08:20:00 +0200 blanchet changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
Tue, 24 Jun 2014 08:19:58 +0200 blanchet use strings to communicate with external process, to ease debugging
Tue, 24 Jun 2014 08:19:57 +0200 blanchet added 'dummy_thf_ml' prover for experiments with HOLyHammer
Tue, 24 Jun 2014 08:19:56 +0200 blanchet phantoms may also occur in THF1
Tue, 24 Jun 2014 08:19:55 +0200 blanchet added experimental MaSh engine
Tue, 24 Jun 2014 08:19:55 +0200 blanchet move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
Tue, 24 Jun 2014 08:19:54 +0200 blanchet help reconstruction of Z3 skolemization by weakening formulas a bit
Tue, 24 Jun 2014 08:19:22 +0200 blanchet supports gradual skolemization (cf. Z3) by threading context through correctly
Tue, 24 Jun 2014 08:19:22 +0200 blanchet given two one-liners, only show the best of the two
Tue, 24 Jun 2014 08:19:22 +0200 blanchet don't generate Isar proof skeleton for what amounts to a one-line proof
Tue, 24 Jun 2014 08:19:22 +0200 blanchet 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)
Sun, 22 Jun 2014 12:37:55 +0200 nipkow r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
Sat, 21 Jun 2014 15:46:52 +0200 nipkow added [simp]
Sat, 21 Jun 2014 10:41:02 +0200 ballarin Two basic lemmas on bij_betw.
Fri, 20 Jun 2014 09:55:31 +0200 blanchet changed default MaSh parameters based on (in vitro) evaluation
Fri, 20 Jun 2014 09:42:36 +0200 blanchet made 'tptp_graph' more liberal (why reject TFF?)
Wed, 18 Jun 2014 17:42:24 +0200 blanchet made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
Wed, 18 Jun 2014 17:42:24 +0200 blanchet more MaSh engine variations, for evaluations
Wed, 18 Jun 2014 17:42:24 +0200 blanchet split parameter into two
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip