src/HOL/IMP/ACom.thy
changeset 46225 d0a2c4a80a00
parent 46157 3d518b508bbb
child 47613 e72e44cee6f2
--- a/src/HOL/IMP/ACom.thy	Sat Jan 14 21:16:15 2012 +0100
+++ b/src/HOL/IMP/ACom.thy	Sun Jan 15 17:27:46 2012 +0100
@@ -7,7 +7,7 @@
 (* is there a better place? *)
 definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
 
-section "Annotated Commands"
+subsection "Annotated Commands"
 
 datatype 'a acom =
   SKIP   'a                           ("SKIP {_}" 61) |