--- a/src/HOL/MicroJava/J/JListExample.thy Wed Feb 20 17:30:46 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Thu Feb 21 09:54:08 2002 +0100
@@ -3,7 +3,7 @@
Author: Stefan Berghofer
*)
-header {* Example for generating executable code from Java semantics *}
+header {* \isaheader{Example for generating executable code from Java semantics} *}
theory JListExample = Eval:
@@ -107,7 +107,7 @@
Expr ({list_name}(LAcc l1_name)..
append_name({[RefT (ClassT list_name)]}[LAcc l4_name])))-> _"
-subsection {* Big step execution *}
+section {* Big step execution *}
ML {*