thys/uncomputable.thy
changeset 112 fea23f9a9d85
parent 109 4635641e77cb
child 141 4d7a568bd911
--- a/thys/uncomputable.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/thys/uncomputable.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -15,7 +15,12 @@
   and "3 = Suc 2"
   and "4 = Suc 3" 
   and "5 = Suc 4" 
-  and "6 = Suc 5" by arith+
+  and "6 = Suc 5" 
+  and "7 = Suc 6"
+  and "8 = Suc 7" 
+  and "9 = Suc 8" 
+  and "10 = Suc 9" 
+  by arith+
 
 text {*
   The {\em Copying} TM, which duplicates its input.