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