etc/isar-keywords-HOL-Nominal.el
changeset 23732 f9f89b7cfdc7
parent 23692 b784849811fc
child 23804 5801141870b1
equal deleted inserted replaced
23731:e42f71809a7a 23732:f9f89b7cfdc7
    53     "code_monad"
    53     "code_monad"
    54     "code_reserved"
    54     "code_reserved"
    55     "code_thms"
    55     "code_thms"
    56     "code_type"
    56     "code_type"
    57     "coinductive"
    57     "coinductive"
    58     "coinductive2"
    58     "coinductive_set"
    59     "commit"
    59     "commit"
    60     "constdefs"
    60     "constdefs"
    61     "consts"
    61     "consts"
    62     "consts_code"
    62     "consts_code"
    63     "context"
    63     "context"
    94     "header"
    94     "header"
    95     "help"
    95     "help"
    96     "hence"
    96     "hence"
    97     "hide"
    97     "hide"
    98     "inductive"
    98     "inductive"
    99     "inductive2"
       
   100     "inductive_cases"
    99     "inductive_cases"
   101     "inductive_cases2"
   100     "inductive_set"
   102     "init_toplevel"
   101     "init_toplevel"
   103     "instance"
   102     "instance"
   104     "interpret"
   103     "interpret"
   105     "interpretation"
   104     "interpretation"
   106     "invoke"
   105     "invoke"
   259     "induction"
   258     "induction"
   260     "infix"
   259     "infix"
   261     "infixl"
   260     "infixl"
   262     "infixr"
   261     "infixr"
   263     "inject"
   262     "inject"
   264     "intros"
       
   265     "invariant"
   263     "invariant"
   266     "is"
   264     "is"
   267     "monos"
   265     "monos"
   268     "morphisms"
   266     "morphisms"
   269     "notes"
   267     "notes"
   402     "code_moduleprolog"
   400     "code_moduleprolog"
   403     "code_monad"
   401     "code_monad"
   404     "code_reserved"
   402     "code_reserved"
   405     "code_type"
   403     "code_type"
   406     "coinductive"
   404     "coinductive"
   407     "coinductive2"
   405     "coinductive_set"
   408     "constdefs"
   406     "constdefs"
   409     "consts"
   407     "consts"
   410     "consts_code"
   408     "consts_code"
   411     "context"
   409     "context"
   412     "datatype"
   410     "datatype"
   421     "finalconsts"
   419     "finalconsts"
   422     "fun"
   420     "fun"
   423     "global"
   421     "global"
   424     "hide"
   422     "hide"
   425     "inductive"
   423     "inductive"
   426     "inductive2"
   424     "inductive_set"
   427     "judgment"
   425     "judgment"
   428     "lemmas"
   426     "lemmas"
   429     "local"
   427     "local"
   430     "locale"
   428     "locale"
   431     "method_setup"
   429     "method_setup"
   460     "types"
   458     "types"
   461     "types_code"))
   459     "types_code"))
   462 
   460 
   463 (defconst isar-keywords-theory-script
   461 (defconst isar-keywords-theory-script
   464   '("declare"
   462   '("declare"
   465     "inductive_cases"
   463     "inductive_cases"))
   466     "inductive_cases2"))
       
   467 
   464 
   468 (defconst isar-keywords-theory-goal
   465 (defconst isar-keywords-theory-goal
   469   '("ax_specification"
   466   '("ax_specification"
   470     "corollary"
   467     "corollary"
   471     "function"
   468     "function"