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/MicroJava/BV/Listn.thy
changeset 26806 40b411ec05aa
parent 23757 087b0a241557
child 27611 2c01c0bdb385 
--- a/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:57:19 2008 +0200
@@ -330,7 +330,7 @@
  apply (rename_tac m n)
  apply (case_tac "m=n")
   apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
+ apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
 apply clarify
 apply (rename_tac n)
 apply (induct_tac n)
isabelle