| changeset 42150 | b0c0638c4aad |
| parent 35416 | d8d7d1b785af |
| child 58886 | 8a6cac7c7247 |
| 42149:7e6f4ca198bb | 42150:b0c0638c4aad |
|---|---|
1 (* Title: HOL/MicroJava/BV/Typing_Framework_err.thy |
1 (* Title: HOL/MicroJava/DFA/Typing_Framework_err.thy |
2 Author: Gerwin Klein |
2 Author: Gerwin Klein |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *} |
6 header {* \isaheader{Lifting the Typing Framework to err, app, and eff} *} |