changeset 9906 | 5c027cca6262 |
parent 9757 | 1024a2d80ac0 |
child 9941 | fe05af7ec816 |
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Sep 07 21:06:55 2000 +0200 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Sep 07 21:10:11 2000 +0200 @@ -264,7 +264,7 @@ assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err" obtain phi where fits: "fits phi ins G rT ?s0 cert" - by (rule exists_phi [elimify]) blast + by (rule exists_phi [elimified]) blast with wtl have allpc: