(* Title: HOL/plain.ML ID: $Id$ Classical Higher-order Logic -- plain Tool bootstrap. *) use_thy "Plain";