src/HOL/SizeChange/Graphs.thy

--- a/src/HOL/SizeChange/Graphs.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/SizeChange/Graphs.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Graphs.thy
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
@@ -710,7 +709,7 @@
   let ?p = "p\<langle>s i,s (Suc i)\<rangle>"
 
   from increasing_strict 
-	have "fst (p (s (Suc i))) = end_node ?p" by simp
+  have "fst (p (s (Suc i))) = end_node ?p" by simp
   moreover
   from increasing_strict[of s i "Suc i"] have "snd ?p \<noteq> []"
     by (simp add:sub_path_def)