changeset 58889 | 5b7a9633cfa8 |
parent 44375 | dfc2e722fe47 |
child 58963 | 26bf09b95dda |
58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
---|---|
1 (* Title: HOL/NanoJava/Example.thy |
1 (* Title: HOL/NanoJava/Example.thy |
2 Author: David von Oheimb |
2 Author: David von Oheimb |
3 Copyright 2001 Technische Universitaet Muenchen |
3 Copyright 2001 Technische Universitaet Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header "Example" |
6 section "Example" |
7 |
7 |
8 theory Example |
8 theory Example |
9 imports Equivalence |
9 imports Equivalence |
10 begin |
10 begin |
11 |
11 |