Fri, 01 Aug 2014 16:07:34 +0200 blanchet beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
Fri, 01 Aug 2014 16:07:33 +0200 blanchet tuning
Fri, 01 Aug 2014 16:07:33 +0200 blanchet peek instead of joining -- is perhaps less risky
Fri, 01 Aug 2014 14:43:57 +0200 blanchet export ML function
Fri, 01 Aug 2014 14:43:57 +0200 blanchet compile
Fri, 01 Aug 2014 14:43:57 +0200 blanchet removed 'metisFT' support in Mirabelle
Fri, 01 Aug 2014 14:43:57 +0200 blanchet removed Mirabelle minimization code
Fri, 01 Aug 2014 14:43:57 +0200 blanchet modernized Mirabelle (a bit) and made it compile
Fri, 01 Aug 2014 14:43:57 +0200 blanchet restored a bit of laziness
Fri, 01 Aug 2014 14:43:57 +0200 blanchet reorder quantifiers to ease Z3 skolemization
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuned order of arguments
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuned name context code
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuned whitespace
Fri, 01 Aug 2014 14:43:57 +0200 blanchet more rational unskolemizing of names
Fri, 01 Aug 2014 14:43:57 +0200 blanchet added appropriate method for skolemization of Z3 steps to the mix
Fri, 01 Aug 2014 14:43:57 +0200 blanchet pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
Fri, 01 Aug 2014 14:43:57 +0200 blanchet honor 'try0' also for one-liners
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
Fri, 01 Aug 2014 14:43:57 +0200 blanchet further minimize one-liner
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated needlessly complex message tail
Fri, 01 Aug 2014 14:43:57 +0200 blanchet updated NEWS
Fri, 01 Aug 2014 14:43:57 +0200 blanchet update documentation after removal of 'min' subcommand
Fri, 01 Aug 2014 14:43:57 +0200 blanchet eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
Fri, 01 Aug 2014 14:43:57 +0200 blanchet rationalized preplaying by eliminating (now superfluous) laziness
Fri, 01 Aug 2014 14:43:57 +0200 blanchet removed proof methods as provers from docs
Fri, 01 Aug 2014 14:43:57 +0200 blanchet simplified minimization logic
Fri, 01 Aug 2014 14:43:57 +0200 blanchet tuning
Fri, 01 Aug 2014 14:43:57 +0200 blanchet remove lambda-lifting related assumptions from generated Isar proofs
Fri, 01 Aug 2014 14:43:57 +0200 blanchet whitespace tuning
Fri, 01 Aug 2014 14:43:57 +0200 blanchet remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
Fri, 01 Aug 2014 14:43:57 +0200 blanchet generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
Thu, 31 Jul 2014 13:19:57 +0200 traytel simplified tactics slightly
Thu, 31 Jul 2014 00:45:55 +0200 blanchet cascading timeout in parallel evaluation, to rapidly find optimum
Wed, 30 Jul 2014 23:52:56 +0200 blanchet put faster proof methods first
Wed, 30 Jul 2014 23:52:56 +0200 blanchet use parallel preplay machinery also for one-line proofs
Wed, 30 Jul 2014 23:52:56 +0200 blanchet updated docs
Wed, 30 Jul 2014 23:52:56 +0200 blanchet always minimize Sledgehammer results by default
Wed, 30 Jul 2014 23:52:56 +0200 blanchet tuned ML function name
Wed, 30 Jul 2014 23:52:56 +0200 blanchet reduced preplay timeout to 1 s
Wed, 30 Jul 2014 23:52:56 +0200 blanchet added more proof methods for one-liners
Wed, 30 Jul 2014 23:52:56 +0200 blanchet unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
Wed, 30 Jul 2014 14:03:58 +0200 fleury Improving robustness and indentation corrections.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Skolemization for tmp_ite_elim rule in the SMT solver veriT.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Whitespace and indentation correction.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Simplifying the labels in the proof of the SMT solver veriT.
Wed, 30 Jul 2014 14:03:13 +0200 fleury Changing ~ into - for unuary minus (not supported by veriT)
Wed, 30 Jul 2014 14:03:13 +0200 fleury imported patch satallax_skolemization_in_tree_part
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch hilbert_choice_support
Wed, 30 Jul 2014 14:03:12 +0200 fleury veriT changes for lifted terms, and ite_elim rules.
Wed, 30 Jul 2014 14:03:12 +0200 fleury imported patch satallax_proof_support_Sledgehammer
Wed, 30 Jul 2014 14:03:12 +0200 fleury Basic support for the higher-order ATP Satallax.
Wed, 30 Jul 2014 14:03:12 +0200 fleury Subproofs for the SMT solver veriT.
Wed, 30 Jul 2014 14:03:12 +0200 fleury Basic support for the SMT prover veriT.
Wed, 30 Jul 2014 14:03:11 +0200 fleury removing the '= True' generated by Leo-II.
Wed, 30 Jul 2014 14:03:11 +0200 fleury Skolemization support for leo-II and Zipperposition.
Wed, 30 Jul 2014 10:50:30 +0200 desharna document property 'set_induct'
Wed, 30 Jul 2014 10:50:28 +0200 desharna generate 'set_induct' theorem for codatatypes
Wed, 30 Jul 2014 00:50:41 +0200 blanchet also try 'metis' with 'full_types'
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip