| changeset 13524 | 604d0f3622d6 |
| parent 12486 | 0ed8bdd883e0 |
| child 13612 | 55d32e76ef4e |
--- a/src/HOL/IMPP/Hoare.ML Tue Aug 27 11:03:02 2002 +0200 +++ b/src/HOL/IMPP/Hoare.ML Tue Aug 27 11:03:05 2002 +0200 @@ -352,10 +352,10 @@ by (Simp_tac 1); by (eatac MGF_lemma2_simult 1 1); by (rtac subset_refl 1); -qed "MGF"; +qed "MGF'"; (* requires Body+empty+insert / BodyN, com_det *) -bind_thm ("hoare_complete", MGF RS MGF_complete); +bind_thm ("hoare_complete", MGF' RS MGF_complete); section "unused derived rules";