Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed proofs -- follow-up to ecd6f0ca62ea;
authorwenzelm
Thu, 05 Mar 2009 14:29:02 +0100
changeset 30282 a16af775e08d
parent 30281 9ad15d8ed311
child 30283 520872460b7b
fixed proofs -- follow-up to ecd6f0ca62ea;
src/HOL/SizeChange/Graphs.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle