etc/isar-keywords-ZF.el
author nipkow
Mon Dec 13 17:07:47 2004 +0100 (2004-12-13)
changeset 15405 010ea63b7a67
parent 15141 a95c2ff210ba
child 15407 9e85d2b04867
permissions -rw-r--r--
added find_rewrites
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; This file was generated by Isabelle/ZF -- 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     "axclass"
    28     "axioms"
    29     "back"
    30     "by"
    31     "cannot_undo"
    32     "case"
    33     "cd"
    34     "chapter"
    35     "classes"
    36     "classrel"
    37     "clear_undos"
    38     "codatatype"
    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     "defs"
    52     "disable_pr"
    53     "display_drafts"
    54     "done"
    55     "enable_pr"
    56     "end"
    57     "exit"
    58     "extract"
    59     "extract_type"
    60     "finalconsts"
    61     "finally"
    62     "fix"
    63     "from"
    64     "full_prf"
    65     "generate_code"
    66     "global"
    67     "have"
    68     "header"
    69     "hence"
    70     "hide"
    71     "inductive"
    72     "inductive_cases"
    73     "init_toplevel"
    74     "instance"
    75     "instantiate"
    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_drafts"
   109     "print_facts"
   110     "print_induct_rules"
   111     "print_intros"
   112     "print_locale"
   113     "print_locales"
   114     "print_methods"
   115     "print_rules"
   116     "print_simpset"
   117     "print_syntax"
   118     "print_tcset"
   119     "print_theorems"
   120     "print_theory"
   121     "print_trans_rules"
   122     "print_translation"
   123     "proof"
   124     "prop"
   125     "pwd"
   126     "qed"
   127     "quickcheck"
   128     "quickcheck_params"
   129     "quit"
   130     "realizability"
   131     "realizers"
   132     "redo"
   133     "remove_thy"
   134     "rep_datatype"
   135     "sect"
   136     "section"
   137     "setup"
   138     "show"
   139     "sorry"
   140     "subsect"
   141     "subsection"
   142     "subsubsect"
   143     "subsubsection"
   144     "syntax"
   145     "term"
   146     "text"
   147     "text_raw"
   148     "then"
   149     "theorem"
   150     "theorems"
   151     "theory"
   152     "thm"
   153     "thm_deps"
   154     "thms_containing"
   155     "thus"
   156     "token_translation"
   157     "touch_all_thys"
   158     "touch_child_thys"
   159     "touch_thy"
   160     "translations"
   161     "txt"
   162     "txt_raw"
   163     "typ"
   164     "typed_print_translation"
   165     "typedecl"
   166     "types"
   167     "types_code"
   168     "ultimately"
   169     "undo"
   170     "undos_proof"
   171     "update_thy"
   172     "update_thy_only"
   173     "use"
   174     "use_thy"
   175     "use_thy_only"
   176     "using"
   177     "welcome"
   178     "with"
   179     "{"
   180     "}"))
   181 
   182 (defconst isar-keywords-minor
   183   '("advanced"
   184     "and"
   185     "assumes"
   186     "begin"
   187     "binder"
   188     "case_eqns"
   189     "con_defs"
   190     "concl"
   191     "defines"
   192     "domains"
   193     "elimination"
   194     "files"
   195     "fixes"
   196     "imports"
   197     "in"
   198     "includes"
   199     "induction"
   200     "infix"
   201     "infixl"
   202     "infixr"
   203     "intros"
   204     "is"
   205     "monos"
   206     "notes"
   207     "open"
   208     "output"
   209     "overloaded"
   210     "recursor_eqns"
   211     "shows"
   212     "structure"
   213     "type_elims"
   214     "type_intros"
   215     "where"))
   216 
   217 (defconst isar-keywords-control
   218   '("ProofGeneral\\.context_thy_only"
   219     "ProofGeneral\\.inform_file_processed"
   220     "ProofGeneral\\.inform_file_retracted"
   221     "ProofGeneral\\.kill_proof"
   222     "ProofGeneral\\.process_pgip"
   223     "ProofGeneral\\.restart"
   224     "ProofGeneral\\.try_context_thy_only"
   225     "ProofGeneral\\.undo"
   226     "cannot_undo"
   227     "clear_undos"
   228     "exit"
   229     "init_toplevel"
   230     "kill"
   231     "quit"
   232     "redo"
   233     "undo"
   234     "undos_proof"))
   235 
   236 (defconst isar-keywords-diag
   237   '("ML"
   238     "ML_command"
   239     "cd"
   240     "commit"
   241     "disable_pr"
   242     "display_drafts"
   243     "enable_pr"
   244     "full_prf"
   245     "header"
   246     "kill_thy"
   247     "pr"
   248     "pretty_setmargin"
   249     "prf"
   250     "print_antiquotations"
   251     "print_attributes"
   252     "print_binds"
   253     "print_cases"
   254     "print_claset"
   255     "print_commands"
   256     "print_context"
   257     "print_drafts"
   258     "print_facts"
   259     "print_induct_rules"
   260     "print_intros"
   261     "print_locale"
   262     "print_locales"
   263     "print_methods"
   264     "print_rules"
   265     "print_simpset"
   266     "print_syntax"
   267     "print_tcset"
   268     "print_theorems"
   269     "print_theory"
   270     "print_trans_rules"
   271     "prop"
   272     "pwd"
   273     "quickcheck"
   274     "remove_thy"
   275     "term"
   276     "thm"
   277     "thm_deps"
   278     "thms_containing"
   279     "touch_all_thys"
   280     "touch_child_thys"
   281     "touch_thy"
   282     "typ"
   283     "update_thy"
   284     "update_thy_only"
   285     "use"
   286     "use_thy"
   287     "use_thy_only"
   288     "welcome"))
   289 
   290 (defconst isar-keywords-theory-begin
   291   '("theory"))
   292 
   293 (defconst isar-keywords-theory-switch
   294   '("context"))
   295 
   296 (defconst isar-keywords-theory-end
   297   '("end"))
   298 
   299 (defconst isar-keywords-theory-heading
   300   '("chapter"
   301     "section"
   302     "subsection"
   303     "subsubsection"))
   304 
   305 (defconst isar-keywords-theory-decl
   306   '("ML_setup"
   307     "arities"
   308     "axclass"
   309     "axioms"
   310     "classes"
   311     "classrel"
   312     "codatatype"
   313     "coinductive"
   314     "constdefs"
   315     "consts"
   316     "consts_code"
   317     "datatype"
   318     "defaultsort"
   319     "defs"
   320     "extract"
   321     "extract_type"
   322     "finalconsts"
   323     "generate_code"
   324     "global"
   325     "hide"
   326     "inductive"
   327     "judgment"
   328     "lemmas"
   329     "local"
   330     "locale"
   331     "method_setup"
   332     "nonterminals"
   333     "oracle"
   334     "parse_ast_translation"
   335     "parse_translation"
   336     "primrec"
   337     "print_ast_translation"
   338     "print_translation"
   339     "quickcheck_params"
   340     "realizability"
   341     "realizers"
   342     "rep_datatype"
   343     "setup"
   344     "syntax"
   345     "text"
   346     "text_raw"
   347     "theorems"
   348     "token_translation"
   349     "translations"
   350     "typed_print_translation"
   351     "typedecl"
   352     "types"
   353     "types_code"))
   354 
   355 (defconst isar-keywords-theory-script
   356   '("declare"
   357     "inductive_cases"))
   358 
   359 (defconst isar-keywords-theory-goal
   360   '("corollary"
   361     "instance"
   362     "lemma"
   363     "theorem"))
   364 
   365 (defconst isar-keywords-qed
   366   '("\\."
   367     "\\.\\."
   368     "by"
   369     "done"
   370     "sorry"))
   371 
   372 (defconst isar-keywords-qed-block
   373   '("qed"))
   374 
   375 (defconst isar-keywords-qed-global
   376   '("oops"))
   377 
   378 (defconst isar-keywords-proof-heading
   379   '("sect"
   380     "subsect"
   381     "subsubsect"))
   382 
   383 (defconst isar-keywords-proof-goal
   384   '("have"
   385     "hence"
   386     "show"
   387     "thus"))
   388 
   389 (defconst isar-keywords-proof-block
   390   '("next"
   391     "proof"))
   392 
   393 (defconst isar-keywords-proof-open
   394   '("{"))
   395 
   396 (defconst isar-keywords-proof-close
   397   '("}"))
   398 
   399 (defconst isar-keywords-proof-chain
   400   '("finally"
   401     "from"
   402     "then"
   403     "ultimately"
   404     "with"))
   405 
   406 (defconst isar-keywords-proof-decl
   407   '("also"
   408     "instantiate"
   409     "let"
   410     "moreover"
   411     "note"
   412     "txt"
   413     "txt_raw"
   414     "using"))
   415 
   416 (defconst isar-keywords-proof-asm
   417   '("assume"
   418     "case"
   419     "def"
   420     "fix"
   421     "presume"))
   422 
   423 (defconst isar-keywords-proof-asm-goal
   424   '("obtain"))
   425 
   426 (defconst isar-keywords-proof-script
   427   '("apply"
   428     "apply_end"
   429     "back"
   430     "defer"
   431     "prefer"))
   432 
   433 (provide 'isar-keywords)