etc/isar-keywords.el
changeset 24904 5b59fadfe878
parent 24876 81ed46bc0420
child 24912 52bc004950c4
equal deleted inserted replaced
24903:57a33f4c2c19 24904:5b59fadfe878
     1 ;;
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; This file was generated from HOL + HOLCF + IOA -- DO NOT EDIT!
     3 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal
       
     4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     4 ;;
     5 ;;
     5 ;; $Id$
     6 ;; $Id$
     6 ;;
     7 ;;
     7 
     8 
     8 (defconst isar-keywords-major
     9 (defconst isar-keywords-major
    21     "also"
    22     "also"
    22     "apply"
    23     "apply"
    23     "apply_end"
    24     "apply_end"
    24     "arities"
    25     "arities"
    25     "assume"
    26     "assume"
       
    27     "atom_decl"
    26     "automaton"
    28     "automaton"
    27     "ax_specification"
    29     "ax_specification"
    28     "axclass"
    30     "axclass"
    29     "axiomatization"
    31     "axiomatization"
    30     "axioms"
    32     "axioms"
    75     "display_drafts"
    77     "display_drafts"
    76     "domain"
    78     "domain"
    77     "done"
    79     "done"
    78     "enable_pr"
    80     "enable_pr"
    79     "end"
    81     "end"
       
    82     "equivariance"
    80     "exit"
    83     "exit"
    81     "export_code"
    84     "export_code"
    82     "extract"
    85     "extract"
    83     "extract_type"
    86     "extract_type"
    84     "finalconsts"
    87     "finalconsts"
   119     "method_setup"
   122     "method_setup"
   120     "moreover"
   123     "moreover"
   121     "next"
   124     "next"
   122     "no_syntax"
   125     "no_syntax"
   123     "no_translations"
   126     "no_translations"
       
   127     "nominal_datatype"
       
   128     "nominal_inductive"
       
   129     "nominal_primrec"
   124     "nonterminals"
   130     "nonterminals"
   125     "normal_form"
   131     "normal_form"
   126     "notation"
   132     "notation"
   127     "note"
   133     "note"
   128     "obtain"
   134     "obtain"
   238   '("actions"
   244   '("actions"
   239     "advanced"
   245     "advanced"
   240     "and"
   246     "and"
   241     "assumes"
   247     "assumes"
   242     "attach"
   248     "attach"
       
   249     "avoids"
   243     "begin"
   250     "begin"
   244     "binder"
   251     "binder"
   245     "compose"
   252     "compose"
   246     "concl"
   253     "concl"
   247     "congs"
   254     "congs"
   397 
   404 
   398 (defconst isar-keywords-theory-decl
   405 (defconst isar-keywords-theory-decl
   399   '("ML_setup"
   406   '("ML_setup"
   400     "abbreviation"
   407     "abbreviation"
   401     "arities"
   408     "arities"
       
   409     "atom_decl"
   402     "automaton"
   410     "automaton"
   403     "axclass"
   411     "axclass"
   404     "axiomatization"
   412     "axiomatization"
   405     "axioms"
   413     "axioms"
   406     "class"
   414     "class"
   431     "defaultsort"
   439     "defaultsort"
   432     "defer_recdef"
   440     "defer_recdef"
   433     "definition"
   441     "definition"
   434     "defs"
   442     "defs"
   435     "domain"
   443     "domain"
       
   444     "equivariance"
   436     "extract"
   445     "extract"
   437     "extract_type"
   446     "extract_type"
   438     "finalconsts"
   447     "finalconsts"
   439     "fixpat"
   448     "fixpat"
   440     "fixrec"
   449     "fixrec"
   449     "local"
   458     "local"
   450     "locale"
   459     "locale"
   451     "method_setup"
   460     "method_setup"
   452     "no_syntax"
   461     "no_syntax"
   453     "no_translations"
   462     "no_translations"
       
   463     "nominal_datatype"
   454     "nonterminals"
   464     "nonterminals"
   455     "notation"
   465     "notation"
   456     "oracle"
   466     "oracle"
   457     "parse_ast_translation"
   467     "parse_ast_translation"
   458     "parse_translation"
   468     "parse_translation"
   489     "function"
   499     "function"
   490     "instance"
   500     "instance"
   491     "instance_proof"
   501     "instance_proof"
   492     "interpretation"
   502     "interpretation"
   493     "lemma"
   503     "lemma"
       
   504     "nominal_inductive"
       
   505     "nominal_primrec"
   494     "pcpodef"
   506     "pcpodef"
   495     "recdef_tc"
   507     "recdef_tc"
   496     "specification"
   508     "specification"
   497     "termination"
   509     "termination"
   498     "theorem"
   510     "theorem"