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