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.