src/HOL/Bali/WellForm.thy
changeset 22424 8a5412121687
parent 21765 89275a3ed7be
child 23350 50c5b0912a0c
     1.1 --- a/src/HOL/Bali/WellForm.thy	Fri Mar 09 08:45:53 2007 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Mar 09 08:45:55 2007 +0100
     1.3 @@ -1634,8 +1634,7 @@
     1.4  	by (auto dest!: stat_overrides_commonD)
     1.5        from super old wf accmodi_old
     1.6        have accmodi_super_method: "Protected \<le> accmodi super_method"
     1.7 -	by (auto dest!: wf_prog_stat_overridesD
     1.8 -                 intro: order_trans)
     1.9 +	by (auto dest!: wf_prog_stat_overridesD)
    1.10        from super accmodi_old wf
    1.11        have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)"
    1.12  	by (auto dest!: wf_prog_stat_overridesD
    1.13 @@ -1747,8 +1746,7 @@
    1.14      then have "\<not> is_static new" by (auto dest: stat_overrides_commonD)
    1.15      with Overriding not_static_old accmodi_old wf 
    1.16      show ?thesis 
    1.17 -      by (auto dest!: wf_prog_stat_overridesD
    1.18 -               intro: order_trans)
    1.19 +      by (auto dest!: wf_prog_stat_overridesD)
    1.20    qed
    1.21  qed
    1.22