changeset 12911 | 704713ca07ea |
parent 12516 | d09d0f160888 |
child 13006 | 51c5f3f11d16 |
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Wed Feb 20 17:30:46 2002 +0100 +++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Thu Feb 21 09:54:08 2002 +0100 @@ -5,7 +5,7 @@ *) -header "Static and Dynamic Welltyping" +header {* \isaheader{Static and Dynamic Welltyping} *} theory Typing_Framework_err = Typing_Framework: