(*theory Main includes everything; note that theory PreList already includes most HOL theories*) Main = Map + String