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
Mon, 16 Jun 2014 19:39:41 +0200 blanchet give Z3 TPTP proofs a chance
Mon, 16 Jun 2014 19:18:10 +0200 blanchet fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
Mon, 16 Jun 2014 17:52:33 +0200 hoelzl add more derivative and continuity rules for complex-values functions
Mon, 16 Jun 2014 16:21:52 +0200 fleury Moving the remote prefix deleting on Sledgehammer's side
Mon, 16 Jun 2014 16:21:39 +0200 fleury Correcting the type parser
Mon, 16 Jun 2014 16:18:34 +0200 fleury imported patch leo2_skolem_simplication
Mon, 16 Jun 2014 16:18:15 +0200 fleury add support for Isar reconstruction for thf1 ATP provers like Leo-II.
Mon, 16 Jun 2014 13:19:48 +0200 hoelzl lemmas about the moments of the normal distribution
Fri, 13 Jun 2014 14:49:59 +0100 paulson NEWS
Fri, 13 Jun 2014 14:08:20 +0200 hoelzl properties of normal distributed random variables (by Sudeep Kanav)
Fri, 13 Jun 2014 07:05:01 +0200 nipkow announce Tree
Thu, 12 Jun 2014 21:23:28 +0200 nipkow new theory of binary trees
Thu, 12 Jun 2014 18:02:39 +0200 haftmann formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
Thu, 12 Jun 2014 18:47:27 +0200 nipkow merged
Thu, 12 Jun 2014 18:47:16 +0200 nipkow added [simp]
Thu, 12 Jun 2014 17:50:49 +0200 blanchet tuning
Thu, 12 Jun 2014 17:10:12 +0200 blanchet renamed Sledgehammer options
Thu, 12 Jun 2014 17:02:03 +0200 blanchet removed dead code
Thu, 12 Jun 2014 17:02:03 +0200 blanchet reintroduced vital 'Thm.transfer'
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuned dependencies
Thu, 12 Jun 2014 17:02:03 +0200 blanchet updated docs
Thu, 12 Jun 2014 17:02:03 +0200 blanchet added support for CVC4 in SMT2
Thu, 12 Jun 2014 17:02:03 +0200 blanchet don't ask proof-disabled solvers to do proofs
Thu, 12 Jun 2014 17:02:03 +0200 blanchet tuning
Thu, 12 Jun 2014 17:02:03 +0200 blanchet took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
Thu, 12 Jun 2014 17:02:02 +0200 blanchet made CVC3 work with SMT2 stack
Thu, 12 Jun 2014 15:47:36 +0200 hoelzl properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip