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;