HOL-ex.Argo_Examples