(* Title: HOL/main.ML ID: $Id$ Classical Higher-order Logic -- only "Main". *) set new_locales; use_thy "Main";