more robust norm_proof: turn env into instantiation, based on visible statement;
chapter Miscsession Tools = Pure + theories Code_Generator Profilingsession SML in SML = Pure + theories Examplessession Haskell in Haskell = HOL + theories Haskell theories [condition = ISABELLE_GHC_STACK] Test