--- a/Implementation.thy	Fri Jun 23 00:27:16 2017 +0100
+++ b/Implementation.thy	Tue Jun 27 14:49:42 2017 +0100
@@ -7,7 +7,7 @@
   The use of dependants has been abandoned. Through a series of lemma 
   named xxx_alt_def, lemma originally expressed using dependants 
   is now expressed in terms of RAG, tRAG and tG.
-*)
+*)                                            
 
 text {*
 
@@ -863,7 +863,7 @@
   by (unfold tRAG_alt_def RAG_es, auto)
 
 lemma tG_kept: "tG (e#s) = tG s"
-  by (unfold tG_def tRAG_kept, simp)
+  by (unfold tG_def_tRAG tRAG_kept, simp)
 
 text {*
   The following lemma shows that @{text th} is completely isolated 
@@ -971,7 +971,7 @@
   Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.
 *}
 lemma tG_kept: "tG (e#s) = tG s"
-  by (unfold tG_def tRAG_kept, simp)
+  by (unfold tG_def_tRAG tRAG_kept, simp)
 
 lemma th_RAG: "Th th \<notin> Field (RAG s)"
 proof -
@@ -1016,7 +1016,7 @@
   shows "cp (e#s) th' = cp s th'"
 proof -
   have "(the_preced (e # s) ` subtree (tG (e # s)) th') =
-        (the_preced s ` subtree (tG s) th')"
+          (the_preced s ` subtree (tG s) th')"
   proof -
     { fix a
       assume "a \<in> subtree (tG s) th'"