src/HOL/MicroJava/BV/Listn.thy
changeset 22271 51a80e238b29
parent 22068 00bed5ac9884
child 23464 bc2563c37b1a
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:41:11 2007 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Wed Feb 07 17:44:07 2007 +0100
     1.3 @@ -321,22 +321,22 @@
     1.4    "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
     1.5  apply (unfold acc_def)
     1.6  apply (subgoal_tac
     1.7 - "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
     1.8 - apply (erule wf_subset)
     1.9 + "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
    1.10 + apply (erule wfP_subset)
    1.11   apply (blast intro: lesssub_list_impl_same_size)
    1.12 -apply (rule wf_UN)
    1.13 +apply (rule wfP_SUP)
    1.14   prefer 2
    1.15   apply clarify
    1.16   apply (rename_tac m n)
    1.17   apply (case_tac "m=n")
    1.18    apply simp
    1.19 - apply (fast intro!: equals0I dest: not_sym)
    1.20 + apply (fast intro!: equals0I [to_pred] dest: not_sym)
    1.21  apply clarify
    1.22  apply (rename_tac n)
    1.23  apply (induct_tac n)
    1.24   apply (simp add: lesssub_def cong: conj_cong)
    1.25  apply (rename_tac k)
    1.26 -apply (simp add: wf_eq_minimal)
    1.27 +apply (simp add: wfP_eq_minimal)
    1.28  apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
    1.29  apply clarify
    1.30  apply (rename_tac M m)