Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder, DFKI 2008
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Comorphisms.PPolyTyConsHOL2IsaUtils

Description

utility function for translation from HasCASL to Isabelle leaving open how partial values are interpreted

Documentation

mapTheory :: SimpKind -> Simplifier -> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])

simpForPairs :: Simplifier

simpForOption :: Simplifier

typeToks :: Env -> Set String

transSentence :: Env -> Set String -> SimpKind -> Simplifier -> Sentence -> Result Sentence

data SimpKind

Constructors

New 
Old OldSimpKind 

Instances

data OldSimpKind

Constructors

NoSimpLift 
Lift2Restrict 
Lift2Case 

Instances