summaryrefslogtreecommitdiff
path: root/Test/dafny0/InductivePredicates.dfy
Commit message (Expand)AuthorAge
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
* Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* Additional test case for inductive predicatesGravatar leino2015-05-07
* Added "inductive lemma" methodsGravatar leino2015-05-07
* Added inductive predicatesGravatar leino2015-05-06