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.PCoClTyConsHOL2IsabelleHOL

Description

The embedding comorphism from HasCASL without subtypes to Isabelle-HOL. Partial functions yield an option or bool result in Isabelle. Case-terms and constructor classes are not supported yet.

Synopsis

Documentation

data PCoClTyConsHOL2IsabelleHOL

The identity of the comorphism

Constructors

PCoClTyConsHOL2IsabelleHOL

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