avoid prove_plain, export_plain, simplified after_qed;
witness = term * thm, i.e. the original proposition with a protected fact
(this achieves reliable discharge and allows facts to be slightly more general/normalized);
internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly;
ObjectLogic.ensure_propT;
(* Title: HOL/Import/Generate-HOL/ROOT.ML
ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
use_thy "GenHOL4Prob";
use_thy "GenHOL4Vec";
use_thy "GenHOL4Word32";