# HG changeset patch
# User nipkow
# Date 1319551742 -7200
# Node ID 13b5fb92b9f5ca165fe78fc58046bc84115cdbe1
# Parent  521508e85c0dfe81278df19a27ffcf1c31dbcb32
tuned text

diff -r 521508e85c0d -r 13b5fb92b9f5 src/HOL/IMP/ASM.thy
--- a/src/HOL/IMP/ASM.thy	Tue Oct 25 15:59:15 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Tue Oct 25 16:09:02 2011 +0200
@@ -1,8 +1,8 @@
-header "Arithmetic Stack Machine and Compilation"
+header "Stack Machine and Compilation"
 
 theory ASM imports AExp begin
 
-subsection "Arithmetic Stack Machine"
+subsection "Stack Machine"
 
 text_raw{*\begin{isaverbatimwrite}\newcommand{\ASMinstrdef}{% *}
 datatype instr = LOADI val | LOAD vname | ADD