Added package for definition by specification.
Added optional theorem names for the constant definitions added during
*** empty log message ***
Changed bstring argument to xstring.
Added the specification command.
Added handling of free variables (provided they are of sort HOL.type).
Added handling of meta implication and meta quantification.
Allowed for splitting the specification over several lemmas.