Hets - the Heterogeneous Tool Set

Copyright(c) Sonja Groening Christian Maeder Uni Bremen 2004-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

Isabelle.IsaConsts

Contents

Description

constants for Isabelle

Synopsis

Documentation

topSort :: (a -> a -> Bool) -> [a] -> [a] Source #

a topological sort with a uses predicate

liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool Source #

extends a dependency relation to lists using any

boolean constants strings

cTrue :: String Source #

cFalse :: String Source #

cNot :: String Source #

Not string

quantor strings

allS :: String Source #

exS :: String Source #

ex1S :: String Source #

Strings of binary ops

conj :: String Source #

disj :: String Source #

impl :: String Source #

eq :: String Source #

neq :: String Source #

plusS :: String Source #

minusS :: String Source #

timesS :: String Source #

divS :: String Source #

modS :: String Source #

consS :: String Source #

lconsS :: String Source #

appendS :: String Source #

compS :: String Source #

pairC :: String Source #

lower case pair

eqvSimS :: String Source #

unionS :: String Source #

membershipS :: String Source #

imageS :: String Source #

Imange of functions

rangeS :: String Source #

some stuff for Isabelle

pcpoS :: String Source #

some stuff for HasCASL

aptS :: String Source #

appS :: String Source #

pAppS :: String Source #

defOpS :: String Source #

someS :: String Source #

Some string

strings for HOLCF lifting functions

lliftbinS :: String Source #

fliftbinS :: String Source #

flift2S :: String Source #

Predefined CLASSES

predefined SORTS

mkSTypeT :: Continuity -> String -> Typ Source #

predefined types

mkSType :: String -> Typ Source #

predefinded HOLCF types

mkSDomType :: String -> Typ Source #

mkBinDomType :: String -> Typ -> Typ -> Typ Source #

term construction

maxPrio :: Int Source #

1000

lowPrio :: Int Source #

10

mkConstVD :: String -> Typ -> Term Source #

construct constants and variables

mkConstV :: String -> DTyp -> Term Source #

mkFree :: String -> Term Source #

con :: VName -> Term Source #

construct a constant with no type

conDouble :: String -> Term Source #

conDoubleC :: String -> Term Source #

binVNameAppl :: VName -> Term -> Term -> Term Source #

apply VName operator to two term

binary junctors

termAppl :: Term -> Term -> Term Source #

HOL function application

terms for HOL-HOLCF

Boolean constants

UNTYPED terms

defOp :: Term Source #

defOp constant

notOp :: Term Source #

Not constant

conSome :: Term Source #

some constant

HOLCF

constant names

notV :: VName Source #

Not VName

VNames of binary operators

vMap' :: Map String VName Source #

vMap :: Map String VName Source #

keywords in theory files from the Isar Reference Manual 2005

endS :: String Source #

headerS :: String Source #

theoryS :: String Source #

importsS :: String Source #

usesS :: String Source #

beginS :: String Source #

contextS :: String Source #

axiomsS :: String Source #

defsS :: String Source #

oopsS :: String Source #

mlS :: String Source #

mlFileS :: String Source #

andS :: String Source #

lemmasS :: String Source #

lemmaS :: String Source #

corollaryS :: String Source #

refuteS :: String Source #

theoremsS :: String Source #

theoremS :: String Source #

axclassS :: String Source #

classesS :: String Source #

definitionS :: String Source #

instanceS :: String Source #

typedeclS :: String Source #

typesS :: String Source #

constsS :: String Source #

structureS :: String Source #

constdefsS :: String Source #

domainS :: String Source #

datatypeS :: String Source #

fixrecS :: String Source #

primrecS :: String Source #

declareS :: String Source #

simpS :: String Source #

applyS :: String Source #

backS :: String Source #

deferS :: String Source #

preferS :: String Source #

byS :: String Source #

doneS :: String Source #

sorryS :: String Source #

autoS :: String Source #

inductS :: String Source #

caseTacS :: String Source #

insertS :: String Source #

subgoalTacS :: String Source #

typedefS :: String Source #

metaImplS :: String Source #

usingS :: String Source #

whereS :: String Source #

dotDot :: String Source #

barS :: String Source #

markups :: [String] Source #

ignoredKeys :: [String] Source #

toplevel keys that are currently ignored

usedTopKeys :: [String] Source #

toplevel keywords currently recognized by IsaParse

isaKeywords :: [String] Source #

all Isabelle keywords

mkVName :: String -> VName Source #