--- 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)