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
Wed, 18 Jun 2014 15:23:40 +0200 blanchet more generous formula -- there are lots of duplicates out there
Wed, 18 Jun 2014 14:19:42 +0200 blanchet automatically learn MaSh facts also in 'blocking' mode
Wed, 18 Jun 2014 13:23:09 +0200 blanchet enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
Tue, 17 Jun 2014 18:41:44 +0200 ballarin Lemmas contributed by Joachim Breitner.
Tue, 17 Jun 2014 18:33:34 +0200 blanchet reintroduce atomize in Waldmeister code
Tue, 17 Jun 2014 16:02:49 +0200 blanchet changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
Mon, 16 Jun 2014 19:44:02 +0200 blanchet compile
Mon, 16 Jun 2014 19:42:44 +0200 blanchet integrated new Waldmeister code with 'sledgehammer' command
Mon, 16 Jun 2014 19:41:42 +0200 blanchet fixed parsing of one-argument 'file()' in TSTP files
Mon, 16 Jun 2014 19:41:01 +0200 blanchet use right delimiters for Waldmeister proofs
Mon, 16 Jun 2014 19:41:00 +0200 blanchet added 'waldmeister_new' as ATP
Mon, 16 Jun 2014 19:40:59 +0200 blanchet simplified code
Mon, 16 Jun 2014 19:40:04 +0200 blanchet moved code around
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip