Paper/Paper.thy
changeset 185 2fad78b479a3
parent 171 1bad3ec5bcd5
child 186 455411d69c12
--- a/Paper/Paper.thy	Tue Feb 19 04:31:18 2013 +0000
+++ b/Paper/Paper.thy	Tue Feb 19 04:56:33 2013 +0000
@@ -163,7 +163,9 @@
   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"
 by(auto simp add: layout_of.simps length_of.simps)
 
-
+fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
+  where
+  "clear n e = [Dec n e, Goto 0]"
 (*>*)
 
 section {* Introduction *}