changeset 42150 | b0c0638c4aad |
parent 41541 | 1fa4725c4656 |
child 42463 | f270e3e18be5 |
42149:7e6f4ca198bb | 42150:b0c0638c4aad |
---|---|
1 (* Title: HOL/MicroJava/BV/Err.thy |
1 (* Title: HOL/MicroJava/DFA/Err.thy |
2 Author: Tobias Nipkow |
2 Author: Tobias Nipkow |
3 Copyright 2000 TUM |
3 Copyright 2000 TUM |
4 *) |
4 *) |
5 |
5 |
6 header {* \isaheader{The Error Type} *} |
6 header {* \isaheader{The Error Type} *} |