src/HOL/Bali/AxCompl.thy
changeset 13524 604d0f3622d6
parent 13384 a34e38154413
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -766,15 +766,6 @@
     1.4  apply   (auto intro: MGFNormalI)
     1.5  done
     1.6  
     1.7 -lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
     1.8 -apply (rule MGF_asm)
     1.9 -apply (intro strip)
    1.10 -apply (rule MGFNormalI)
    1.11 -apply (rule ax_derivs.weaken)
    1.12 -apply  (erule MGF_simult_Methd)
    1.13 -apply auto
    1.14 -done
    1.15 -
    1.16  
    1.17  section "corollaries"
    1.18