HOL-ex.Code_Assertion