etc/isar-keywords.el
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15624 484178635bd8
child 15762 13d1ec61bc89
permissions -rw-r--r--
*** empty log message ***
     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     "ML"
    11     "ML_command"
    12     "ML_setup"
    13     "ProofGeneral\\.context_thy_only"
    14     "ProofGeneral\\.inform_file_processed"
    15     "ProofGeneral\\.inform_file_retracted"
    16     "ProofGeneral\\.kill_proof"
    17     "ProofGeneral\\.process_pgip"
    18     "ProofGeneral\\.restart"
    19     "ProofGeneral\\.try_context_thy_only"
    20     "ProofGeneral\\.undo"
    21     "\\.\\."
    22     "also"
    23     "apply"
    24     "apply_end"
    25     "arities"
    26     "assume"
    27     "automaton"
    28     "ax_specification"
    29     "axclass"
    30     "axioms"
    31     "back"
    32     "by"
    33     "cannot_undo"
    34     "case"
    35     "cd"
    36     "chapter"
    37     "classes"
    38     "classrel"
    39     "clear_undos"
    40     "coinductive"
    41     "commit"
    42     "constdefs"
    43     "consts"
    44     "consts_code"
    45     "context"
    46     "corollary"
    47     "datatype"
    48     "declare"
    49     "def"
    50     "defaultsort"
    51     "defer"
    52     "defer_recdef"
    53     "defs"
    54     "disable_pr"
    55     "display_drafts"
    56     "domain"
    57     "done"
    58     "enable_pr"
    59     "end"
    60     "exit"
    61     "extract"
    62     "extract_type"
    63     "finalconsts"
    64     "finally"
    65     "find_rewrites"
    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_intros"
   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     "defines"
   207     "distinct"
   208     "files"
   209     "fixes"
   210     "hide_action"
   211     "hints"
   212     "imports"
   213     "in"
   214     "includes"
   215     "induction"
   216     "infix"
   217     "infixl"
   218     "infixr"
   219     "initially"
   220     "inject"
   221     "inputs"
   222     "internals"
   223     "intros"
   224     "is"
   225     "lazy"
   226     "monos"
   227     "morphisms"
   228     "notes"
   229     "open"
   230     "output"
   231     "outputs"
   232     "overloaded"
   233     "permissive"
   234     "post"
   235     "pre"
   236     "rename"
   237     "restrict"
   238     "shows"
   239     "signature"
   240     "states"
   241     "structure"
   242     "to"
   243     "transitions"
   244     "transrel"
   245     "where"))
   246 
   247 (defconst isar-keywords-control
   248   '("ProofGeneral\\.context_thy_only"
   249     "ProofGeneral\\.inform_file_processed"
   250     "ProofGeneral\\.inform_file_retracted"
   251     "ProofGeneral\\.kill_proof"
   252     "ProofGeneral\\.process_pgip"
   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     "find_rewrites"
   275     "full_prf"
   276     "header"
   277     "kill_thy"
   278     "pr"
   279     "pretty_setmargin"
   280     "prf"
   281     "print_antiquotations"
   282     "print_attributes"
   283     "print_binds"
   284     "print_cases"
   285     "print_claset"
   286     "print_commands"
   287     "print_context"
   288     "print_drafts"
   289     "print_facts"
   290     "print_induct_rules"
   291     "print_interps"
   292     "print_intros"
   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     "generate_code"
   358     "global"
   359     "hide"
   360     "inductive"
   361     "judgment"
   362     "lemmas"
   363     "local"
   364     "locale"
   365     "method_setup"
   366     "no_syntax"
   367     "nonterminals"
   368     "oracle"
   369     "parse_ast_translation"
   370     "parse_translation"
   371     "primrec"
   372     "print_ast_translation"
   373     "print_translation"
   374     "quickcheck_params"
   375     "realizability"
   376     "realizers"
   377     "recdef"
   378     "record"
   379     "refute_params"
   380     "rep_datatype"
   381     "setup"
   382     "syntax"
   383     "text"
   384     "text_raw"
   385     "theorems"
   386     "token_translation"
   387     "translations"
   388     "typed_print_translation"
   389     "typedecl"
   390     "types"
   391     "types_code"))
   392 
   393 (defconst isar-keywords-theory-script
   394   '("declare"
   395     "inductive_cases"))
   396 
   397 (defconst isar-keywords-theory-goal
   398   '("ax_specification"
   399     "corollary"
   400     "instance"
   401     "interpretation"
   402     "lemma"
   403     "recdef_tc"
   404     "specification"
   405     "theorem"
   406     "typedef"))
   407 
   408 (defconst isar-keywords-qed
   409   '("\\."
   410     "\\.\\."
   411     "by"
   412     "done"
   413     "sorry"))
   414 
   415 (defconst isar-keywords-qed-block
   416   '("qed"))
   417 
   418 (defconst isar-keywords-qed-global
   419   '("oops"))
   420 
   421 (defconst isar-keywords-proof-heading
   422   '("sect"
   423     "subsect"
   424     "subsubsect"))
   425 
   426 (defconst isar-keywords-proof-goal
   427   '("have"
   428     "hence"
   429     "interpret"
   430     "show"
   431     "thus"))
   432 
   433 (defconst isar-keywords-proof-block
   434   '("next"
   435     "proof"))
   436 
   437 (defconst isar-keywords-proof-open
   438   '("{"))
   439 
   440 (defconst isar-keywords-proof-close
   441   '("}"))
   442 
   443 (defconst isar-keywords-proof-chain
   444   '("finally"
   445     "from"
   446     "then"
   447     "ultimately"
   448     "with"))
   449 
   450 (defconst isar-keywords-proof-decl
   451   '("also"
   452     "instantiate"
   453     "let"
   454     "moreover"
   455     "note"
   456     "txt"
   457     "txt_raw"
   458     "using"))
   459 
   460 (defconst isar-keywords-proof-asm
   461   '("assume"
   462     "case"
   463     "def"
   464     "fix"
   465     "presume"))
   466 
   467 (defconst isar-keywords-proof-asm-goal
   468   '("obtain"))
   469 
   470 (defconst isar-keywords-proof-script
   471   '("apply"
   472     "apply_end"
   473     "back"
   474     "defer"
   475     "prefer"))
   476 
   477 (provide 'isar-keywords)