Isabelle.IsaConsts

Contents

• boolean constants strings
• quantor strings
• Strings of binary ops
• some stuff for Isabelle
• some stuff for HasCASL
• strings for HOLCF lifting functions
• Predefined CLASSES
• predefined SORTS
• predefined types
• predefinded HOLCF types
• term construction
• binary junctors
• terms for HOL-HOLCF
• Boolean constants
• UNTYPED terms
• HOLCF
• constant names
• VNames of binary operators
• keywords in theory files from the Isar Reference Manual 2005

Description

Synopsis

• topSort :: (a -> a -> Bool) -> [a] -> [a]
• liftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
• getTypeIds :: Typ -> Set TName
• deDepOn :: DomainEntry -> DomainEntry -> Bool
• ordDoms :: DomainTab -> DomainTab
• cTrue :: String
• cFalse :: String
• cNot :: String
• allS :: String
• ex1S :: String
• exS :: String
• conj :: String
• disj :: String
• impl :: String
• eq :: String
• neq :: String
• plusS :: String
• minusS :: String
• timesS :: String
• divS :: String
• modS :: String
• consS :: String
• lconsS :: String
• appendS :: String
• compS :: String
• pairC :: String
• eqvSimS :: String
• unionS :: String
• membershipS :: String
• imageS :: String
• rangeS :: String
• pcpoS :: String
• prodS :: TName
• lSumS :: TName
• lProdS :: TName
• sSumS :: TName
• lFunS :: TName
• cFunS :: TName
• funS :: TName
• sProdS :: TName
• aptS :: String
• appS :: String
• pAppS :: String
• defOpS :: String
• someS :: String
• lliftbinS :: String
• fliftbinS :: String
• flift2S :: String
• pcpo :: IsaClass
• isaTerm :: IsaClass
• holType :: Sort
• dom :: Sort
• sortT :: Continuity -> Sort
• mkSTypeT :: Continuity -> String -> Typ
• listT :: Continuity -> Typ -> Typ
• charT :: Continuity -> Typ
• ratT :: Continuity -> Typ
• fracT :: Continuity -> Typ
• integerT :: Continuity -> Typ
• boolT :: Continuity -> Typ
• orderingT :: Continuity -> Typ
• intT :: Continuity -> Typ
• prodT :: Continuity -> Typ -> Typ -> Typ
• funT :: Continuity -> Typ -> Typ -> Typ
• curryFunT :: Continuity -> [Typ] -> Typ -> Typ
• mkSType :: String -> Typ
• noTypeT :: Typ
• noType :: DTyp
• noTypeC :: DTyp
• hideNN :: Typ -> DTyp
• hideCN :: Typ -> DTyp
• dispNN :: Typ -> DTyp
• dispMN :: Typ -> DTyp
• boolType :: Typ
• mkListType :: Typ -> Typ
• mkOptionType :: Typ -> Typ
• prodType :: Typ -> Typ -> Typ
• mkFunType :: Typ -> Typ -> Typ
• mkCurryFunType :: [Typ] -> Typ -> Typ
• mkSDomType :: String -> Typ
• voidDom :: Typ
• flatDom :: Typ
• tLift :: Typ -> Typ
• mkBinDomType :: String -> Typ -> Typ -> Typ
• mkContFun :: Typ -> Typ -> Typ
• mkStrictProduct :: Typ -> Typ -> Typ
• mkContProduct :: Typ -> Typ -> Typ
• mkCurryContFun :: [Typ] -> Typ -> Typ
• mkStrictSum :: Typ -> Typ -> Typ
• maxPrio :: Int
• lowPrio :: Int
• isaEqPrio :: Int
• mkConstVD :: String -> Typ -> Term
• mkConstV :: String -> DTyp -> Term
• mkConstD :: VName -> Typ -> Term
• mkConst :: VName -> DTyp -> Term
• mkFree :: String -> Term
• con :: VName -> Term
• conC :: VName -> Term
• conDouble :: String -> Term
• conDoubleC :: String -> Term
• binVNameAppl :: VName -> Term -> Term -> Term
• binConj :: Term -> Term -> Term
• binImageOp :: Term -> Term -> Term
• binMembership :: Term -> Term -> Term
• binUnion :: Term -> Term -> Term
• binEqvSim :: Term -> Term -> Term
• binEq :: Term -> Term -> Term
• binEqv :: Term -> Term -> Term
• binImpl :: Term -> Term -> Term
• binDisj :: Term -> Term -> Term
• rangeOp :: Term -> Term
• termAppl :: Term -> Term -> Term
• andPT :: Continuity -> Term
• orPT :: Continuity -> Term
• notPT :: Continuity -> Term
• bottomPT :: Continuity -> Term
• nilPT :: Continuity -> Term
• consPT :: Continuity -> Term
• truePT :: Continuity -> Term
• falsePT :: Continuity -> Term
• headPT :: Continuity -> Term
• tailPT :: Continuity -> Term
• unitPT :: Continuity -> Term
• fstPT :: Continuity -> Term
• sndPT :: Continuity -> Term
• pairPT :: Continuity -> Term
• nothingPT :: Continuity -> Term
• justPT :: Continuity -> Term
• leftPT :: Continuity -> Term
• rightPT :: Continuity -> Term
• compPT :: Term
• eqPT :: Term
• neqPT :: Term
• eqTPT :: Typ -> Term
• neqTPT :: Typ -> Term
• true :: Term
• false :: Term
• defOp :: Term
• notOp :: Term
• conSome :: Term
• liftString :: Term
• lpairTerm :: Term
• notV :: VName
• conjV :: VName
• disjV :: VName
• implV :: VName
• eqV :: VName
• neqV :: VName
• plusV :: VName
• minusV :: VName
• divV :: VName
• modV :: VName
• timesV :: VName
• consV :: VName
• lconsV :: VName
• appendV :: VName
• compV :: VName
• eqvSimV :: VName
• unionV :: VName
• membershipV :: VName
• imageV :: VName
• rangeV :: VName
• vMap' :: Map String VName
• vMap :: Map String VName
• endS :: String
• headerS :: String
• theoryS :: String
• importsS :: String
• usesS :: String
• beginS :: String
• contextS :: String
• axiomsS :: String
• axiomatizationS :: String
• defsS :: String
• oopsS :: String
• mlS :: String
• mlFileS :: String
• andS :: String
• lemmasS :: String
• lemmaS :: String
• corollaryS :: String
• refuteS :: String
• theoremsS :: String
• theoremS :: String
• axclassS :: String
• classesS :: String
• definitionS :: String
• instanceS :: String
• instantiationS :: String
• typedeclS :: String
• typesS :: String
• constsS :: String
• structureS :: String
• constdefsS :: String
• domainS :: String
• datatypeS :: String
• fixrecS :: String
• primrecS :: String
• declareS :: String
• simpS :: String
• applyS :: String
• backS :: String
• deferS :: String
• preferS :: String
• byS :: String
• doneS :: String
• sorryS :: String
• autoS :: String
• inductS :: String
• caseTacS :: String
• insertS :: String
• subgoalTacS :: String
• typedefS :: String
• premiseOpenS :: String
• premiseCloseS :: String
• metaImplS :: String
• usingS :: String
• whereS :: String
• dotDot :: String
• barS :: String
• markups :: [String]
• ignoredKeys :: [String]
• usedTopKeys :: [String]
• isaKeywords :: [String]
• mkVName :: String -> VName

Documentation

boolean constants strings

quantor strings

Strings of binary ops

some stuff for Isabelle

some stuff for HasCASL

strings for HOLCF lifting functions

Predefined CLASSES

predefined SORTS

predefined types

predefinded HOLCF types

term construction

binary junctors

terms for HOL-HOLCF

Boolean constants

UNTYPED terms

HOLCF

constant names

VNames of binary operators

keywords in theory files from the Isar Reference Manual 2005