Haskell2IsabelleHOLCF.hs revision eb0e19a83d8e3eaeb936c197555b20d37129022c
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : $Header$
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : All rights reserved.
Portability : non-portable (imports Logic.Logic)
module Comorphisms.Haskell2IsabelleHOLCF where
import Comorphisms.Hs2HOLCF as Hs2HOLCF
import Logic.Logic as Logic
import Logic.Comorphism
import Haskell.Logic_Haskell
import Haskell.HatParser as HatParser
import Haskell.HatAna as HatAna
import Isabelle.IsaSign as IsaSign
import Isabelle.Logic_Isabelle
HatAna.Sign HaskellMorphism
Isabelle () () IsaSign.Sentence () ()
Hs2HOLCF.transTheory IsCont False sign sens
HatAna.Sign HaskellMorphism
Isabelle () () IsaSign.Sentence () ()
Hs2HOLCF.transTheory NotCont False sign sens