etc/isar-keywords.el
author wenzelm
Thu Oct 04 11:22:10 2001 +0200 (2001-10-04)
changeset 11661 37cfa9aad9c0
parent 11618 7067101463c0
child 11746 9bf11f1de9d6
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_induct_rules"
   103     "print_methods"
   104     "print_simpset"
   105     "print_syntax"
   106     "print_theorems"
   107     "print_theory"
   108     "print_trans_rules"
   109     "print_translation"
   110     "proof"
   111     "prop"
   112     "pwd"
   113     "qed"
   114     "quit"
   115     "recdef"
   116     "recdef_tc"
   117     "record"
   118     "redo"
   119     "remove_thy"
   120     "rep_datatype"
   121     "sect"
   122     "section"
   123     "setup"
   124     "show"
   125     "sorry"
   126     "subsect"
   127     "subsection"
   128     "subsubsect"
   129     "subsubsection"
   130     "syntax"
   131     "term"
   132     "text"
   133     "text_raw"
   134     "then"
   135     "theorem"
   136     "theorems"
   137     "theory"
   138     "thm"
   139     "thm_deps"
   140     "thms_containing"
   141     "thus"
   142     "token_translation"
   143     "touch_all_thys"
   144     "touch_child_thys"
   145     "touch_thy"
   146     "translations"
   147     "txt"
   148     "txt_raw"
   149     "typ"
   150     "typed_print_translation"
   151     "typedecl"
   152     "typedef"
   153     "types"
   154     "types_code"
   155     "ultimately"
   156     "undo"
   157     "undos_proof"
   158     "update_thy"
   159     "update_thy_only"
   160     "use"
   161     "use_thy"
   162     "use_thy_only"
   163     "welcome"
   164     "with"
   165     "{"
   166     "}"))
   167 
   168 (defconst isar-keywords-minor
   169   '("actions"
   170     "and"
   171     "binder"
   172     "compose"
   173     "con_defs"
   174     "concl"
   175     "congs"
   176     "distinct"
   177     "files"
   178     "hide_action"
   179     "hints"
   180     "in"
   181     "induction"
   182     "infix"
   183     "infixl"
   184     "infixr"
   185     "initially"
   186     "inject"
   187     "inputs"
   188     "internals"
   189     "intros"
   190     "is"
   191     "monos"
   192     "output"
   193     "outputs"
   194     "overloaded"
   195     "permissive"
   196     "post"
   197     "pre"
   198     "rename"
   199     "restrict"
   200     "signature"
   201     "states"
   202     "to"
   203     "transitions"
   204     "transrel"
   205     "using"
   206     "where"))
   207 
   208 (defconst isar-keywords-control
   209   '("ProofGeneral\\.context_thy_only"
   210     "ProofGeneral\\.inform_file_processed"
   211     "ProofGeneral\\.inform_file_retracted"
   212     "ProofGeneral\\.kill_proof"
   213     "ProofGeneral\\.restart"
   214     "ProofGeneral\\.try_context_thy_only"
   215     "ProofGeneral\\.undo"
   216     "cannot_undo"
   217     "clear_undos"
   218     "exit"
   219     "init_toplevel"
   220     "kill"
   221     "quit"
   222     "redo"
   223     "undo"
   224     "undos_proof"))
   225 
   226 (defconst isar-keywords-diag
   227   '("ML"
   228     "ML_command"
   229     "cd"
   230     "commit"
   231     "disable_pr"
   232     "enable_pr"
   233     "full_prf"
   234     "header"
   235     "kill_thy"
   236     "pr"
   237     "pretty_setmargin"
   238     "prf"
   239     "print_antiquotations"
   240     "print_attributes"
   241     "print_binds"
   242     "print_cases"
   243     "print_claset"
   244     "print_commands"
   245     "print_context"
   246     "print_facts"
   247     "print_induct_rules"
   248     "print_methods"
   249     "print_simpset"
   250     "print_syntax"
   251     "print_theorems"
   252     "print_theory"
   253     "print_trans_rules"
   254     "prop"
   255     "pwd"
   256     "remove_thy"
   257     "term"
   258     "thm"
   259     "thm_deps"
   260     "thms_containing"
   261     "touch_all_thys"
   262     "touch_child_thys"
   263     "touch_thy"
   264     "typ"
   265     "update_thy"
   266     "update_thy_only"
   267     "use"
   268     "use_thy"
   269     "use_thy_only"
   270     "welcome"))
   271 
   272 (defconst isar-keywords-theory-begin
   273   '("theory"))
   274 
   275 (defconst isar-keywords-theory-switch
   276   '("context"))
   277 
   278 (defconst isar-keywords-theory-end
   279   '("end"))
   280 
   281 (defconst isar-keywords-theory-heading
   282   '("chapter"
   283     "section"
   284     "subsection"
   285     "subsubsection"))
   286 
   287 (defconst isar-keywords-theory-decl
   288   '("ML_setup"
   289     "arities"
   290     "automaton"
   291     "axclass"
   292     "axioms"
   293     "classes"
   294     "classrel"
   295     "coinductive"
   296     "constdefs"
   297     "consts"
   298     "consts_code"
   299     "datatype"
   300     "defaultsort"
   301     "defer_recdef"
   302     "defs"
   303     "generate_code"
   304     "global"
   305     "hide"
   306     "inductive"
   307     "judgment"
   308     "lemmas"
   309     "local"
   310     "method_setup"
   311     "nonterminals"
   312     "oracle"
   313     "parse_ast_translation"
   314     "parse_translation"
   315     "primrec"
   316     "print_ast_translation"
   317     "print_translation"
   318     "recdef"
   319     "record"
   320     "rep_datatype"
   321     "setup"
   322     "syntax"
   323     "text"
   324     "text_raw"
   325     "theorems"
   326     "token_translation"
   327     "translations"
   328     "typed_print_translation"
   329     "typedecl"
   330     "types"
   331     "types_code"))
   332 
   333 (defconst isar-keywords-theory-script
   334   '("declare"
   335     "inductive_cases"))
   336 
   337 (defconst isar-keywords-theory-goal
   338   '("instance"
   339     "lemma"
   340     "recdef_tc"
   341     "theorem"
   342     "typedef"))
   343 
   344 (defconst isar-keywords-qed
   345   '("\\."
   346     "\\.\\."
   347     "by"
   348     "done"
   349     "sorry"))
   350 
   351 (defconst isar-keywords-qed-block
   352   '("qed"))
   353 
   354 (defconst isar-keywords-qed-global
   355   '("oops"))
   356 
   357 (defconst isar-keywords-proof-heading
   358   '("sect"
   359     "subsect"
   360     "subsubsect"))
   361 
   362 (defconst isar-keywords-proof-goal
   363   '("have"
   364     "hence"
   365     "show"
   366     "thus"))
   367 
   368 (defconst isar-keywords-proof-block
   369   '("next"
   370     "proof"))
   371 
   372 (defconst isar-keywords-proof-open
   373   '("{"))
   374 
   375 (defconst isar-keywords-proof-close
   376   '("}"))
   377 
   378 (defconst isar-keywords-proof-chain
   379   '("finally"
   380     "from"
   381     "then"
   382     "ultimately"
   383     "with"))
   384 
   385 (defconst isar-keywords-proof-decl
   386   '("also"
   387     "let"
   388     "moreover"
   389     "note"
   390     "txt"
   391     "txt_raw"))
   392 
   393 (defconst isar-keywords-proof-asm
   394   '("assume"
   395     "case"
   396     "def"
   397     "fix"
   398     "presume"))
   399 
   400 (defconst isar-keywords-proof-asm-goal
   401   '("obtain"))
   402 
   403 (defconst isar-keywords-proof-script
   404   '("apply"
   405     "apply_end"
   406     "back"
   407     "defer"
   408     "prefer"))
   409 
   410 (provide 'isar-keywords)