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