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

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 MonadicHasCASL2IsabelleHOL

The identity of the comorphism

Constructors

MonadicHasCASL2IsabelleHOL

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