IsaConsts.hs revision 99c923311eab71a85f1dcc4785d349609c828da4
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederconstants for Isabelle
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- possibly differentiate between HOL and HOLCF
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * predefined sorts
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederholType :: Sort
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederholType = [IsaClass "hol_type"]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm :: IsaClass
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm = IsaClass "type"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS = "pcpo"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederpcpo :: IsaClass
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederpcpo = IsaClass pcpoS
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * predefinded types
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedernoType = Type "dummy" holType []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederboolType :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederboolType = Type "bool" holType []
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaederintType :: Typ
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaederintType = Type "int" holType []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType :: Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType t = Type "option" holType [t]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodType :: Typ -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodType t1 t2 = Type prodS holType [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFunType :: Typ -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFunType s t = Type funS holType [s,t] -- was "-->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType = flip $ foldr mkFunType -- was "--->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom = Type "void" dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- should this be included (as primitive)? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom = Type "flat" dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- sort is ok? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContFun :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkContFun t1 t2 = Type cFunS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictProduct :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkStrictProduct t1 t2 = Type sProdS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContProduct :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkContProduct t1 t2 = Type prodS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryContFun :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryContFun = flip $ foldr mkContFun -- was "--->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictSum :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkStrictSum t1 t2 = Type sSumS dom [t1,t2]
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaederprodS, sProdS, funS, cFunS, sSumS :: TName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodS = "*" -- this is printed as it is!
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * functions for term formation
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio = 1000
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederlowPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio = 2 -- left assoc
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | function application
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertermAppl :: Term -> Term -> Term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedertermAppl t1 t2 = MixfixApp t1 [t2] NotCont
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | function application to a list of arguments
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedertermMixfixAppl :: Term -> [Term] -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedertermMixfixAppl t1 t2 = MixfixApp t1 t2 NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | apply binary operation to arguments
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConst :: String -> Term -> Term -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederbinConst s t1 t2 = MixfixApp (conDouble s) [t1,t2] NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant with no type
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedercon :: VName -> Term
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinicon s = Const s noType
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble :: String -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble = con . mkVName
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Some string
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS = "Some"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Some term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSomeT :: Typ -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconSomeT t = Const (mkVName someS) t
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | some constant with no type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSome :: Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconSome = conDouble someS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | defOp constant
c36dc42a63287db1e3e81b03ee5655aed69e7cdeChristian MaederdefOp = conDouble "defOp"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Not string
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercNot :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Not VName
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedernotV = VName cNot $ Just $ AltSyntax "~/ _" [40] 40
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Not constant
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedernotOp = con notV
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * quantor strings
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederallS, exS, ex1S :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- * Strings and VNames of binary ops
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconj :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdisj :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimpl :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimpl = "op -->"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconjV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconjV = VName conj $ Just $ AltSyntax "(_ &/ _)" [36, 35] 35
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdisjV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdisjV = VName disj $ Just $ AltSyntax "(_ |/ _)" [31, 30] 30
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV = VName impl $ Just $ AltSyntax "(_ -->/ _)" [26, 25] 25
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedereqV = VName eq $ Just $ AltSyntax "(_ =/ _)" [50, 51] 50
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusS = "op +"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusS = "op -"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesS = "op *"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsS = "Cons"
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederplusV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusV = VName plusS $ Just $ AltSyntax "(_ +/ _)" [65, 66] 65
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederminusV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusV = VName minusS $ Just $ AltSyntax "(_ -/ _)" [65, 66] 65
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertimesV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesV = VName timesS $ Just $ AltSyntax "(_ */ _)" [70, 71] 70
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV = VName consS $ Just $ AltSyntax "(_ #/ _)" [66, 65] 65
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | apply VName operator to two term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederbinVNameAppl :: VName -> Term -> Term -> Term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederbinVNameAppl v t1 t2 = MixfixApp (con v) [t1,t2] NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * binary junctors
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinConj = binVNameAppl conjV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinDisj = binVNameAppl disjV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinImpl = binVNameAppl implV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinEq = binVNameAppl eqV
613bf0ed7d98a961755408ead328687ec17f74fdChristian MaederbinEqv = binEq
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * boolean constants
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercTrue :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercTrue = "True"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercFalse :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercFalse = "False"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maedertrue = Const (mkVName cTrue) boolType
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederfalse = Const (mkVName cFalse) boolType
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | lower case pair
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC = "pair"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | upper case pair
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair = "Pair"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- * keywords in theory files from the Isar Reference Manual 2005
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederendS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederheaderS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederheaderS = "header"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoryS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoryS = "theory"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederimportsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederimportsS = "imports"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusesS = "uses"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbeginS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbeginS = "begin"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercontextS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercontextS = "context"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxiomsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxiomsS = "axioms"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdefsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdefsS = "defs"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederoopsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederoopsS = "oops"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederandS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmasS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmasS = "lemmas"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmaS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmaS = "lemma"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercorollaryS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercorollaryS = "corollary"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrefuteS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrefuteS = "refute"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremsS = "theorems"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremS = "theorem"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxclassS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxclassS = "axclass"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederclassesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederclassesS = "classes"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS = "instance"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypedeclS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypedeclS = "typedecl"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypesS = "types"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederconstsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederconstsS = "consts"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS = "domain"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS = "datatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS = "fixrec"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS = "primrec"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedersimpS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedersimpS = "simp"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maedermarkups :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "--", "chapter" , "section", "subsection", "subsubsection", "text"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "text_raw", "sect", "subsect", "subsubsect", "txt", "txt_raw"]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | toplevel keys that are currently ignored
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederignoredKeys :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ datatypeS, domainS, oopsS, refuteS, fixrecS, primrecS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "sorry", "done", "by", "proofs", "apply", "qed"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "classrel", "defaultsort", "nonterminls", "arities"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "constdefs", "syntax", "no_syntax", "translations"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "global", "local", "hide", "use", "setup", "method_setup"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "ML_command", "ML_setup", "oracle"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "fix", "assume", "presume", "def", "note", "then", "from", "with"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "using", "have", "show", "hence", "thus", "shows", ".", ".."
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- , "rule", "iprover","OF", "of", "where", "assumption", "this", "-"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "let", "is", "next", "apply_end", "defer", "prefer", "back", "declare"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "pr", "thm", "prf", "term", "prop", "typ", "full_prf"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "undo", "redo", "kill", "thms_containing", "thms_deps"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "cd", "pwd", "use_thy", "use_thy_only", "update_thy", "update_thy_only"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "display_drafts", "in", "locale" -- "intro_classes"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "fixes", "constrains", "assumes", "defines", "notes", "includes"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "interpretation", "interpret", "obtain", "also", "finally"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "moreover", "ultimately" -- "trans", "sym", "symmetric"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "case", "judgment", "typedef", "morphisms", "record", "rep_datatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "recdef", "recdef_tc", "specification","ax_specification"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "inductive", "coinductive", "inductive_cases", "codatatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "code_module", "code_library", "consts_code", "types_code" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ map (++ "_translation")
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "parse_ast", "parse", "print", "print_ast", "typed_print", "token" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ map ("print_" ++)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "commands", "syntax", "methods", "attributes", "theorems", "tcset"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "facts", "binds", "drafts", "locale", "locales", "interps"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "trans_rules", "simp_set", "claset", "cases", "induct_rules" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | toplevel keywords currently recognized by IsaParse
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusedTopKeys :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusedTopKeys = markups ++
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ importsS, usesS, beginS, contextS, mlS, axiomsS, defsS, constsS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , lemmasS, theoremsS, lemmaS, corollaryS, theoremS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , classesS, axclassS, instanceS, typesS, typedeclS, endS ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | all Isabelle keywords
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords = "::" : andS : theoryS : map (:[]) ":=<"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ usedTopKeys ++ ignoredKeys