diff -r 47fdd4f40d00 -r 8a6cac7c7247 src/HOL/MicroJava/DFA/Semilat.thy
--- a/src/HOL/MicroJava/DFA/Semilat.thy	Sun Nov 02 17:39:52 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sun Nov 02 17:58:35 2014 +0100
@@ -3,10 +3,9 @@
     Copyright   2000 TUM
 *)
 
-header {* 
-  \chapter{Bytecode Verifier}\label{cha:bv}
-  \isaheader{Semilattices} 
-*}
+chapter {* Bytecode Verifier \label{cha:bv} *}
+
+section {* Semilattices *}
 
 theory Semilat
 imports Main "~~/src/HOL/Library/While_Combinator"