--- a/thys/Abacus_Mopup.thy	Fri Feb 15 14:07:39 2013 +0000
+++ b/thys/Abacus_Mopup.thy	Fri Feb 15 23:02:20 2013 +0800
@@ -666,20 +666,6 @@
 lemma mod_ex2: "(a mod (2::nat) = 0) = (\<exists> q. a = 2 * q)"
 by arith
 
-(*
-lemma [simp]: "(a mod 2 \<noteq> Suc 0) = (a mod 2 = 0)  "
-by arith
-
-lemma [simp]: "(a mod 2 \<noteq> 0) = (a mod 2 = Suc 0)  "
-by arith
-
-
-lemma [simp]: "(2*q - Suc 0) div 2 = (q - 1)"
-by arith
-
-lemma [simp]: "(Suc (2*q)) div 2 = q"
-by arith
-*)
 lemma mod_2: "x mod 2  = 0 \<or>  x mod 2 = Suc 0"
 by arith
 
@@ -858,8 +844,6 @@
     done
 qed
 
-(*we can use Hoare_plus here*)
-
 lemma wf_mopup[intro]: "tm_wf (mopup n, 0)"
 apply(induct n, simp add: mopup.simps shift.simps mopup_b_def tm_wf.simps)
 apply(auto simp: mopup.simps shift.simps mopup_b_def tm_wf.simps)