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