| changeset 22271 | 51a80e238b29 |
| parent 22068 | 00bed5ac9884 |
| child 27611 | 2c01c0bdb385 |
--- a/src/HOL/MicroJava/BV/Err.thy Wed Feb 07 17:41:11 2007 +0100 +++ b/src/HOL/MicroJava/BV/Err.thy Wed Feb 07 17:44:07 2007 +0100 @@ -155,7 +155,7 @@ lemma acc_err [simp, intro!]: "acc r \<Longrightarrow> acc(le r)" apply (unfold acc_def lesub_def le_def lesssub_def) -apply (simp add: wf_eq_minimal split: err.split) +apply (simp add: wfP_eq_minimal split: err.split) apply clarify apply (case_tac "Err : Q") apply blast