--- a/src/HOL/Bali/WellForm.thy Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Bali/WellForm.thy Fri Mar 09 08:45:55 2007 +0100
@@ -1634,8 +1634,7 @@
by (auto dest!: stat_overrides_commonD)
from super old wf accmodi_old
have accmodi_super_method: "Protected \<le> accmodi super_method"
- by (auto dest!: wf_prog_stat_overridesD
- intro: order_trans)
+ by (auto dest!: wf_prog_stat_overridesD)
from super accmodi_old wf
have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
by (auto dest!: wf_prog_stat_overridesD
@@ -1747,8 +1746,7 @@
then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
with Overriding not_static_old accmodi_old wf
show ?thesis
- by (auto dest!: wf_prog_stat_overridesD
- intro: order_trans)
+ by (auto dest!: wf_prog_stat_overridesD)
qed
qed