src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 9970 dfe4747c8318
     1.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4    assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
     1.5  
     1.6    obtain phi where fits: "fits phi ins G rT ?s0 cert"    
     1.7 -    by (rule exists_phi [elimified]) blast
     1.8 +    by (rule exists_phi [elim_format]) blast
     1.9  
    1.10    with wtl
    1.11    have allpc: