etc/isar-keywords.el
changeset 18888 3b643f81b378
parent 18775 becdbf57eeb8
child 19069 a4b956f8b233
equal deleted inserted replaced
18887:6ad81e3fa478 18888:3b643f81b378
    36     "cannot_undo"
    36     "cannot_undo"
    37     "case"
    37     "case"
    38     "cd"
    38     "cd"
    39     "chapter"
    39     "chapter"
    40     "class"
    40     "class"
    41     "class_instance"
       
    42     "classes"
    41     "classes"
    43     "classrel"
    42     "classrel"
    44     "clear_undos"
    43     "clear_undos"
    45     "code_alias"
    44     "code_alias"
    46     "code_class"
       
    47     "code_generate"
    45     "code_generate"
    48     "code_library"
    46     "code_library"
    49     "code_module"
    47     "code_module"
    50     "code_primclass"
    48     "code_primclass"
    51     "code_primconst"
    49     "code_primconst"
   228     "contains"
   226     "contains"
   229     "defines"
   227     "defines"
   230     "depending_on"
   228     "depending_on"
   231     "distinct"
   229     "distinct"
   232     "file"
   230     "file"
   233     "files"
       
   234     "fixes"
   231     "fixes"
   235     "hide_action"
   232     "hide_action"
   236     "hints"
   233     "hints"
   237     "imports"
   234     "imports"
   238     "in"
   235     "in"
   249     "is"
   246     "is"
   250     "lazy"
   247     "lazy"
   251     "monos"
   248     "monos"
   252     "morphisms"
   249     "morphisms"
   253     "notes"
   250     "notes"
       
   251     "obtains"
   254     "open"
   252     "open"
   255     "output"
   253     "output"
   256     "outputs"
   254     "outputs"
   257     "overloaded"
   255     "overloaded"
   258     "permissive"
   256     "permissive"
   371     "axioms"
   369     "axioms"
   372     "class"
   370     "class"
   373     "classes"
   371     "classes"
   374     "classrel"
   372     "classrel"
   375     "code_alias"
   373     "code_alias"
   376     "code_class"
       
   377     "code_generate"
   374     "code_generate"
   378     "code_library"
   375     "code_library"
   379     "code_module"
   376     "code_module"
   380     "code_primclass"
   377     "code_primclass"
   381     "code_primconst"
   378     "code_primconst"
   437   '("declare"
   434   '("declare"
   438     "inductive_cases"))
   435     "inductive_cases"))
   439 
   436 
   440 (defconst isar-keywords-theory-goal
   437 (defconst isar-keywords-theory-goal
   441   '("ax_specification"
   438   '("ax_specification"
   442     "class_instance"
       
   443     "corollary"
   439     "corollary"
   444     "cpodef"
   440     "cpodef"
   445     "instance"
   441     "instance"
   446     "interpretation"
   442     "interpretation"
   447     "lemma"
   443     "lemma"