# File HOL.ML

    (* legacy ML bindings *)

    val choice_eq = thm "choice_eq";

    structure HOL =
    struct
      val thy = the_context ();
      val eq_reflection = eq_reflection;
      val refl = refl;
      val subst = subst;
      val ext = ext;
      val impI = impI;
      val mp = mp;
      val True_def = True_def;
      val All_def = All_def;
      val Ex_def = Ex_def;
      val False_def = False_def;
      val not_def = not_def;
      val and_def = and_def;
      val or_def = or_def;
      val Ex1_def = Ex1_def;
      val iff = iff;
      val True_or_False = True_or_False;
      val Let_def = Let_def;
      val if_def = if_def;
    end;

    open HOL;