diff -r 51dc6c7b1fd7 -r bc9e5587d05a src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Tue Apr 06 16:19:45 2004 +0200
+++ b/src/HOL/Induct/Com.thy	Wed Apr 07 14:25:48 2004 +0200
@@ -6,6 +6,8 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
+header{*Mutual Induction via Iteratived Inductive Definitions*}
+
 theory Com = Main:
 
 typedecl loc
@@ -27,6 +29,9 @@
       | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
       | While exp com          ("WHILE _ DO _"  60)
 
+
+subsection {* Commands *}
+
 text{* Execution of commands *}
 consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
        "@exec"  :: "((exp*state) * (nat*state)) set => 
@@ -97,7 +102,7 @@
 done
 
 
-section {* Expressions *}
+subsection {* Expressions *}
 
 text{* Evaluation of arithmetic expressions *}
 consts  eval    :: "((exp*state) * (nat*state)) set"