blanchet [Fri, 01 Aug 2014 20:08:50 +0200] rev 57763
nicer generated variable names
blanchet [Fri, 01 Aug 2014 19:44:18 +0200] rev 57762
tuning
blanchet [Fri, 01 Aug 2014 19:36:23 +0200] rev 57761
tuning
blanchet [Fri, 01 Aug 2014 19:32:46 +0200] rev 57760
no need to 'obtain' variables not in formula
blanchet [Fri, 01 Aug 2014 19:32:10 +0200] rev 57759
more precise handling of LEO-II skolemization
blanchet [Fri, 01 Aug 2014 16:07:34 +0200] rev 57758
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
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.