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