# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1467032901 -3600
# Node ID 6a7a8c51d42ff8ef595d10a27ef4d1c8604ab6b1
# Parent  0f124691c1919175ca085f439787830256a93f64
unified Rtree.

diff -r 0f124691c191 -r 6a7a8c51d42f PIPBasics.thy
--- a/PIPBasics.thy	Fri Jun 17 09:46:25 2016 +0100
+++ b/PIPBasics.thy	Mon Jun 27 14:08:21 2016 +0100
@@ -2837,7 +2837,7 @@
 
 lemma rtree_RAG: "rtree (RAG s)"
   using sgv_RAG acyclic_RAG
-  by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+  by (unfold rtree_def, auto)
 
 end
 
diff -r 0f124691c191 -r 6a7a8c51d42f RTree.thy
--- a/RTree.thy	Fri Jun 17 09:46:25 2016 +0100
+++ b/RTree.thy	Mon Jun 27 14:08:21 2016 +0100
@@ -1,6 +1,5 @@
 theory RTree
-imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
-        (* "Lcrules" *)
+imports "~~/src/HOL/Library/Transitive_Closure_Table" 
 begin
 
 section {* A theory of relational trees *}
@@ -21,18 +20,10 @@
   {\em single valued} and {\em acyclic}. 
 *}
 
-text {*
-  The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}.
-*}
-locale sgv = 
+
+locale rtree = 
   fixes r
   assumes sgv: "single_valued r"
-
-text {*
-  The following @{text "rtree"} specifies that @{text "r"} is a 
-  {\em Relational Tree}.
-*}
-locale rtree = sgv + 
   assumes acl: "acyclic r"
 
 text {*