src/HOL/MicroJava/BV/Listn.thy
changeset 23757 087b0a241557
parent 23464 bc2563c37b1a
child 26806 40b411ec05aa
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:29:44 2007 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Jul 11 11:32:02 2007 +0200
     1.3 @@ -330,7 +330,7 @@
     1.4   apply (rename_tac m n)
     1.5   apply (case_tac "m=n")
     1.6    apply simp
     1.7 - apply (fast intro!: equals0I [to_pred] dest: not_sym)
     1.8 + apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
     1.9  apply clarify
    1.10  apply (rename_tac n)
    1.11  apply (induct_tac n)