src/HOL/IMPP/Hoare.ML

 by (clarsimp_tac (claset(), simpset() addsimps
   [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
 qed "MGF_complete";
 
 AddSEs WTs_elim_cases;
+AddIffs [not_None_eq];
 (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
 Goal "state_not_singleton ==> \
 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
 by (induct_tac "c" 1);
 by        (ALLGOALS Clarsimp_tac);