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