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