Mon, 18 Jun 2012 15:48:43 +0200 class target handles additional non-class term parameters appropriately
haftmann [Mon, 18 Jun 2012 15:48:43 +0200] rev 48102
class target handles additional non-class term parameters appropriately
Tue, 12 Jun 2012 15:32:14 +0200 merged
Andreas Lochbihler [Tue, 12 Jun 2012 15:32:14 +0200] rev 48101
merged
Tue, 12 Jun 2012 15:31:53 +0200 add lemma to FinFun
Andreas Lochbihler [Tue, 12 Jun 2012 15:31:53 +0200] rev 48100
add lemma to FinFun
Wed, 06 Jun 2012 21:36:21 +0200 fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss [Wed, 06 Jun 2012 21:36:21 +0200] rev 48099
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
Wed, 06 Jun 2012 10:35:05 +0200 tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48098
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
Wed, 06 Jun 2012 10:35:05 +0200 pass more facts to LEO-II, in the light of latest evaluation
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48097
pass more facts to LEO-II, in the light of latest evaluation
Wed, 06 Jun 2012 10:35:05 +0200 prevent an "Empty" exception (e.g. with Satallax, "mono_native")
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48096
prevent an "Empty" exception (e.g. with Satallax, "mono_native")
Wed, 06 Jun 2012 10:35:05 +0200 tuning terminology
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48095
tuning terminology
Wed, 06 Jun 2012 10:35:05 +0200 updated NEWS
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48094
updated NEWS
Wed, 06 Jun 2012 10:35:05 +0200 updated docs
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48093
updated docs
Wed, 06 Jun 2012 10:35:05 +0200 added "args_query" encodings
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48092
added "args_query" encodings
Wed, 06 Jun 2012 10:35:05 +0200 removed killed encodings from Metis examples
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48091
removed killed encodings from Metis examples
Wed, 06 Jun 2012 10:35:05 +0200 updated docs
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48090
updated docs
Wed, 06 Jun 2012 10:35:05 +0200 killed most unsound encodings
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48089
killed most unsound encodings
Wed, 06 Jun 2012 10:35:05 +0200 generalized monotonic constructor optimisation so that it works with e.g. the product type
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48088
generalized monotonic constructor optimisation so that it works with e.g. the product type
Wed, 06 Jun 2012 10:35:05 +0200 removed micro-optimization whose justification I can't recall
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48087
removed micro-optimization whose justification I can't recall
Wed, 06 Jun 2012 10:35:05 +0200 add missing timeout multiplier
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48086
add missing timeout multiplier
Wed, 06 Jun 2012 10:35:05 +0200 avoid dumping definitions several times in LEO-II proofs
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48085
avoid dumping definitions several times in LEO-II proofs
Wed, 06 Jun 2012 10:35:05 +0200 robust LEO-II setup that doesn't rely on ".leoatprc"
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48084
robust LEO-II setup that doesn't rely on ".leoatprc"
Wed, 06 Jun 2012 10:35:05 +0200 renamed TPTP commands to agree with Sutcliffe's terminology
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48083
renamed TPTP commands to agree with Sutcliffe's terminology
Wed, 06 Jun 2012 10:35:05 +0200 don't use aggressive with HO ATP
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48082
don't use aggressive with HO ATP
Wed, 06 Jun 2012 10:35:05 +0200 more aggressive type argument optimization
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48081
more aggressive type argument optimization
Wed, 06 Jun 2012 10:35:05 +0200 use cover for "poly_guards" encoding
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48080
use cover for "poly_guards" encoding
Wed, 06 Jun 2012 10:35:05 +0200 hack to make LEO-II perform better on TPTP THF problems
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48079
hack to make LEO-II perform better on TPTP THF problems
Wed, 06 Jun 2012 10:35:05 +0200 swap adjectives (cf. Google)
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48078
swap adjectives (cf. Google)
Wed, 06 Jun 2012 10:35:05 +0200 tweaked remote Vampire version
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48077
tweaked remote Vampire version
Wed, 06 Jun 2012 10:35:05 +0200 don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway
blanchet [Wed, 06 Jun 2012 10:35:05 +0200] rev 48076
don't cripple Sledgehammer/ATP needlessly just because of "metis" -- there's also "smt" as a fallback anyway
Tue, 05 Jun 2012 10:12:54 +0200 apply preprocessing simpset also to rhs of abstract code equations
haftmann [Tue, 05 Jun 2012 10:12:54 +0200] rev 48075
apply preprocessing simpset also to rhs of abstract code equations
Tue, 05 Jun 2012 07:11:49 +0200 clarified code translation code
haftmann [Tue, 05 Jun 2012 07:11:49 +0200] rev 48074
clarified code translation code
Tue, 05 Jun 2012 07:10:51 +0200 prefer sys.error over plain error in Scala to avoid deprecation warning
haftmann [Tue, 05 Jun 2012 07:10:51 +0200] rev 48073
prefer sys.error over plain error in Scala to avoid deprecation warning
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 tip