--- a/PIPBasics.thy	Mon Mar 21 14:33:02 2016 +0000
+++ b/PIPBasics.thy	Mon Mar 21 14:41:40 2016 +0000
@@ -2913,10 +2913,10 @@
 
 end
 
-sublocale valid_trace < rtree_RAG: rtree "RAG s"
+sublocale valid_trace < rtree_RAG?: rtree "RAG s"
   using rtree_RAG .
 
-sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"
+sublocale valid_trace < fsbtRAGs?: fsubtree "RAG s"
 proof -
   show "fsubtree (RAG s)"
   proof(intro_locales)
@@ -2962,14 +2962,14 @@
   finite-branch relational tree (or forest):  
 *}
 
-sublocale valid_trace < rtree_s: rtree "tRAG s"
+sublocale valid_trace < rtree_s?: rtree "tRAG s"
 proof(unfold_locales)
   from sgv_tRAG show "single_valued (tRAG s)" .
 next
   from acyclic_tRAG show "acyclic (tRAG s)" .
 qed
 
-sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"
+sublocale valid_trace < fsbttRAGs?: fsubtree "tRAG s"
 proof -
   have "fsubtree (tRAG s)"
   proof -