IsaConsts.hs revision cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2006
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
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorrinihskClass :: IsaClass
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorrinihskClass = IsaClass "hskTerm"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm :: IsaClass
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm = IsaClass "type"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS = "pcpo"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederpcpo :: IsaClass
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederpcpo = IsaClass pcpoS
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniholType :: Sort
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniholType = [isaTerm]
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
81eaac399d69af15425d06b054e5d0331dbc132bChristian MaedertermAppl t1 t2 = App 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
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder-- * some stuff for HasCASL
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Some string
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS = "Some"
f1082bc15d1cbd06522cf49842929d73ba4214fcChristian Maeder-- | some constant
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSome :: Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconSome = conDouble someS
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederaptS :: String
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederappS :: String
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederpAppS :: String
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederpAppS = "pApp"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederdefOpS :: String
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederdefOpS = "defOp"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederfliftbinS :: String
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederfliftbinS = "fliftbin"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | defOp constant
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederdefOp = conDouble defOpS
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"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompS :: String
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompS = "comp"
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederplusV :: VName
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian 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
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV :: VName
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV = VName compS $ Just $ AltSyntax "(_ o/ _)" [55, 56] 55
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | apply VName operator to two term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederbinVNameAppl :: VName -> Term -> Term -> Term
81eaac399d69af15425d06b054e5d0331dbc132bChristian MaederbinVNameAppl v t1 t2 = termAppl (termAppl (con v) t1) t2
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
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian 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-- * 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"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureS :: String
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureS = "structure"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederconstdefsS :: String
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederconstdefsS = "constdefs"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS = "domain"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS = "datatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS = "fixrec"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS = "primrec"
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian MaederdeclareS :: String
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian MaederdeclareS = "declare"
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]
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder [ domainS, oopsS, refuteS, fixrecS, primrecS, declareS
e96fb97935ac710a295b04d60b8ac90ef8364079Christian Maeder , "sorry", "done", "by", "proof", "apply", "qed"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "classrel", "defaultsort", "nonterminls", "arities"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder , "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", "-"
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder , "let", "is", "next", "apply_end", "defer", "prefer", "back"
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
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder , constdefsS, lemmasS, theoremsS, lemmaS, corollaryS, theoremS, datatypeS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , classesS, axclassS, instanceS, typesS, typedeclS, endS ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | all Isabelle keywords
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords :: [String]
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian MaederisaKeywords = "::" : andS : theoryS : map (:[]) ":=<|"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ usedTopKeys ++ ignoredKeys