diff -r 251e192339b7 -r 559e5c6e5113 thys/abacus.thy
--- a/thys/abacus.thy	Thu Jan 17 11:51:00 2013 +0000
+++ b/thys/abacus.thy	Fri Jan 18 11:40:01 2013 +0000
@@ -381,7 +381,7 @@
 lemma abc_step_red: 
  "abc_steps_l ac aprog stp = (as, am) \<Longrightarrow> 
    abc_steps_l ac aprog (Suc stp) = abc_step_l (as, am) (abc_fetch as aprog) "
-sorry
+oops
 
 lemma tm_shift_fetch: 
   "\<lbrakk>fetch A s b = (ac, ns); ns \<noteq> 0 \<rbrakk>
@@ -445,12 +445,7 @@
        (Suc s - start_of ly as) b = (ac, ns)"
   and notfinal: "ns \<noteq> 0"
   shows "fetch tp s b = (ac, ns)"
-proof -
-  have "s > start_of ly as \<and> s < start_of ly (Suc as)"
-    sorry
-  thus "fetch tp s b = (ac, ns)"
-    sorry
-qed
+oops
   
 lemma step_eq_in:
   assumes layout: "ly = layout_of ap"