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