--- a/thys/Abacus_Hoare.thy	Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Abacus_Hoare.thy	Fri Dec 21 15:30:24 2018 +0100
@@ -240,6 +240,7 @@
 apply(rule_tac abc_comp_frist_steps_halt_eq', simp_all)
 done
 
+
 lemma abc_comp_second_step_eq: 
   assumes exec: "abc_step_l (s, lm) (abc_fetch s B) = (sa, lma)"
   shows "abc_step_l (s + length A, lm) (abc_fetch (s + length A) (A [+] B))