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