src/HOL/MicroJava/BV/Listn.thy
changeset 26806 40b411ec05aa
parent 23757 087b0a241557
child 27611 2c01c0bdb385
equal deleted inserted replaced
26805:27941d7d9a11 26806:40b411ec05aa
   328  prefer 2
   328  prefer 2
   329  apply clarify
   329  apply clarify
   330  apply (rename_tac m n)
   330  apply (rename_tac m n)
   331  apply (case_tac "m=n")
   331  apply (case_tac "m=n")
   332   apply simp
   332   apply simp
   333  apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
   333  apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
   334 apply clarify
   334 apply clarify
   335 apply (rename_tac n)
   335 apply (rename_tac n)
   336 apply (induct_tac n)
   336 apply (induct_tac n)
   337  apply (simp add: lesssub_def cong: conj_cong)
   337  apply (simp add: lesssub_def cong: conj_cong)
   338 apply (rename_tac k)
   338 apply (rename_tac k)