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