less physical "logic" argument, with option -l like "isabelle console" etc.;
(* 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"