etc/isar-keywords.el
author berghofe
Tue Jul 12 11:54:55 2005 +0200 (2005-07-12)
changeset 16771 2b534c5b5625
parent 16701 abd0abd66387
child 17091 13593aa6a546
permissions -rw-r--r--
Added "attach" keyword for code generator setup.
     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     "attach"
   204     "begin"
   205     "binder"
   206     "compose"
   207     "concl"
   208     "congs"
   209     "constrains"
   210     "defines"
   211     "distinct"
   212     "files"
   213     "fixes"
   214     "hide_action"
   215     "hints"
   216     "imports"
   217     "in"
   218     "includes"
   219     "induction"
   220     "infix"
   221     "infixl"
   222     "infixr"
   223     "initially"
   224     "inject"
   225     "inputs"
   226     "internals"
   227     "intros"
   228     "is"
   229     "lazy"
   230     "monos"
   231     "morphisms"
   232     "notes"
   233     "open"
   234     "output"
   235     "outputs"
   236     "overloaded"
   237     "permissive"
   238     "post"
   239     "pre"
   240     "rename"
   241     "restrict"
   242     "shows"
   243     "signature"
   244     "states"
   245     "structure"
   246     "to"
   247     "transitions"
   248     "transrel"
   249     "uses"
   250     "where"))
   251 
   252 (defconst isar-keywords-control
   253   '("ProofGeneral\\.context_thy_only"
   254     "ProofGeneral\\.inform_file_processed"
   255     "ProofGeneral\\.inform_file_retracted"
   256     "ProofGeneral\\.kill_proof"
   257     "ProofGeneral\\.process_pgip"
   258     "ProofGeneral\\.redo"
   259     "ProofGeneral\\.restart"
   260     "ProofGeneral\\.try_context_thy_only"
   261     "ProofGeneral\\.undo"
   262     "cannot_undo"
   263     "clear_undos"
   264     "exit"
   265     "init_toplevel"
   266     "kill"
   267     "quit"
   268     "redo"
   269     "undo"
   270     "undos_proof"))
   271 
   272 (defconst isar-keywords-diag
   273   '("ML"
   274     "ML_command"
   275     "cd"
   276     "commit"
   277     "disable_pr"
   278     "display_drafts"
   279     "enable_pr"
   280     "full_prf"
   281     "header"
   282     "kill_thy"
   283     "pr"
   284     "pretty_setmargin"
   285     "prf"
   286     "print_antiquotations"
   287     "print_attributes"
   288     "print_binds"
   289     "print_cases"
   290     "print_claset"
   291     "print_commands"
   292     "print_context"
   293     "print_drafts"
   294     "print_facts"
   295     "print_induct_rules"
   296     "print_interps"
   297     "print_locale"
   298     "print_locales"
   299     "print_methods"
   300     "print_rules"
   301     "print_simpset"
   302     "print_syntax"
   303     "print_theorems"
   304     "print_theory"
   305     "print_trans_rules"
   306     "prop"
   307     "pwd"
   308     "quickcheck"
   309     "refute"
   310     "remove_thy"
   311     "term"
   312     "thm"
   313     "thm_deps"
   314     "thms_containing"
   315     "touch_all_thys"
   316     "touch_child_thys"
   317     "touch_thy"
   318     "typ"
   319     "update_thy"
   320     "update_thy_only"
   321     "use"
   322     "use_thy"
   323     "use_thy_only"
   324     "welcome"))
   325 
   326 (defconst isar-keywords-theory-begin
   327   '("theory"))
   328 
   329 (defconst isar-keywords-theory-switch
   330   '("context"))
   331 
   332 (defconst isar-keywords-theory-end
   333   '("end"))
   334 
   335 (defconst isar-keywords-theory-heading
   336   '("chapter"
   337     "section"
   338     "subsection"
   339     "subsubsection"))
   340 
   341 (defconst isar-keywords-theory-decl
   342   '("ML_setup"
   343     "arities"
   344     "automaton"
   345     "axclass"
   346     "axioms"
   347     "classes"
   348     "classrel"
   349     "coinductive"
   350     "constdefs"
   351     "consts"
   352     "consts_code"
   353     "datatype"
   354     "defaultsort"
   355     "defer_recdef"
   356     "defs"
   357     "domain"
   358     "extract"
   359     "extract_type"
   360     "finalconsts"
   361     "fixpat"
   362     "fixrec"
   363     "generate_code"
   364     "global"
   365     "hide"
   366     "inductive"
   367     "judgment"
   368     "lemmas"
   369     "local"
   370     "locale"
   371     "method_setup"
   372     "no_syntax"
   373     "nonterminals"
   374     "oracle"
   375     "parse_ast_translation"
   376     "parse_translation"
   377     "primrec"
   378     "print_ast_translation"
   379     "print_translation"
   380     "quickcheck_params"
   381     "realizability"
   382     "realizers"
   383     "recdef"
   384     "record"
   385     "refute_params"
   386     "rep_datatype"
   387     "setup"
   388     "syntax"
   389     "text"
   390     "text_raw"
   391     "theorems"
   392     "token_translation"
   393     "translations"
   394     "typed_print_translation"
   395     "typedecl"
   396     "types"
   397     "types_code"))
   398 
   399 (defconst isar-keywords-theory-script
   400   '("declare"
   401     "inductive_cases"))
   402 
   403 (defconst isar-keywords-theory-goal
   404   '("ax_specification"
   405     "corollary"
   406     "cpodef"
   407     "instance"
   408     "interpretation"
   409     "lemma"
   410     "pcpodef"
   411     "recdef_tc"
   412     "specification"
   413     "theorem"
   414     "typedef"))
   415 
   416 (defconst isar-keywords-qed
   417   '("\\."
   418     "\\.\\."
   419     "by"
   420     "done"
   421     "sorry"))
   422 
   423 (defconst isar-keywords-qed-block
   424   '("qed"))
   425 
   426 (defconst isar-keywords-qed-global
   427   '("oops"))
   428 
   429 (defconst isar-keywords-proof-heading
   430   '("sect"
   431     "subsect"
   432     "subsubsect"))
   433 
   434 (defconst isar-keywords-proof-goal
   435   '("have"
   436     "hence"
   437     "interpret"
   438     "show"
   439     "thus"))
   440 
   441 (defconst isar-keywords-proof-block
   442   '("next"
   443     "proof"))
   444 
   445 (defconst isar-keywords-proof-open
   446   '("{"))
   447 
   448 (defconst isar-keywords-proof-close
   449   '("}"))
   450 
   451 (defconst isar-keywords-proof-chain
   452   '("finally"
   453     "from"
   454     "then"
   455     "ultimately"
   456     "with"))
   457 
   458 (defconst isar-keywords-proof-decl
   459   '("also"
   460     "let"
   461     "moreover"
   462     "note"
   463     "txt"
   464     "txt_raw"
   465     "using"))
   466 
   467 (defconst isar-keywords-proof-asm
   468   '("assume"
   469     "case"
   470     "def"
   471     "fix"
   472     "presume"))
   473 
   474 (defconst isar-keywords-proof-asm-goal
   475   '("obtain"))
   476 
   477 (defconst isar-keywords-proof-script
   478   '("apply"
   479     "apply_end"
   480     "back"
   481     "defer"
   482     "prefer"))
   483 
   484 (provide 'isar-keywords)