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.
avoid very slow metis invocation;
authorwenzelm
Sun, 21 Oct 2007 14:21:45 +0200
changeset 25130 d91391a8705b
parent 25129 de54445dc82c
child 25131 2c8caac48ade
avoid very slow metis invocation;
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- 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