diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,11 +1,11 @@
-(*  Title:      HOL/UNITY/Reachability
-    ID:         $Id$
+(*  Title:      HOL/UNITY/Reachability.thy
     Author:     Tanja Vos, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
-Reachability in Graphs
+Reachability in Graphs.
 
-From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2
+and 11.3.
 *)
 
 theory Reachability imports "../Detects" Reach begin
@@ -300,7 +300,7 @@
              ((reachable v <==> {s. (root,v): REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
 apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
 apply (subgoal_tac
-	 "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
+         "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
               UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
               nmsg_eq 0 (v,w) ")
 apply simp