--- 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"