etc/isar-keywords-HOL-Nominal.el
changeset 23804 5801141870b1
parent 23732 f9f89b7cfdc7
child 23992 bf352c4c499b
equal deleted inserted replaced
23803:11bf7af10ec8 23804:5801141870b1
   407     "consts"
   407     "consts"
   408     "consts_code"
   408     "consts_code"
   409     "context"
   409     "context"
   410     "datatype"
   410     "datatype"
   411     "declaration"
   411     "declaration"
       
   412     "declare"
   412     "defaultsort"
   413     "defaultsort"
   413     "defer_recdef"
   414     "defer_recdef"
   414     "definition"
   415     "definition"
   415     "defs"
   416     "defs"
   416     "equivariance"
   417     "equivariance"
   457     "typedecl"
   458     "typedecl"
   458     "types"
   459     "types"
   459     "types_code"))
   460     "types_code"))
   460 
   461 
   461 (defconst isar-keywords-theory-script
   462 (defconst isar-keywords-theory-script
   462   '("declare"
   463   '("inductive_cases"))
   463     "inductive_cases"))
       
   464 
   464 
   465 (defconst isar-keywords-theory-goal
   465 (defconst isar-keywords-theory-goal
   466   '("ax_specification"
   466   '("ax_specification"
   467     "corollary"
   467     "corollary"
   468     "function"
   468     "function"