diff -r 6a7a8c51d42f -r d9974794436a PIPBasics.thy
--- a/PIPBasics.thy	Mon Jun 27 14:08:21 2016 +0100
+++ b/PIPBasics.thy	Mon Jul 04 14:04:11 2016 +0100
@@ -2844,17 +2844,12 @@
 sublocale valid_trace < rtree_RAG?: rtree "RAG s"
   using rtree_RAG .
 
-sublocale valid_trace < fsbtRAGs?: fsubtree "RAG s"
-proof -
-  show "fsubtree (RAG s)"
-  proof(intro_locales)
-    show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
-  next
-    show "fsubtree_axioms (RAG s)"
-    proof(unfold fsubtree_axioms_def)
-      from wf_RAG show "wf (RAG s)" .
-    qed
-  qed
+sublocale valid_trace < fsbtRAGs?: fgraph "RAG s"
+proof
+  show "\<forall>x\<in>Range (RAG s). finite (children (RAG s) x)" 
+    by (rule finite_fbranchI[OF finite_RAG])
+next
+  show "wf (RAG s)" using wf_RAG .
 qed
 
 subsection {* Derived properties for sub-graphs of RAG *}
@@ -2897,36 +2892,31 @@
   from acyclic_tRAG show "acyclic (tRAG s)" .
 qed
 
-sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s"
-proof -
-  have "fsubtree (tRAG s)"
-  proof -
-    have "fbranch (tRAG s)"
-    proof(unfold tRAG_def, rule fbranch_compose)
-        show "fbranch (wRAG s)"
+sublocale valid_trace < fsbttRAGs?: fgraph "tRAG s"
+proof
+  show "\<forall>x\<in>Range (tRAG s). finite (children (tRAG s) x)"
+  proof(unfold tRAG_def, rule fbranch_compose)
+        show "\<forall>x\<in>Range (wRAG s). finite (children (wRAG s) x)"
         proof(rule finite_fbranchI)
            from finite_RAG show "finite (wRAG s)"
            by (unfold RAG_split, auto)
         qed
     next
-        show "fbranch (hRAG s)"
+        show "\<forall>x\<in>Range (hRAG s). finite (children (hRAG s) x)"
         proof(rule finite_fbranchI)
            from finite_RAG 
            show "finite (hRAG s)" by (unfold RAG_split, auto)
         qed
-    qed
-    moreover have "wf (tRAG s)"
-    proof(rule wf_subset)
+  qed
+next
+  show "wf (tRAG s)"
+  proof(rule wf_subset)
       show "wf (RAG s O RAG s)" using wf_RAG
         by (fold wf_comp_self, simp)
-    next
+  next
       show "tRAG s \<subseteq> (RAG s O RAG s)"
         by (unfold tRAG_alt_def, auto)
-    qed
-    ultimately show ?thesis
-      by (unfold fsubtree_def fsubtree_axioms_def,auto)
   qed
-  from this[folded tRAG_def] show "fsubtree (tRAG s)" .
 qed
 
 section {* Chain to readys *}