more operations on types and terms;
abstract syntax operations for Pure and HOL;