etc/isar-keywords.el
changeset 23732 f9f89b7cfdc7
parent 22864 e2511e6e5cbb
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"
    97     "header"
    97     "header"
    98     "help"
    98     "help"
    99     "hence"
    99     "hence"
   100     "hide"
   100     "hide"
   101     "inductive"
   101     "inductive"
   102     "inductive2"
       
   103     "inductive_cases"
   102     "inductive_cases"
   104     "inductive_cases2"
   103     "inductive_set"
   105     "init_toplevel"
   104     "init_toplevel"
   106     "instance"
   105     "instance"
   107     "interpret"
   106     "interpret"
   108     "interpretation"
   107     "interpretation"
   109     "invoke"
   108     "invoke"
   264     "infixr"
   263     "infixr"
   265     "initially"
   264     "initially"
   266     "inject"
   265     "inject"
   267     "inputs"
   266     "inputs"
   268     "internals"
   267     "internals"
   269     "intros"
       
   270     "is"
   268     "is"
   271     "lazy"
   269     "lazy"
   272     "monos"
   270     "monos"
   273     "morphisms"
   271     "morphisms"
   274     "notes"
   272     "notes"
   416     "code_moduleprolog"
   414     "code_moduleprolog"
   417     "code_monad"
   415     "code_monad"
   418     "code_reserved"
   416     "code_reserved"
   419     "code_type"
   417     "code_type"
   420     "coinductive"
   418     "coinductive"
   421     "coinductive2"
   419     "coinductive_set"
   422     "constdefs"
   420     "constdefs"
   423     "consts"
   421     "consts"
   424     "consts_code"
   422     "consts_code"
   425     "context"
   423     "context"
   426     "datatype"
   424     "datatype"
   437     "fixrec"
   435     "fixrec"
   438     "fun"
   436     "fun"
   439     "global"
   437     "global"
   440     "hide"
   438     "hide"
   441     "inductive"
   439     "inductive"
   442     "inductive2"
   440     "inductive_set"
   443     "judgment"
   441     "judgment"
   444     "lemmas"
   442     "lemmas"
   445     "local"
   443     "local"
   446     "locale"
   444     "locale"
   447     "method_setup"
   445     "method_setup"
   475     "types"
   473     "types"
   476     "types_code"))
   474     "types_code"))
   477 
   475 
   478 (defconst isar-keywords-theory-script
   476 (defconst isar-keywords-theory-script
   479   '("declare"
   477   '("declare"
   480     "inductive_cases"
   478     "inductive_cases"))
   481     "inductive_cases2"))
       
   482 
   479 
   483 (defconst isar-keywords-theory-goal
   480 (defconst isar-keywords-theory-goal
   484   '("ax_specification"
   481   '("ax_specification"
   485     "corollary"
   482     "corollary"
   486     "cpodef"
   483     "cpodef"