changeset 58886 | 8a6cac7c7247 |
parent 42463 | f270e3e18be5 |
child 61361 | 8b5f00202e1a |
58885:47fdd4f40d00 | 58886:8a6cac7c7247 |
---|---|
1 (* Title: HOL/MicroJava/DFA/Typing_Framework.thy |
1 (* Title: HOL/MicroJava/DFA/Typing_Framework.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Typing and Dataflow Analysis Framework} *} |
6 section {* Typing and Dataflow Analysis Framework *} |
7 |
7 |
8 theory Typing_Framework |
8 theory Typing_Framework |
9 imports Listn |
9 imports Listn |
10 begin |
10 begin |
11 |
11 |