# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1361249793 0
# Node ID 2fad78b479a33f3fe9596abf851e01a71eb220e0
# Parent  7386b3758360d3f63e83aa95380bd62da07e3af8
added clear-definition to paper

diff -r 7386b3758360 -r 2fad78b479a3 Paper/Paper.thy
--- 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 *}
diff -r 7386b3758360 -r 2fad78b479a3 ROOT
--- a/ROOT	Tue Feb 19 04:31:18 2013 +0000
+++ b/ROOT	Tue Feb 19 04:56:33 2013 +0000
@@ -1,4 +1,4 @@
-session utm = HOL +
+session UTM = HOL +
   options [document = false]
   theories
     "thys/Turing"
diff -r 7386b3758360 -r 2fad78b479a3 paper.pdf
Binary file paper.pdf has changed