src/HOL/Main.ML
author wenzelm
Fri, 20 Jul 2001 21:52:54 +0200
changeset 11432 8a203ae6efe3
parent 9650 6f0b89f2a1f9
permissions -rw-r--r--
added "The" (definite description operator) (by Larry);


structure Main =
struct
  val thy = the_context ();
end;