--- a/thys/uncomputable.thy	Wed Jan 30 09:33:06 2013 +0000
+++ b/thys/uncomputable.thy	Wed Jan 30 23:00:09 2013 +0000
@@ -104,6 +104,9 @@
 apply(simp_all add: assms)
 done
 
+lemma begin_partial_correctness:
+  assumes "\<exists>stp. steps0 cf tcopy_begin stp = (0, l, r)"
+
 fun measure_begin_state :: "config \<Rightarrow> nat"
   where
   "measure_begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"