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