# File IFOL.ML

    structure IFOL =
    struct
      val thy = the_context ();
      val refl = refl;
      val subst = subst;
      val conjI = conjI;
      val conjunct1 = conjunct1;
      val conjunct2 = conjunct2;
      val disjI1 = disjI1;
      val disjI2 = disjI2;
      val disjE = disjE;
      val impI = impI;
      val mp = mp;
      val FalseE = FalseE;
      val True_def = True_def;
      val not_def = not_def;
      val iff_def = iff_def;
      val ex1_def = ex1_def;
      val allI = allI;
      val spec = spec;
      val exI = exI;
      val exE = exE;
      val eq_reflection = eq_reflection;
      val iff_reflection = iff_reflection;
    end;

    open IFOL;