src/FOL/FOL.ML

theorems case_split = case_split_thm [case_names True False, cases type: o];

structure FOL =
struct
  val thy = the_context ();
  val classical = classical;
end;

AddXEs [disjI1, disjI2];

open FOL;