etc/isar-keywords-ZF.el
author haftmann
Tue Jan 03 11:33:18 2006 +0100 (2006-01-03)
changeset 18552 30911da9fb27
parent 18541 00890455e95f
child 18612 7300f75028dc
permissions -rw-r--r--
class now a keyword
     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\\.redo"
    20     "ProofGeneral\\.restart"
    21     "ProofGeneral\\.try_context_thy_only"
    22     "ProofGeneral\\.undo"
    23     "also"
    24     "apply"
    25     "apply_end"
    26     "arities"
    27     "assume"
    28     "axclass"
    29     "axioms"
    30     "back"
    31     "by"
    32     "cannot_undo"
    33     "case"
    34     "cd"
    35     "chapter"
    36     "class"
    37     "classes"
    38     "classrel"
    39     "clear_undos"
    40     "codatatype"
    41     "code_alias"
    42     "code_class"
    43     "code_generate"
    44     "code_library"
    45     "code_module"
    46     "code_primclass"
    47     "code_primconst"
    48     "code_primtyco"
    49     "code_serialize"
    50     "code_syntax_const"
    51     "code_syntax_tyco"
    52     "coinductive"
    53     "commit"
    54     "constdefs"
    55     "consts"
    56     "consts_code"
    57     "context"
    58     "corollary"
    59     "datatype"
    60     "declare"
    61     "def"
    62     "defaultsort"
    63     "defer"
    64     "defs"
    65     "disable_pr"
    66     "display_drafts"
    67     "done"
    68     "enable_pr"
    69     "end"
    70     "exit"
    71     "extract"
    72     "extract_type"
    73     "finalconsts"
    74     "finally"
    75     "find_theorems"
    76     "fix"
    77     "from"
    78     "full_prf"
    79     "global"
    80     "guess"
    81     "have"
    82     "header"
    83     "hence"
    84     "hide"
    85     "inductive"
    86     "inductive_cases"
    87     "init_toplevel"
    88     "instance"
    89     "interpret"
    90     "interpretation"
    91     "judgment"
    92     "kill"
    93     "kill_thy"
    94     "lemma"
    95     "lemmas"
    96     "let"
    97     "local"
    98     "locale"
    99     "method_setup"
   100     "moreover"
   101     "next"
   102     "no_syntax"
   103     "nonterminals"
   104     "note"
   105     "obtain"
   106     "oops"
   107     "oracle"
   108     "parse_ast_translation"
   109     "parse_translation"
   110     "pr"
   111     "prefer"
   112     "presume"
   113     "pretty_setmargin"
   114     "prf"
   115     "primrec"
   116     "print_antiquotations"
   117     "print_ast_translation"
   118     "print_attributes"
   119     "print_binds"
   120     "print_cases"
   121     "print_claset"
   122     "print_commands"
   123     "print_context"
   124     "print_drafts"
   125     "print_facts"
   126     "print_induct_rules"
   127     "print_interps"
   128     "print_locale"
   129     "print_locales"
   130     "print_methods"
   131     "print_rules"
   132     "print_simpset"
   133     "print_syntax"
   134     "print_tcset"
   135     "print_theorems"
   136     "print_theory"
   137     "print_trans_rules"
   138     "print_translation"
   139     "proof"
   140     "prop"
   141     "pwd"
   142     "qed"
   143     "quickcheck"
   144     "quickcheck_params"
   145     "quit"
   146     "realizability"
   147     "realizers"
   148     "redo"
   149     "remove_thy"
   150     "rep_datatype"
   151     "sect"
   152     "section"
   153     "setup"
   154     "show"
   155     "sorry"
   156     "subsect"
   157     "subsection"
   158     "subsubsect"
   159     "subsubsection"
   160     "syntax"
   161     "term"
   162     "text"
   163     "text_raw"
   164     "then"
   165     "theorem"
   166     "theorems"
   167     "theory"
   168     "thm"
   169     "thm_deps"
   170     "thus"
   171     "token_translation"
   172     "touch_all_thys"
   173     "touch_child_thys"
   174     "touch_thy"
   175     "translations"
   176     "txt"
   177     "txt_raw"
   178     "typ"
   179     "typed_print_translation"
   180     "typedecl"
   181     "types"
   182     "types_code"
   183     "ultimately"
   184     "undo"
   185     "undos_proof"
   186     "unfolding"
   187     "update_thy"
   188     "update_thy_only"
   189     "use"
   190     "use_thy"
   191     "use_thy_only"
   192     "using"
   193     "value"
   194     "welcome"
   195     "with"
   196     "{"
   197     "}"))
   198 
   199 (defconst isar-keywords-minor
   200   '("advanced"
   201     "and"
   202     "assumes"
   203     "attach"
   204     "begin"
   205     "binder"
   206     "case_eqns"
   207     "con_defs"
   208     "concl"
   209     "constants"
   210     "constrains"
   211     "contains"
   212     "defines"
   213     "depending_on"
   214     "domains"
   215     "elimination"
   216     "file"
   217     "files"
   218     "fixes"
   219     "imports"
   220     "in"
   221     "includes"
   222     "induction"
   223     "infix"
   224     "infixl"
   225     "infixr"
   226     "intros"
   227     "is"
   228     "monos"
   229     "notes"
   230     "open"
   231     "output"
   232     "overloaded"
   233     "recursor_eqns"
   234     "shows"
   235     "structure"
   236     "type_elims"
   237     "type_intros"
   238     "uses"
   239     "where"))
   240 
   241 (defconst isar-keywords-control
   242   '("ProofGeneral\\.context_thy_only"
   243     "ProofGeneral\\.inform_file_processed"
   244     "ProofGeneral\\.inform_file_retracted"
   245     "ProofGeneral\\.kill_proof"
   246     "ProofGeneral\\.process_pgip"
   247     "ProofGeneral\\.redo"
   248     "ProofGeneral\\.restart"
   249     "ProofGeneral\\.try_context_thy_only"
   250     "ProofGeneral\\.undo"
   251     "cannot_undo"
   252     "clear_undos"
   253     "exit"
   254     "init_toplevel"
   255     "kill"
   256     "quit"
   257     "redo"
   258     "undo"
   259     "undos_proof"))
   260 
   261 (defconst isar-keywords-diag
   262   '("ML"
   263     "ML_command"
   264     "cd"
   265     "commit"
   266     "disable_pr"
   267     "display_drafts"
   268     "enable_pr"
   269     "find_theorems"
   270     "full_prf"
   271     "header"
   272     "kill_thy"
   273     "pr"
   274     "pretty_setmargin"
   275     "prf"
   276     "print_antiquotations"
   277     "print_attributes"
   278     "print_binds"
   279     "print_cases"
   280     "print_claset"
   281     "print_commands"
   282     "print_context"
   283     "print_drafts"
   284     "print_facts"
   285     "print_induct_rules"
   286     "print_interps"
   287     "print_locale"
   288     "print_locales"
   289     "print_methods"
   290     "print_rules"
   291     "print_simpset"
   292     "print_syntax"
   293     "print_tcset"
   294     "print_theorems"
   295     "print_theory"
   296     "print_trans_rules"
   297     "prop"
   298     "pwd"
   299     "quickcheck"
   300     "remove_thy"
   301     "term"
   302     "thm"
   303     "thm_deps"
   304     "touch_all_thys"
   305     "touch_child_thys"
   306     "touch_thy"
   307     "typ"
   308     "update_thy"
   309     "update_thy_only"
   310     "use"
   311     "use_thy"
   312     "use_thy_only"
   313     "value"
   314     "welcome"))
   315 
   316 (defconst isar-keywords-theory-begin
   317   '("theory"))
   318 
   319 (defconst isar-keywords-theory-switch
   320   '("context"))
   321 
   322 (defconst isar-keywords-theory-end
   323   '("end"))
   324 
   325 (defconst isar-keywords-theory-heading
   326   '("chapter"
   327     "section"
   328     "subsection"
   329     "subsubsection"))
   330 
   331 (defconst isar-keywords-theory-decl
   332   '("ML_setup"
   333     "arities"
   334     "axclass"
   335     "axioms"
   336     "class"
   337     "classes"
   338     "classrel"
   339     "codatatype"
   340     "code_alias"
   341     "code_class"
   342     "code_generate"
   343     "code_library"
   344     "code_module"
   345     "code_primclass"
   346     "code_primconst"
   347     "code_primtyco"
   348     "code_serialize"
   349     "code_syntax_const"
   350     "code_syntax_tyco"
   351     "coinductive"
   352     "constdefs"
   353     "consts"
   354     "consts_code"
   355     "datatype"
   356     "defaultsort"
   357     "defs"
   358     "extract"
   359     "extract_type"
   360     "finalconsts"
   361     "global"
   362     "hide"
   363     "inductive"
   364     "judgment"
   365     "lemmas"
   366     "local"
   367     "locale"
   368     "method_setup"
   369     "no_syntax"
   370     "nonterminals"
   371     "oracle"
   372     "parse_ast_translation"
   373     "parse_translation"
   374     "primrec"
   375     "print_ast_translation"
   376     "print_translation"
   377     "quickcheck_params"
   378     "realizability"
   379     "realizers"
   380     "rep_datatype"
   381     "setup"
   382     "syntax"
   383     "text"
   384     "text_raw"
   385     "theorems"
   386     "token_translation"
   387     "translations"
   388     "typed_print_translation"
   389     "typedecl"
   390     "types"
   391     "types_code"))
   392 
   393 (defconst isar-keywords-theory-script
   394   '("declare"
   395     "inductive_cases"))
   396 
   397 (defconst isar-keywords-theory-goal
   398   '("corollary"
   399     "instance"
   400     "interpretation"
   401     "lemma"
   402     "theorem"))
   403 
   404 (defconst isar-keywords-qed
   405   '("\\."
   406     "\\.\\."
   407     "by"
   408     "done"
   409     "sorry"))
   410 
   411 (defconst isar-keywords-qed-block
   412   '("qed"))
   413 
   414 (defconst isar-keywords-qed-global
   415   '("oops"))
   416 
   417 (defconst isar-keywords-proof-heading
   418   '("sect"
   419     "subsect"
   420     "subsubsect"))
   421 
   422 (defconst isar-keywords-proof-goal
   423   '("have"
   424     "hence"
   425     "interpret"
   426     "show"
   427     "thus"))
   428 
   429 (defconst isar-keywords-proof-block
   430   '("next"
   431     "proof"))
   432 
   433 (defconst isar-keywords-proof-open
   434   '("{"))
   435 
   436 (defconst isar-keywords-proof-close
   437   '("}"))
   438 
   439 (defconst isar-keywords-proof-chain
   440   '("finally"
   441     "from"
   442     "then"
   443     "ultimately"
   444     "with"))
   445 
   446 (defconst isar-keywords-proof-decl
   447   '("also"
   448     "let"
   449     "moreover"
   450     "note"
   451     "txt"
   452     "txt_raw"
   453     "unfolding"
   454     "using"))
   455 
   456 (defconst isar-keywords-proof-asm
   457   '("assume"
   458     "case"
   459     "def"
   460     "fix"
   461     "presume"))
   462 
   463 (defconst isar-keywords-proof-asm-goal
   464   '("guess"
   465     "obtain"))
   466 
   467 (defconst isar-keywords-proof-script
   468   '("apply"
   469     "apply_end"
   470     "back"
   471     "defer"
   472     "prefer"))
   473 
   474 (provide 'isar-keywords)