--- a/Paper/Paper.thy	Wed Feb 06 04:32:18 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 06 04:39:08 2013 +0000
@@ -1307,7 +1307,7 @@
   the arity, say @{term l}, we can define an inductive evaluation relation that  
   relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l},
   to what the result of the recursive function is, say @{text n}---we omit the straightforward
-  definition of @{term "rec_cal_rel r ns n"}. Because of space reasons, we also omit the 
+  definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the 
   definition of translating
   recursive functions into abacus programs. We can prove the following
   theorem about the translation: Assuming 

Binary file paper.pdf has changed

--- a/thys/UTM.thy	Wed Feb 06 04:32:18 2013 +0000
+++ b/thys/UTM.thy	Wed Feb 06 04:39:08 2013 +0000
@@ -711,8 +711,8 @@
 by(simp)
 
 lemma tape_of_nl_cons_app1: "(<a # xs @ [b]>) = (Oc\<up>(Suc a) @ Bk # (<xs@ [b]>))"
-apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps)
+apply(case_tac xs, simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
+apply(simp add: tape_of_nl_abv  tape_of_nat_list.simps tape_of_nat_abv)
 done
 
 lemma bl_bin_bk_oc[simp]:
@@ -1231,7 +1231,7 @@
       done
   qed
   thus "?thesis"
-    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
+    apply(simp add: tape_of_nl_abv tape_of_nat_list.simps tape_of_nat_abv)
     done
 qed