--- a/Implementation.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/Implementation.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -161,7 +161,7 @@
   "ancestors (RAG s) (Cs cs) = {Th th}"
 proof -
   have "ancestors (RAG s) (Cs cs) = ancestors (RAG s) (Th th)  \<union>  {Th th}"
-   by (rule rtree_RAG.ancestors_accum[OF edge_of_th])
+   by (rule forest_RAG.ancestors_accum[OF edge_of_th])
   from this[unfolded ancestors_th] show ?thesis by simp
 qed
 
@@ -193,7 +193,7 @@
   "ancestors (RAG s) (Th taker) = {Th th, Cs cs}" 
 proof -
   have "ancestors (RAG s) (Th taker) = ancestors (RAG s) (Cs cs) \<union> {Cs cs}"
-  proof(rule  rtree_RAG.ancestors_accum)
+  proof(rule  forest_RAG.ancestors_accum)
     from sub_RAGs' show "(Th taker, Cs cs) \<in> RAG s" by auto
   qed
   thus ?thesis using ancestors_th ancestors_cs by auto
@@ -311,7 +311,7 @@
 
 lemma subtree_th: 
   "subtree (RAG (e#s)) (Th th) = subtree (RAG s) (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule rtree_RAG.subtree_del_inside)
+proof(unfold RAG_s, fold subtree_cs, rule forest_RAG.subtree_del_inside)
   from edge_of_th
   show "(Cs cs, Th th) \<in> edges_in (RAG s) (Th th)"
     by (unfold edges_in_def, auto simp:subtree_def)
@@ -482,7 +482,7 @@
           assume a_in: "a \<in> ?A"
           from 1(2)
           show "?f a = ?g a"
-          proof(cases rule:vat_es.rtree_s.ancestors_childrenE[case_names in_ch out_ch])
+          proof(cases rule:vat_es.forest_s.ancestors_childrenE[case_names in_ch out_ch])
              case in_ch
              show ?thesis
              proof(cases "a = u")
@@ -494,7 +494,7 @@
                 proof
                   assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                   have "a = u"
-                  proof(rule vat_es.rtree_s.ancestors_children_unique)
+                  proof(rule vat_es.forest_s.ancestors_children_unique)
                     from a_in' a_in show "a \<in> ancestors (tRAG (e#s)) (Th th) \<inter> 
                                           RTree.children (tRAG (e#s)) x" by auto
                   next 
@@ -528,7 +528,7 @@
               proof
                 assume a_in': "a \<in> ancestors (tRAG (e#s)) (Th th)"
                 have "a = z"
-                proof(rule vat_es.rtree_s.ancestors_children_unique)
+                proof(rule vat_es.forest_s.ancestors_children_unique)
                   from assms(1) h(1) have "z \<in> ancestors (tRAG (e#s)) (Th th)"
                       by (auto simp:ancestors_def)
                   with h(2) show " z \<in> ancestors (tRAG (e#s)) (Th th) \<inter>