etc/isar-keywords.el
author huffman
Sat Jun 04 02:13:31 2005 +0200 (2005-06-04)
changeset 16231 91c0a3e253b1
parent 16168 adb83939177f
child 16419 0c3db621bbbd
permissions -rw-r--r--
add keywords fixrec and fixpat for HOLCF fixrec package
     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     "fixrec"
    68     "fixpat"
    69     "from"
    70     "full_prf"
    71     "generate_code"
    72     "global"
    73     "have"
    74     "header"
    75     "hence"
    76     "hide"
    77     "inductive"
    78     "inductive_cases"
    79     "init_toplevel"
    80     "instance"
    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_locale"
   121     "print_locales"
   122     "print_methods"
   123     "print_rules"
   124     "print_simpset"
   125     "print_syntax"
   126     "print_theorems"
   127     "print_theory"
   128     "print_trans_rules"
   129     "print_translation"
   130     "proof"
   131     "prop"
   132     "pwd"
   133     "qed"
   134     "quickcheck"
   135     "quickcheck_params"
   136     "quit"
   137     "realizability"
   138     "realizers"
   139     "recdef"
   140     "recdef_tc"
   141     "record"
   142     "redo"
   143     "refute"
   144     "refute_params"
   145     "remove_thy"
   146     "rep_datatype"
   147     "sect"
   148     "section"
   149     "setup"
   150     "show"
   151     "sorry"
   152     "specification"
   153     "subsect"
   154     "subsection"
   155     "subsubsect"
   156     "subsubsection"
   157     "syntax"
   158     "term"
   159     "text"
   160     "text_raw"
   161     "then"
   162     "theorem"
   163     "theorems"
   164     "theory"
   165     "thm"
   166     "thm_deps"
   167     "thms_containing"
   168     "thus"
   169     "token_translation"
   170     "touch_all_thys"
   171     "touch_child_thys"
   172     "touch_thy"
   173     "translations"
   174     "txt"
   175     "txt_raw"
   176     "typ"
   177     "typed_print_translation"
   178     "typedecl"
   179     "typedef"
   180     "types"
   181     "types_code"
   182     "ultimately"
   183     "undo"
   184     "undos_proof"
   185     "update_thy"
   186     "update_thy_only"
   187     "use"
   188     "use_thy"
   189     "use_thy_only"
   190     "using"
   191     "welcome"
   192     "with"
   193     "{"
   194     "}"))
   195 
   196 (defconst isar-keywords-minor
   197   '("actions"
   198     "advanced"
   199     "and"
   200     "assumes"
   201     "begin"
   202     "binder"
   203     "compose"
   204     "concl"
   205     "congs"
   206     "constrains"
   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     "full_prf"
   277     "header"
   278     "kill_thy"
   279     "pr"
   280     "pretty_setmargin"
   281     "prf"
   282     "print_antiquotations"
   283     "print_attributes"
   284     "print_binds"
   285     "print_cases"
   286     "print_claset"
   287     "print_commands"
   288     "print_context"
   289     "print_drafts"
   290     "print_facts"
   291     "print_induct_rules"
   292     "print_interps"
   293     "print_locale"
   294     "print_locales"
   295     "print_methods"
   296     "print_rules"
   297     "print_simpset"
   298     "print_syntax"
   299     "print_theorems"
   300     "print_theory"
   301     "print_trans_rules"
   302     "prop"
   303     "pwd"
   304     "quickcheck"
   305     "refute"
   306     "remove_thy"
   307     "term"
   308     "thm"
   309     "thm_deps"
   310     "thms_containing"
   311     "touch_all_thys"
   312     "touch_child_thys"
   313     "touch_thy"
   314     "typ"
   315     "update_thy"
   316     "update_thy_only"
   317     "use"
   318     "use_thy"
   319     "use_thy_only"
   320     "welcome"))
   321 
   322 (defconst isar-keywords-theory-begin
   323   '("theory"))
   324 
   325 (defconst isar-keywords-theory-switch
   326   '("context"))
   327 
   328 (defconst isar-keywords-theory-end
   329   '("end"))
   330 
   331 (defconst isar-keywords-theory-heading
   332   '("chapter"
   333     "section"
   334     "subsection"
   335     "subsubsection"))
   336 
   337 (defconst isar-keywords-theory-decl
   338   '("ML_setup"
   339     "arities"
   340     "automaton"
   341     "axclass"
   342     "axioms"
   343     "classes"
   344     "classrel"
   345     "coinductive"
   346     "constdefs"
   347     "consts"
   348     "consts_code"
   349     "datatype"
   350     "defaultsort"
   351     "defer_recdef"
   352     "defs"
   353     "domain"
   354     "extract"
   355     "extract_type"
   356     "finalconsts"
   357     "fixrec"
   358     "fixpat"
   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     "let"
   455     "moreover"
   456     "note"
   457     "txt"
   458     "txt_raw"
   459     "using"))
   460 
   461 (defconst isar-keywords-proof-asm
   462   '("assume"
   463     "case"
   464     "def"
   465     "fix"
   466     "presume"))
   467 
   468 (defconst isar-keywords-proof-asm-goal
   469   '("obtain"))
   470 
   471 (defconst isar-keywords-proof-script
   472   '("apply"
   473     "apply_end"
   474     "back"
   475     "defer"
   476     "prefer"))
   477 
   478 (provide 'isar-keywords)