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