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