| changeset 22068 | 00bed5ac9884 |
| parent 16417 | 9bc16273c2d4 |
| child 22271 | 51a80e238b29 |
--- a/src/HOL/MicroJava/BV/Opt.thy Tue Jan 16 08:06:55 2007 +0100 +++ b/src/HOL/MicroJava/BV/Opt.thy Tue Jan 16 08:06:57 2007 +0100 @@ -54,7 +54,7 @@ lemma order_le_opt [intro!,simp]: "order r \<Longrightarrow> order(le r)" -apply (subst order_def) +apply (subst Semilat.order_def) apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym) done