diff -r 95e7933968f8 -r a88af0e4731f RTree.thy
--- a/RTree.thy	Thu Jun 02 13:15:03 2016 +0100
+++ b/RTree.thy	Tue Jun 07 13:51:39 2016 +0100
@@ -45,40 +45,42 @@
 definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)"
 
 text {*
-  To reason about {\em Relational Graph}, a notion of path is 
-  needed, which is given by the following @{text "rpath"} (short 
-  for `relational path`). 
-  The path @{text "xs"} in proposition @{text "rpath r x xs y"} is 
-  a path leading from @{text "x"} to @{text "y"}, which serves as a 
-  witness of the fact @{text "(x, y) \<in> r^*"}. 
 
-  @{text "rpath"}
-  is simply a wrapper of the @{text "rtrancl_path"} defined in the imported 
-  theory @{text "Transitive_Closure_Table"}, which defines 
-  a notion of path for the predicate form of binary relations. 
-*}
+  To reason about {\em Relational Graph}, a notion of path is needed,
+  which is given by the following @{text "rpath"} (short for
+  `relational path`).  The path @{text "xs"} in proposition @{text
+  "rpath r x xs y"} is a path leading from @{text "x"} to @{text "y"},
+  which serves as a witness of the fact @{text "(x, y) \<in> r^*"}.
+
+  @{text "rpath"} is simply a wrapper of the @{text "rtrancl_path"}
+  defined in the imported theory @{text "Transitive_Closure_Table"},
+  which defines a notion of path for the predicate form of binary
+  relations.  *}
+
 definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y"
 
 text {*
-  Given a path @{text "ps"}, @{text "edges_on ps"} is the 
-  set of edges along the path, which is defined as follows:
-*}
+
+  Given a path @{text "ps"}, @{text "edges_on ps"} is the set of edges
+  along the path, which is defined as follows: *}
 
 definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}"
 
 text {*
-   The following @{text "indep"} defines a notion of independence. 
+
+   The following @{text "indep"} defines a notion of independence.
    Two nodes @{text "x"} and @{text "y"} are said to be independent
-   (expressed as @{text "indep x y"}),  if neither one is reachable 
-   from the other in relational graph @{text "r"}.
-*}
+   (expressed as @{text "indep x y"}), if neither one is reachable
+   from the other in relational graph @{text "r"}.  *}
+
 definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))"
 
 text {*
-  In relational tree @{text "r"}, the sub tree of node @{text "x"} is written
-  @{text "subtree r x"}, which is defined to be the set of nodes (including itself) 
-  which can reach @{text "x"} by following some path in @{text "r"}:
-*}
+ 
+ In relational tree @{text "r"}, the sub tree of node @{text "x"} is
+  written @{text "subtree r x"}, which is defined to be the set of
+  nodes (including itself) which can reach @{text "x"} by following
+  some path in @{text "r"}: *}
 
 definition "subtree r x = {y . (y, x) \<in> r^*}"
 
@@ -87,17 +89,20 @@
 definition "root r x = (ancestors r x = {})"
 
 text {*
-  The following @{text "edge_in r x"} is the set of edges
-  contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph.
-*}
+ 
+  The following @{text "edge_in r x"} is the set of edges contained in
+  the sub-tree of @{text "x"}, with @{text "r"} as the underlying
+  graph.  *}
 
 definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}"
 
 text {*
-  The following lemma @{text "edges_in_meaning"} shows the intuitive meaning 
-  of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`, 
-  i.e., both @{text "a"} and @{text "b"} are in the sub-tree.
-*}
+
+  The following lemma @{text "edges_in_meaning"} shows the intuitive
+  meaning of `an edge @{text "(a, b)"} is in the sub-tree of @{text
+  "x"}`, i.e., both @{text "a"} and @{text "b"} are in the sub-tree.
+  *}
+
 lemma edges_in_meaning: 
   "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"
  by (auto simp:edges_in_def subtree_def)
@@ -1735,12 +1740,6 @@
   with h_b(2) and that show ?thesis by metis
 qed
 
-(*
-lcrules crules
-
-declare crules(26,43,44,45,46,47)[rule del]
-*)
-
 
 declare RTree.subtree_transfer[rule del]