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