Hets - the Heterogeneous Tool Set

Copyright(c) Soeren Schulze Uni Bremen 2012
LicenseGPLv2 or higher, see LICENSE.txt
Maintainers.schulze@uni-bremen.de
Stabilityexperimental
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.CommonLogic2IsabelleHOL

Description

A direct comorphism from CommonLogic to Isabelle-HOL, passing arguments as native Isabelle lists.

Documentation

data CommonLogic2IsabelleHOL Source #

Instances

Show CommonLogic2IsabelleHOL Source # 
Language CommonLogic2IsabelleHOL Source # 
Comorphism CommonLogic2IsabelleHOL CommonLogic CommonLogicSL BASIC_SPEC TEXT_META SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

individualS :: String Source #

type RENAMES = Map String VName Source #

mkIndName :: String -> VName Source #

addRenames :: RENAMES -> [String] -> RENAMES Source #

makeRenames :: [String] -> RENAMES Source #

rename :: RENAMES -> String -> VName Source #

quantify :: RENAMES -> QUANT -> String -> Term -> Term Source #