Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/List.thy
changeset 25130 d91391a8705b
parent 25112 98824cc791c0
child 25134 3d4953e88449 
--- a/src/HOL/List.thy	Sun Oct 21 14:21:44 2007 +0200
+++ b/src/HOL/List.thy	Sun Oct 21 14:21:45 2007 +0200
@@ -2152,7 +2152,11 @@
  apply (clarsimp simp add: set_conv_nth)
  apply (erule_tac x = 0 in allE, simp)
  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
+(*TOO SLOW
 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
+*)
+apply (erule_tac x = "Suc i" in allE, simp)
+apply (erule_tac x = "Suc j" in allE, simp)
 done
 
 lemma nth_eq_iff_index_eq:
isabelle