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