Rafal Kolanski <rafal.kolanski@nicta.com.au> [Tue, 19 Jun 2012 11:18:09 +0200] rev 48107
Updated comment to reflect current state.
haftmann [Sun, 17 Jun 2012 20:38:12 +0200] rev 48106
clarifying comment
blanchet [Mon, 18 Jun 2012 17:50:06 +0200] rev 48105
sound monotonicity inference in the presence of "aggressive" helpers
blanchet [Mon, 18 Jun 2012 17:50:06 +0200] rev 48104
less confusing error message
blanchet [Mon, 18 Jun 2012 17:50:06 +0200] rev 48103
removed dead code
haftmann [Mon, 18 Jun 2012 15:48:43 +0200] rev 48102
class target handles additional non-class term parameters appropriately
Andreas Lochbihler [Tue, 12 Jun 2012 15:32:14 +0200] rev 48101
merged
Andreas Lochbihler [Tue, 12 Jun 2012 15:31:53 +0200] rev 48100
add lemma to FinFun
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
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