diff -r 4b717aa162fa -r 8a13b37b4d95 PIPBasics.thy
--- a/PIPBasics.thy	Thu Jul 07 13:32:09 2016 +0100
+++ b/PIPBasics.thy	Fri Jul 08 01:25:19 2016 +0100
@@ -2835,16 +2835,16 @@
 context valid_trace
 begin
 
-lemma rtree_RAG: "rtree (RAG s)"
+lemma forest_RAG: "forest (RAG s)"
   using sgv_RAG acyclic_RAG
-  by (unfold rtree_def, auto)
+  by (unfold forest_def, auto)
 
 end
 
-sublocale valid_trace < rtree_RAG?: rtree "RAG s"
-  using rtree_RAG .
-
-sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
+sublocale valid_trace < forest_RAG?: forest "RAG s"
+  using forest_RAG .
+
+sublocale valid_trace < fsbtRAGs?: fforest "RAG s"
 proof
   show "\<And>x. finite (children (RAG s) x)"
     by (smt Collect_empty_eq Range.intros children_def finite.emptyI finite_RAG finite_fbranchI) 
@@ -2886,7 +2886,7 @@
   finite-branch relational tree (or forest):  
 *}
 
-sublocale valid_trace < rtree_s?: rtree "tRAG s"
+sublocale valid_trace < forest_s?: forest "tRAG s"
 proof(unfold_locales)
   from sgv_tRAG show "single_valued (tRAG s)" .
 next
@@ -2894,7 +2894,7 @@
 qed
 
 
-sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
+sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
 proof
   fix x
   show "finite (children (tRAG s) x)"
@@ -3210,7 +3210,7 @@
     obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)"
                          "rpath (RAG s) n xs2 (Th th2)" by metis
     hence False
-    proof(cases rule:rtree_RAG.rpath_overlap')
+    proof(cases rule:forest_RAG.rpath_overlap')
       case (less_1 xs3)
       from rpath_star[OF this(3)]
       have "Th th1 \<in> subtree (RAG s) (Th th2)"