| changeset 12911 | 704713ca07ea |
| parent 12517 | 360e3215f029 |
| child 12951 | a9fdcb71d252 |
| 12910:f5bceeec9d91 | 12911:704713ca07ea |
|---|---|
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header "Example MicroJava Program" |
7 header {* \isaheader{Example MicroJava Program} *} |
8 |
8 |
9 theory Example = Eval: |
9 theory Example = Eval: |
10 |
10 |
11 text {* |
11 text {* |
12 The following example MicroJava program includes: |
12 The following example MicroJava program includes: |