equal
deleted
inserted
replaced
218 by (clarsimp_tac (claset(), simpset() addsimps |
218 by (clarsimp_tac (claset(), simpset() addsimps |
219 [hoare_valids_def,eval_eq,triple_valid_def2]) 1); |
219 [hoare_valids_def,eval_eq,triple_valid_def2]) 1); |
220 qed "MGF_complete"; |
220 qed "MGF_complete"; |
221 |
221 |
222 AddSEs WTs_elim_cases; |
222 AddSEs WTs_elim_cases; |
|
223 AddIffs [not_None_eq]; |
223 (* requires com_det, escape (i.e. hoare_derivs.conseq) *) |
224 (* requires com_det, escape (i.e. hoare_derivs.conseq) *) |
224 Goal "state_not_singleton ==> \ |
225 Goal "state_not_singleton ==> \ |
225 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"; |
226 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"; |
226 by (induct_tac "c" 1); |
227 by (induct_tac "c" 1); |
227 by (ALLGOALS Clarsimp_tac); |
228 by (ALLGOALS Clarsimp_tac); |