| changeset 58622 | aa99568f56de |
| parent 58372 | bfd497f2f4c2 |
| child 58889 | 5b7a9633cfa8 |
| 58621:7a2c567061b3 | 58622:aa99568f56de |
|---|---|
8 imports Old_Datatype |
8 imports Old_Datatype |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 Derivation of Warshall's algorithm using program extraction, |
12 Derivation of Warshall's algorithm using program extraction, |
13 based on Berger, Schwichtenberg and Seisenberger \cite{Berger-JAR-2001}. |
13 based on Berger, Schwichtenberg and Seisenberger @{cite "Berger-JAR-2001"}. |
14 *} |
14 *} |
15 |
15 |
16 datatype b = T | F |
16 datatype b = T | F |
17 |
17 |
18 primrec |
18 primrec |