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