proper try_run for exactly one evaluation of body (amending 91c3aedbfc5e);
(* additional abbreviations for syntactic completion *)(*prevent replacement of very long arrows*)"===>" = "===>""--->" = "\<midarrow>\<rightarrow>"(*HOL-NSA*)"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S""--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"