src/HOL/Bali/AxCompl.thy

 apply clarsimp
 apply (rule MGF_asm [THEN MGFNormalD])
 apply   (auto intro: MGFNormalI)
 done
 
-lemma MGF_deriv: "wf_prog G \<Longrightarrow> G,({}::state triple set)\<turnstile>{\<doteq>} t\<succ> {G\<rightarrow>}"
-apply (rule MGF_asm)
-apply (intro strip)
-apply (rule MGFNormalI)
-apply (rule ax_derivs.weaken)
-apply  (erule MGF_simult_Methd)
-apply auto
-done
-
 
 section "corollaries"
 
 lemma eval_to_evaln: "\<lbrakk>G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (Y', s');type_ok G t s; wf_prog G\<rbrakk>
  \<Longrightarrow>   \<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"