etc/isar-keywords-ZF.el
author bulwahn
Mon May 11 09:18:42 2009 +0200 (2009-05-11)
changeset 31106 9a1178204dc0
parent 30745 2823a89c76a4
child 31107 657386d94f14
permissions -rw-r--r--
Added pred_code command
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
     4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     5 ;;
     6 
     7 (defconst isar-keywords-major
     8   '("\\."
     9     "\\.\\."
    10     "Isabelle\\.command"
    11     "Isar\\.begin_document"
    12     "Isar\\.command"
    13     "Isar\\.define_command"
    14     "Isar\\.edit_document"
    15     "Isar\\.end_document"
    16     "Isar\\.insert"
    17     "Isar\\.remove"
    18     "ML"
    19     "ML_command"
    20     "ML_prf"
    21     "ML_val"
    22     "ProofGeneral\\.inform_file_processed"
    23     "ProofGeneral\\.inform_file_retracted"
    24     "ProofGeneral\\.kill_proof"
    25     "ProofGeneral\\.process_pgip"
    26     "ProofGeneral\\.restart"
    27     "ProofGeneral\\.undo"
    28     "abbreviation"
    29     "also"
    30     "apply"
    31     "apply_end"
    32     "arities"
    33     "assume"
    34     "attribute_setup"
    35     "axclass"
    36     "axiomatization"
    37     "axioms"
    38     "back"
    39     "by"
    40     "cannot_undo"
    41     "case"
    42     "cd"
    43     "chapter"
    44     "class"
    45     "class_deps"
    46     "classes"
    47     "classrel"
    48     "code_datatype"
    49     "code_library"
    50     "code_module"
    51     "commit"
    52     "constdefs"
    53     "consts"
    54     "consts_code"
    55     "context"
    56     "corollary"
    57     "declaration"
    58     "declare"
    59     "def"
    60     "defaultsort"
    61     "defer"
    62     "definition"
    63     "defs"
    64     "disable_pr"
    65     "display_drafts"
    66     "done"
    67     "enable_pr"
    68     "end"
    69     "exit"
    70     "extract"
    71     "extract_type"
    72     "finalconsts"
    73     "finally"
    74     "find_consts"
    75     "find_theorems"
    76     "fix"
    77     "from"
    78     "full_prf"
    79     "global"
    80     "guess"
    81     "have"
    82     "header"
    83     "help"
    84     "hence"
    85     "hide"
    86     "init_toplevel"
    87     "instance"
    88     "instantiation"
    89     "interpret"
    90     "interpretation"
    91     "judgment"
    92     "kill"
    93     "kill_thy"
    94     "lemma"
    95     "lemmas"
    96     "let"
    97     "linear_undo"
    98     "local"
    99     "local_setup"
   100     "locale"
   101     "method_setup"
   102     "moreover"
   103     "next"
   104     "no_notation"
   105     "no_syntax"
   106     "no_translations"
   107     "nonterminals"
   108     "notation"
   109     "note"
   110     "obtain"
   111     "oops"
   112     "oracle"
   113     "overloading"
   114     "parse_ast_translation"
   115     "parse_translation"
   116     "pr"
   117     "prefer"
   118     "presume"
   119     "pretty_setmargin"
   120     "prf"
   121     "print_abbrevs"
   122     "print_antiquotations"
   123     "print_ast_translation"
   124     "print_attributes"
   125     "print_binds"
   126     "print_cases"
   127     "print_claset"
   128     "print_classes"
   129     "print_codesetup"
   130     "print_commands"
   131     "print_configs"
   132     "print_context"
   133     "print_drafts"
   134     "print_facts"
   135     "print_induct_rules"
   136     "print_locale"
   137     "print_locales"
   138     "print_methods"
   139     "print_rules"
   140     "print_simpset"
   141     "print_statement"
   142     "print_syntax"
   143     "print_theorems"
   144     "print_theory"
   145     "print_trans_rules"
   146     "print_translation"
   147     "proof"
   148     "prop"
   149     "pwd"
   150     "qed"
   151     "quickcheck"
   152     "quickcheck_params"
   153     "quit"
   154     "realizability"
   155     "realizers"
   156     "remove_thy"
   157     "sect"
   158     "section"
   159     "setup"
   160     "show"
   161     "simproc_setup"
   162     "sorry"
   163     "subclass"
   164     "sublocale"
   165     "subsect"
   166     "subsection"
   167     "subsubsect"
   168     "subsubsection"
   169     "syntax"
   170     "term"
   171     "text"
   172     "text_raw"
   173     "then"
   174     "theorem"
   175     "theorems"
   176     "theory"
   177     "thm"
   178     "thm_deps"
   179     "thus"
   180     "thy_deps"
   181     "touch_thy"
   182     "translations"
   183     "txt"
   184     "txt_raw"
   185     "typ"
   186     "typed_print_translation"
   187     "typedecl"
   188     "types"
   189     "types_code"
   190     "ultimately"
   191     "undo"
   192     "undos_proof"
   193     "unfolding"
   194     "unused_thms"
   195     "use"
   196     "use_thy"
   197     "using"
   198     "welcome"
   199     "with"
   200     "{"
   201     "}"))
   202 
   203 (defconst isar-keywords-minor
   204   '("advanced"
   205     "and"
   206     "assumes"
   207     "attach"
   208     "begin"
   209     "binder"
   210     "constrains"
   211     "contains"
   212     "defines"
   213     "file"
   214     "fixes"
   215     "for"
   216     "identifier"
   217     "if"
   218     "imports"
   219     "in"
   220     "infix"
   221     "infixl"
   222     "infixr"
   223     "is"
   224     "notes"
   225     "obtains"
   226     "open"
   227     "output"
   228     "overloaded"
   229     "shows"
   230     "structure"
   231     "unchecked"
   232     "uses"
   233     "where"))
   234 
   235 (defconst isar-keywords-control
   236   '("Isabelle\\.command"
   237     "Isar\\.begin_document"
   238     "Isar\\.command"
   239     "Isar\\.define_command"
   240     "Isar\\.edit_document"
   241     "Isar\\.end_document"
   242     "Isar\\.insert"
   243     "Isar\\.remove"
   244     "ProofGeneral\\.inform_file_processed"
   245     "ProofGeneral\\.inform_file_retracted"
   246     "ProofGeneral\\.kill_proof"
   247     "ProofGeneral\\.process_pgip"
   248     "ProofGeneral\\.restart"
   249     "ProofGeneral\\.undo"
   250     "cannot_undo"
   251     "exit"
   252     "init_toplevel"
   253     "kill"
   254     "linear_undo"
   255     "quit"
   256     "undo"
   257     "undos_proof"))
   258 
   259 (defconst isar-keywords-diag
   260   '("ML_command"
   261     "ML_val"
   262     "cd"
   263     "class_deps"
   264     "commit"
   265     "disable_pr"
   266     "display_drafts"
   267     "enable_pr"
   268     "find_consts"
   269     "find_theorems"
   270     "full_prf"
   271     "header"
   272     "help"
   273     "kill_thy"
   274     "pr"
   275     "pretty_setmargin"
   276     "prf"
   277     "print_abbrevs"
   278     "print_antiquotations"
   279     "print_attributes"
   280     "print_binds"
   281     "print_cases"
   282     "print_claset"
   283     "print_classes"
   284     "print_codesetup"
   285     "print_commands"
   286     "print_configs"
   287     "print_context"
   288     "print_drafts"
   289     "print_facts"
   290     "print_induct_rules"
   291     "print_locale"
   292     "print_locales"
   293     "print_methods"
   294     "print_rules"
   295     "print_simpset"
   296     "print_statement"
   297     "print_syntax"
   298     "print_theorems"
   299     "print_theory"
   300     "print_trans_rules"
   301     "prop"
   302     "pwd"
   303     "quickcheck"
   304     "remove_thy"
   305     "term"
   306     "thm"
   307     "thm_deps"
   308     "thy_deps"
   309     "touch_thy"
   310     "typ"
   311     "unused_thms"
   312     "use_thy"
   313     "welcome"))
   314 
   315 (defconst isar-keywords-theory-begin
   316   '("theory"))
   317 
   318 (defconst isar-keywords-theory-switch
   319   '())
   320 
   321 (defconst isar-keywords-theory-end
   322   '("end"))
   323 
   324 (defconst isar-keywords-theory-heading
   325   '("chapter"
   326     "section"
   327     "subsection"
   328     "subsubsection"))
   329 
   330 (defconst isar-keywords-theory-decl
   331   '("ML"
   332     "abbreviation"
   333     "arities"
   334     "attribute_setup"
   335     "axclass"
   336     "axiomatization"
   337     "axioms"
   338     "class"
   339     "classes"
   340     "classrel"
   341     "code_datatype"
   342     "code_library"
   343     "code_module"
   344     "constdefs"
   345     "consts"
   346     "consts_code"
   347     "context"
   348     "declaration"
   349     "declare"
   350     "defaultsort"
   351     "definition"
   352     "defs"
   353     "extract"
   354     "extract_type"
   355     "finalconsts"
   356     "global"
   357     "hide"
   358     "instantiation"
   359     "judgment"
   360     "lemmas"
   361     "local"
   362     "local_setup"
   363     "locale"
   364     "method_setup"
   365     "no_notation"
   366     "no_syntax"
   367     "no_translations"
   368     "nonterminals"
   369     "notation"
   370     "oracle"
   371     "overloading"
   372     "parse_ast_translation"
   373     "parse_translation"
   374     "print_ast_translation"
   375     "print_translation"
   376     "quickcheck_params"
   377     "realizability"
   378     "realizers"
   379     "setup"
   380     "simproc_setup"
   381     "syntax"
   382     "text"
   383     "text_raw"
   384     "theorems"
   385     "translations"
   386     "typed_print_translation"
   387     "typedecl"
   388     "types"
   389     "types_code"
   390     "use"))
   391 
   392 (defconst isar-keywords-theory-script
   393   '())
   394 
   395 (defconst isar-keywords-theory-goal
   396   '("corollary"
   397     "instance"
   398     "interpretation"
   399     "lemma"
   400     "subclass"
   401     "sublocale"
   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 
   427 (defconst isar-keywords-proof-block
   428   '("next"
   429     "proof"))
   430 
   431 (defconst isar-keywords-proof-open
   432   '("{"))
   433 
   434 (defconst isar-keywords-proof-close
   435   '("}"))
   436 
   437 (defconst isar-keywords-proof-chain
   438   '("finally"
   439     "from"
   440     "then"
   441     "ultimately"
   442     "with"))
   443 
   444 (defconst isar-keywords-proof-decl
   445   '("ML_prf"
   446     "also"
   447     "let"
   448     "moreover"
   449     "note"
   450     "txt"
   451     "txt_raw"
   452     "unfolding"
   453     "using"))
   454 
   455 (defconst isar-keywords-proof-asm
   456   '("assume"
   457     "case"
   458     "def"
   459     "fix"
   460     "presume"))
   461 
   462 (defconst isar-keywords-proof-asm-goal
   463   '("guess"
   464     "obtain"
   465     "show"
   466     "thus"))
   467 
   468 (defconst isar-keywords-proof-script
   469   '("apply"
   470     "apply_end"
   471     "back"
   472     "defer"
   473     "prefer"))
   474 
   475 (provide 'isar-keywords)