merged
authornipkow
Fri, 21 Oct 2011 08:25:04 +0200
changeset 45223 62ca94616539
parent 45221 3eadb9b6a055 (current diff)
parent 45222 6eab55bab82f (diff)
child 45225 7da4e22714fb
child 45238 ed2bb3b58cc4
merged
--- a/src/HOL/IMP/ASM.thy	Thu Oct 20 22:26:02 2011 +0200
+++ b/src/HOL/IMP/ASM.thy	Fri Oct 21 08:25:04 2011 +0200
@@ -4,7 +4,7 @@
 
 subsection "Arithmetic Stack Machine"
 
-datatype ainstr = LOADI val | LOAD string | ADD
+datatype ainstr = LOADI val | LOAD vname | ADD
 
 type_synonym stack = "val list"