specific bundle for x86_64-linux, which is especially important for JRE due to its extra library dependencies;
(* Title: ZF/Resid/ROOT.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Executes the Residuals example.
This is a proof of the Church-Rosser Theorem for the untyped lambda-calculus.
By Ole Rasmussen, following the Coq proof given in
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
J. Functional Programming 4(3) 1994, 371-394.
*)
use_thys ["Confluence"];