diff -r dfc629cd11de -r fea23f9a9d85 thys/abacus.thy
--- a/thys/abacus.thy	Sun Feb 03 13:31:14 2013 +0000
+++ b/thys/abacus.thy	Mon Feb 04 01:17:09 2013 +0000
@@ -6,14 +6,6 @@
 imports uncomputable
 begin
 
-(*
-declare tm_comp.simps [simp add] 
-declare adjust.simps[simp add] 
-declare shift.simps[simp add]
-declare tm_wf.simps[simp add]
-declare step.simps[simp add]
-declare steps.simps[simp add]
-*)
 declare replicate_Suc[simp add]
 
 text {*
@@ -1731,23 +1723,6 @@
 lemma wf_inc_le[intro]: "wf inc_LE"
 by(auto intro:wf_inv_image simp: inc_LE_def lex_triple_def lex_pair_def)
 
-lemma numeral_5_eq_5: "5 = Suc (Suc (Suc (Suc (Suc 0))))"
-by arith
-
-lemma numeral_6_eq_6: "6 = Suc (Suc (Suc (Suc (Suc 1))))"
-by arith
-
-lemma numeral_7_eq_7: "7 = Suc (Suc (Suc (Suc (Suc 2))))"
-by arith
-
-lemma numeral_8_eq_8: "8 = Suc (Suc (Suc (Suc (Suc 3))))"
-by arith
-
-lemma numeral_9_eq_9: "9 = Suc (Suc (Suc (Suc (Suc (Suc 3)))))"
-by arith
-
-lemma numeral_10_eq_10: "10 = Suc (Suc (Suc (Suc (Suc (Suc (Suc 3))))))"
-by arith
 
 lemma inv_locate_b_2_after_write[simp]: 
       "inv_locate_b (as, am) (n, aaa, Bk # xs) ires
@@ -2153,9 +2128,8 @@
       apply(simp add:Q)
       apply(simp add: inc_inv.simps)
       apply(case_tac c, case_tac [2] aa)
-      apply(auto simp: Let_def step.simps tinc_b_def numeral_2_eq_2 numeral_3_eq_3  split: if_splits)
-      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral_5_eq_5
-                          numeral_6_eq_6 numeral_7_eq_7 numeral_8_eq_8 numeral_9_eq_9)         
+      apply(auto simp: Let_def step.simps tinc_b_def numeral  split: if_splits)
+      apply(simp_all add: inc_inv.simps inc_LE_def lex_triple_def lex_pair_def inc_measure_def numeral)         
       done
   qed
 qed
@@ -3682,7 +3656,7 @@
         apply(simp_all split: if_splits)
         using fetch layout dec_suc
         apply(auto simp: step.simps P dec_inv_2.simps Let_def abc_dec_2_LE_def lex_triple_def lex_pair_def lex_square_def
-                         fix_add numeral_3_eq_3) 
+                         fix_add numeral) 
         done
     qed
   qed