--- a/Implementation.thy	Mon Jul 03 15:29:29 2017 +0100
+++ b/Implementation.thy	Fri Jul 07 15:10:14 2017 +0100
@@ -396,12 +396,12 @@
   the @{text cp}-values for @{text th} and @{text taker}.
 *}
 
-lemma "taker \<notin> children (tG (e#s)) th"
+lemma t1: "taker \<notin> children (tG (e#s)) th"
   by (metis children_subtree empty_iff in_mono neq_taker_th root_def set_mp
           subtree_ancestorsI taker_ready_es vat_es.root_readys_tG)
   
 
-lemma "th \<notin> children (tG (e#s)) taker"
+lemma t2: "th \<notin> children (tG (e#s)) taker"
   by (metis children_subtree empty_iff  neq_taker_th root_def 
          subsetD subtree_ancestorsI th_ready_es vat_es.root_readys_tG)