--- a/Implementation.thy	Wed Aug 02 13:18:14 2017 +0100
+++ b/Implementation.thy	Wed Aug 02 14:56:47 2017 +0100
@@ -690,7 +690,7 @@
   show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)
 qed
 
-lemma cp_kept_tG:
+lemma cp_kept_tG: (* aaa *)
   assumes "th'' \<notin> ancestors (tG (e#s)) th"
   shows "cp (e#s) th'' = cp s th''"
   using cp_kept tG_ancestors_tRAG_refute assms
@@ -859,7 +859,7 @@
   show ?thesis by metis
 qed
 
-lemma cp_up_tG:
+lemma cp_up_tG: (* aaa *)
   assumes "th' \<in> ancestors (tG (e#s)) th"
   and "cp (e#s) th' = cp s th'"
   and "th'' \<in> ancestors (tG (e#s)) th'"