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