Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder DFKI 2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

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 Source #

The identity of the comorphism

Instances

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