etc/isar-keywords.el
author wenzelm
Fri Sep 28 16:15:26 2001 +0200 (2001-09-28)
changeset 11618 7067101463c0
parent 11538 f8588786cc9c
child 11661 37cfa9aad9c0
permissions -rw-r--r--
updated;
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
     4 ;;
     5 ;; $Id$
     6 ;;
     7 
     8 (defconst isar-keywords-major
     9   '("\\."
    10     "\\.\\."
    11     "ML"
    12     "ML_command"
    13     "ML_setup"
    14     "ProofGeneral\\.context_thy_only"
    15     "ProofGeneral\\.inform_file_processed"
    16     "ProofGeneral\\.inform_file_retracted"
    17     "ProofGeneral\\.kill_proof"
    18     "ProofGeneral\\.restart"
    19     "ProofGeneral\\.try_context_thy_only"
    20     "ProofGeneral\\.undo"
    21     "also"
    22     "apply"
    23     "apply_end"
    24     "arities"
    25     "assume"
    26     "automaton"
    27     "axclass"
    28     "axioms"
    29     "back"
    30     "by"
    31     "cannot_undo"
    32     "case"
    33     "cd"
    34     "chapter"
    35     "classes"
    36     "classrel"
    37     "clear_undos"
    38     "coinductive"
    39     "commit"
    40     "constdefs"
    41     "consts"
    42     "consts_code"
    43     "context"
    44     "datatype"
    45     "declare"
    46     "def"
    47     "defaultsort"
    48     "defer"
    49     "defer_recdef"
    50     "defs"
    51     "disable_pr"
    52     "done"
    53     "enable_pr"
    54     "end"
    55     "exit"
    56     "finally"
    57     "fix"
    58     "from"
    59     "full_prf"
    60     "generate_code"
    61     "global"
    62     "have"
    63     "header"
    64     "hence"
    65     "hide"
    66     "inductive"
    67     "inductive_cases"
    68     "init_toplevel"
    69     "instance"
    70     "judgment"
    71     "kill"
    72     "kill_thy"
    73     "lemma"
    74     "lemmas"
    75     "let"
    76     "local"
    77     "method_setup"
    78     "moreover"
    79     "next"
    80     "nonterminals"
    81     "note"
    82     "obtain"
    83     "oops"
    84     "oracle"
    85     "parse_ast_translation"
    86     "parse_translation"
    87     "pr"
    88     "prefer"
    89     "presume"
    90     "pretty_setmargin"
    91     "prf"
    92     "primrec"
    93     "print_antiquotations"
    94     "print_ast_translation"
    95     "print_attributes"
    96     "print_binds"
    97     "print_cases"
    98     "print_claset"
    99     "print_commands"
   100     "print_context"
   101     "print_facts"
   102     "print_methods"
   103     "print_simpset"
   104     "print_syntax"
   105     "print_theorems"
   106     "print_theory"
   107     "print_trans_rules"
   108     "print_translation"
   109     "proof"
   110     "prop"
   111     "pwd"
   112     "qed"
   113     "quit"
   114     "recdef"
   115     "recdef_tc"
   116     "record"
   117     "redo"
   118     "remove_thy"
   119     "rep_datatype"
   120     "sect"
   121     "section"
   122     "setup"
   123     "show"
   124     "sorry"
   125     "subsect"
   126     "subsection"
   127     "subsubsect"
   128     "subsubsection"
   129     "syntax"
   130     "term"
   131     "text"
   132     "text_raw"
   133     "then"
   134     "theorem"
   135     "theorems"
   136     "theory"
   137     "thm"
   138     "thm_deps"
   139     "thms_containing"
   140     "thus"
   141     "token_translation"
   142     "touch_all_thys"
   143     "touch_child_thys"
   144     "touch_thy"
   145     "translations"
   146     "txt"
   147     "txt_raw"
   148     "typ"
   149     "typed_print_translation"
   150     "typedecl"
   151     "typedef"
   152     "types"
   153     "types_code"
   154     "ultimately"
   155     "undo"
   156     "undos_proof"
   157     "update_thy"
   158     "update_thy_only"
   159     "use"
   160     "use_thy"
   161     "use_thy_only"
   162     "welcome"
   163     "with"
   164     "{"
   165     "}"))
   166 
   167 (defconst isar-keywords-minor
   168   '("actions"
   169     "and"
   170     "binder"
   171     "compose"
   172     "con_defs"
   173     "concl"
   174     "congs"
   175     "distinct"
   176     "files"
   177     "hide_action"
   178     "hints"
   179     "in"
   180     "induction"
   181     "infixl"
   182     "infixr"
   183     "initially"
   184     "inject"
   185     "inputs"
   186     "internals"
   187     "intros"
   188     "is"
   189     "monos"
   190     "output"
   191     "outputs"
   192     "overloaded"
   193     "permissive"
   194     "post"
   195     "pre"
   196     "rename"
   197     "restrict"
   198     "signature"
   199     "states"
   200     "to"
   201     "transitions"
   202     "transrel"
   203     "using"
   204     "where"))
   205 
   206 (defconst isar-keywords-control
   207   '("ProofGeneral\\.context_thy_only"
   208     "ProofGeneral\\.inform_file_processed"
   209     "ProofGeneral\\.inform_file_retracted"
   210     "ProofGeneral\\.kill_proof"
   211     "ProofGeneral\\.restart"
   212     "ProofGeneral\\.try_context_thy_only"
   213     "ProofGeneral\\.undo"
   214     "cannot_undo"
   215     "clear_undos"
   216     "exit"
   217     "init_toplevel"
   218     "kill"
   219     "quit"
   220     "redo"
   221     "undo"
   222     "undos_proof"))
   223 
   224 (defconst isar-keywords-diag
   225   '("ML"
   226     "ML_command"
   227     "cd"
   228     "commit"
   229     "disable_pr"
   230     "enable_pr"
   231     "full_prf"
   232     "header"
   233     "kill_thy"
   234     "pr"
   235     "pretty_setmargin"
   236     "prf"
   237     "print_antiquotations"
   238     "print_attributes"
   239     "print_binds"
   240     "print_cases"
   241     "print_claset"
   242     "print_commands"
   243     "print_context"
   244     "print_facts"
   245     "print_methods"
   246     "print_simpset"
   247     "print_syntax"
   248     "print_theorems"
   249     "print_theory"
   250     "print_trans_rules"
   251     "prop"
   252     "pwd"
   253     "remove_thy"
   254     "term"
   255     "thm"
   256     "thm_deps"
   257     "thms_containing"
   258     "touch_all_thys"
   259     "touch_child_thys"
   260     "touch_thy"
   261     "typ"
   262     "update_thy"
   263     "update_thy_only"
   264     "use"
   265     "use_thy"
   266     "use_thy_only"
   267     "welcome"))
   268 
   269 (defconst isar-keywords-theory-begin
   270   '("theory"))
   271 
   272 (defconst isar-keywords-theory-switch
   273   '("context"))
   274 
   275 (defconst isar-keywords-theory-end
   276   '("end"))
   277 
   278 (defconst isar-keywords-theory-heading
   279   '("chapter"
   280     "section"
   281     "subsection"
   282     "subsubsection"))
   283 
   284 (defconst isar-keywords-theory-decl
   285   '("ML_setup"
   286     "arities"
   287     "automaton"
   288     "axclass"
   289     "axioms"
   290     "classes"
   291     "classrel"
   292     "coinductive"
   293     "constdefs"
   294     "consts"
   295     "consts_code"
   296     "datatype"
   297     "defaultsort"
   298     "defer_recdef"
   299     "defs"
   300     "generate_code"
   301     "global"
   302     "hide"
   303     "inductive"
   304     "judgment"
   305     "lemmas"
   306     "local"
   307     "method_setup"
   308     "nonterminals"
   309     "oracle"
   310     "parse_ast_translation"
   311     "parse_translation"
   312     "primrec"
   313     "print_ast_translation"
   314     "print_translation"
   315     "recdef"
   316     "record"
   317     "rep_datatype"
   318     "setup"
   319     "syntax"
   320     "text"
   321     "text_raw"
   322     "theorems"
   323     "token_translation"
   324     "translations"
   325     "typed_print_translation"
   326     "typedecl"
   327     "types"
   328     "types_code"))
   329 
   330 (defconst isar-keywords-theory-script
   331   '("declare"
   332     "inductive_cases"))
   333 
   334 (defconst isar-keywords-theory-goal
   335   '("instance"
   336     "lemma"
   337     "recdef_tc"
   338     "theorem"
   339     "typedef"))
   340 
   341 (defconst isar-keywords-qed
   342   '("\\."
   343     "\\.\\."
   344     "by"
   345     "done"
   346     "sorry"))
   347 
   348 (defconst isar-keywords-qed-block
   349   '("qed"))
   350 
   351 (defconst isar-keywords-qed-global
   352   '("oops"))
   353 
   354 (defconst isar-keywords-proof-heading
   355   '("sect"
   356     "subsect"
   357     "subsubsect"))
   358 
   359 (defconst isar-keywords-proof-goal
   360   '("have"
   361     "hence"
   362     "show"
   363     "thus"))
   364 
   365 (defconst isar-keywords-proof-block
   366   '("next"
   367     "proof"))
   368 
   369 (defconst isar-keywords-proof-open
   370   '("{"))
   371 
   372 (defconst isar-keywords-proof-close
   373   '("}"))
   374 
   375 (defconst isar-keywords-proof-chain
   376   '("finally"
   377     "from"
   378     "then"
   379     "ultimately"
   380     "with"))
   381 
   382 (defconst isar-keywords-proof-decl
   383   '("also"
   384     "let"
   385     "moreover"
   386     "note"
   387     "txt"
   388     "txt_raw"))
   389 
   390 (defconst isar-keywords-proof-asm
   391   '("assume"
   392     "case"
   393     "def"
   394     "fix"
   395     "presume"))
   396 
   397 (defconst isar-keywords-proof-asm-goal
   398   '("obtain"))
   399 
   400 (defconst isar-keywords-proof-script
   401   '("apply"
   402     "apply_end"
   403     "back"
   404     "defer"
   405     "prefer"))
   406 
   407 (provide 'isar-keywords)