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<>.