| changeset 22271 | 51a80e238b29 |
| parent 22068 | 00bed5ac9884 |
| child 27680 | 5a557a5afc48 |
--- a/src/HOL/MicroJava/BV/Opt.thy Wed Feb 07 17:41:11 2007 +0100 +++ b/src/HOL/MicroJava/BV/Opt.thy Wed Feb 07 17:44:07 2007 +0100 @@ -272,7 +272,7 @@ lemma acc_le_optI [intro!]: "acc r \<Longrightarrow> acc(le r)" apply (unfold acc_def lesub_def le_def lesssub_def) -apply (simp add: wf_eq_minimal split: option.split) +apply (simp add: wfP_eq_minimal split: option.split) apply clarify apply (case_tac "? a. Some a : Q") apply (erule_tac x = "{a . Some a : Q}" in allE)