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