blanchet [Fri, 01 Aug 2014 16:07:33 +0200] rev 57757
tuning
blanchet [Fri, 01 Aug 2014 16:07:33 +0200] rev 57756
peek instead of joining -- is perhaps less risky
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57755
export ML function
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57754
compile
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57753
removed 'metisFT' support in Mirabelle
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57752
removed Mirabelle minimization code
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57751
modernized Mirabelle (a bit) and made it compile
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57750
restored a bit of laziness
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57749
reorder quantifiers to ease Z3 skolemization
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57748
tuned order of arguments
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57747
tuned name context code
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57746
tuned whitespace
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57745
more rational unskolemizing of names
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57744
added appropriate method for skolemization of Z3 steps to the mix
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57743
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57742
honor 'try0' also for one-liners
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57741
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57740
further minimize one-liner
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57739
tuning
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57738
eliminated needlessly complex message tail
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57737
updated NEWS
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57736
update documentation after removal of 'min' subcommand
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57735
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57734
rationalized preplaying by eliminating (now superfluous) laziness
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57733
removed proof methods as provers from docs
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57732
simplified minimization logic
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57731
tuning
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57730
remove lambda-lifting related assumptions from generated Isar proofs
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57729
whitespace tuning
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57728
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
blanchet [Fri, 01 Aug 2014 14:43:57 +0200] rev 57727
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
traytel [Thu, 31 Jul 2014 13:19:57 +0200] rev 57726
simplified tactics slightly
blanchet [Thu, 31 Jul 2014 00:45:55 +0200] rev 57725
cascading timeout in parallel evaluation, to rapidly find optimum
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57724
put faster proof methods first
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57723
use parallel preplay machinery also for one-line proofs
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57722
updated docs
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57721
always minimize Sledgehammer results by default
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57720
tuned ML function name
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57719
reduced preplay timeout to 1 s
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57718
added more proof methods for one-liners
blanchet [Wed, 30 Jul 2014 23:52:56 +0200] rev 57717
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
fleury [Wed, 30 Jul 2014 14:03:58 +0200] rev 57716
Improving robustness and indentation corrections.
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57715
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57714
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57713
Whitespace and indentation correction.
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57712
Simplifying the labels in the proof of the SMT solver veriT.
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57711
Changing ~ into - for unuary minus (not supported by veriT)
fleury [Wed, 30 Jul 2014 14:03:13 +0200] rev 57710
imported patch satallax_skolemization_in_tree_part
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57709
imported patch hilbert_choice_support
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57708
veriT changes for lifted terms, and ite_elim rules.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57707
imported patch satallax_proof_support_Sledgehammer
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57706
Basic support for the higher-order ATP Satallax.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57705
Subproofs for the SMT solver veriT.
fleury [Wed, 30 Jul 2014 14:03:12 +0200] rev 57704
Basic support for the SMT prover veriT.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57703
removing the '= True' generated by Leo-II.
fleury [Wed, 30 Jul 2014 14:03:11 +0200] rev 57702
Skolemization support for leo-II and Zipperposition.