summaryrefslogtreecommitdiff
path: root/Test/dafny0/CoinductiveProofs.dfy
Commit message (Expand)AuthorAge
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/l...Gravatar Rustan Leino2015-10-02
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Fixed the problem with the previous check-in.Gravatar Rustan Leino2013-01-18
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
* Support for copredicates and prefix predicates in comethods.Gravatar Rustan Leino2012-12-04
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
* New feature:Gravatar Rustan Leino2012-10-11