Copyright	(c) C. Maeder, DFKI 2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.PCoClTyConsHOL2PairsInIsaHOL

Description

An embedding comorphism from HasCASL without subtypes to Isabelle-HOL.

Synopsis

Documentation

The identity of the comorphism

Constructors

Show PCoClTyConsHOL2PairsInIsaHOL
Language PCoClTyConsHOL2PairsInIsaHOL
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () ()