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