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