| changeset 60758 | d8d85a8172b5 |
| parent 58889 | 5b7a9633cfa8 |
| 60757:c09598a97436 | 60758:d8d85a8172b5 |
|---|---|
4 Copyright 2013 |
4 Copyright 2013 |
5 |
5 |
6 Coinduction method that avoids some boilerplate compared to coinduct. |
6 Coinduction method that avoids some boilerplate compared to coinduct. |
7 *) |
7 *) |
8 |
8 |
9 section {* Coinduction Method *} |
9 section \<open>Coinduction Method\<close> |
10 |
10 |
11 theory Coinduction |
11 theory Coinduction |
12 imports Ctr_Sugar |
12 imports Ctr_Sugar |
13 begin |
13 begin |
14 |
14 |