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