diff options
| author |  leino <unknown> | 2015-05-10 08:28:54 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-10 08:28:54 -0700 |
| commit | 2e88568000690f3b5e79069e0fdcba5fef8f5ca9 (patch) | |
| tree | a63330579dc56f1117acc3ca2d3f34c2d7b28704 /Test/dafny4/NipkowKlein-chapter3.dfy | |
| parent | 9e999ccbf8581acf181ff00a529de96e12c690d5 (diff) | |
Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Klein book on semantics.
It includes many uses of inductive predicates and inductive lemmas.
Diffstat (limited to 'Test/dafny4/NipkowKlein-chapter3.dfy')
| -rw-r--r-- | Test/dafny4/NipkowKlein-chapter3.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy index df56a3b3..024ef9bd 100644 --- a/Test/dafny4/NipkowKlein-chapter3.dfy +++ b/Test/dafny4/NipkowKlein-chapter3.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file is a Dafny encoding of chapter 3 from "Concrete Semantics: With Isabelle/HOL" by
|