To use the tactic univ_rcf, 1). In a Linux environment, set MATH_KERNEL to an executable of Mathematica Kernel 2). univ_rcf and univ_rcf_cert should now work if RCF_Decision_Proc.thy is loaded. Examples can be found in Univ_RCF_Example.thy Note, the source is for Isabelle 2016. If there is any problem, please email to Wenda Li<email@example.comfirstname.lastname@example.org>.