more operations on types and terms;
abstract syntax operations for Pure and HOL;
chapter Toolssession Tools = Pure + theories Code_Generatorsession SML in SML = Pure + theories Examplessession Haskell in Haskell = HOL + theories Haskell theories [condition = ISABELLE_GHC_STACK] Test