src/HOL/MicroJava/BV/LBVComplete.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
     1.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4      case None
     1.5      with wtl fits
     1.6      show ?thesis 
     1.7 -      by - (rule wtl_inst_mono [elimified], (simp add: wtl_cert_def)+)
     1.8 +      by - (rule wtl_inst_mono [elim_format], (simp add: wtl_cert_def)+)
     1.9    next
    1.10      case Some
    1.11      with wtl fits
    1.12 @@ -406,7 +406,7 @@
    1.13    "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
    1.14    wtl_method G C pTs rT mxl ins cert"
    1.15  by (simp add: wt_method_def wtl_method_def)
    1.16 -   (rule wt_imp_wtl_inst_list [rulified, elimified], auto simp add: wt_start_def) 
    1.17 +   (rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) 
    1.18  
    1.19  
    1.20  lemma wtl_method_complete:
    1.21 @@ -462,17 +462,17 @@
    1.22  
    1.23      from 1
    1.24      show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
    1.25 -    proof (rule bspec [elimified], clarsimp)
    1.26 +    proof (rule bspec [elim_format], clarsimp)
    1.27        assume ub : "unique b"
    1.28        assume m: "\<forall>(sig,rT,mb)\<in>set b. wf_mhead G sig rT \<and> 
    1.29                    (\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb" 
    1.30        from m b
    1.31        show ?thesis
    1.32 -      proof (rule bspec [elimified], clarsimp)
    1.33 +      proof (rule bspec [elim_format], clarsimp)
    1.34          assume "wt_method G a ba ad ae bb (Phi a (ac, ba))"         
    1.35          with wfprog uG ub b 1
    1.36          show ?thesis
    1.37 -          by - (rule wtl_method_complete [elimified], assumption+, 
    1.38 +          by - (rule wtl_method_complete [elim_format], assumption+, 
    1.39                  simp add: make_Cert_def unique_epsilon)
    1.40        qed 
    1.41      qed