src/HOL/Nominal/Examples/ROOT.ML

refer to THIS_JAVA dynamically, and treat ISABELLE_JAVA as static default -- relevant for nested JVM invocation within an existing Isabelle enviroment;

use_thys ["Nominal_Examples"];

setmp_noncritical quick_and_dirty true use_thys ["VC_Condition"];