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