chapter Tools session Spec_Check in Spec_Check = Pure + theories Spec_Check Examples session SML in SML = Pure + theories Examples session Haskell in Haskell = Pure + theories Haskell theories [condition = ISABELLE_GHC] Test