# HG changeset patch
# User wenzelm
# Date 1236259742 -3600
# Node ID a16af775e08d6a40692ebde8ecbda27c1f5a3138
# Parent  9ad15d8ed31172d9a68ee0d49afa456919adbfe0
fixed proofs -- follow-up to ecd6f0ca62ea;

diff -r 9ad15d8ed311 -r a16af775e08d src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Thu Mar 05 12:11:25 2009 +0100
+++ b/src/HOL/SizeChange/Graphs.thy	Thu Mar 05 14:29:02 2009 +0100
@@ -351,7 +351,7 @@
 
 lemma in_tcl: 
   "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
-  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps)
+  apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps power_Suc)
   apply (rule_tac x = "n - 1" in exI, auto)
   done