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
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip