src/FOL/FOL.ML

added thms to perm_compose (so far only composition
theorems were included where the type of the permutation
was equal)

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

open FOL;