changeset 20217 | 25b068a99d2b |
parent 19803 | aa2581752afb |
child 23746 | a455e69c31cc |
--- a/src/HOL/IMPP/Hoare.thy Wed Jul 26 13:31:07 2006 +0200 +++ b/src/HOL/IMPP/Hoare.thy Wed Jul 26 19:23:04 2006 +0200 @@ -381,7 +381,6 @@ apply (drule finite_subset) apply (erule finite_imageI) apply (simp (no_asm_simp)) -apply arith done lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>