etc/isar-keywords.el
author ballarin
Thu Mar 24 17:03:37 2005 +0100 (2005-03-24)
changeset 15624 484178635bd8
parent 15598 4ab52355bb53
child 15703 727ef1b8b3ee
permissions -rw-r--r--
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; This file was generated by Isabelle/HOLCF/IOA -- 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\\.restart"
    20     "ProofGeneral\\.try_context_thy_only"
    21     "ProofGeneral\\.undo"
    22     "also"
    23     "apply"
    24     "apply_end"
    25     "arities"
    26     "assume"
    27     "automaton"
    28     "ax_specification"
    29     "axclass"
    30     "axioms"
    31     "back"
    32     "by"
    33     "cannot_undo"
    34     "case"
    35     "cd"
    36     "chapter"
    37     "classes"
    38     "classrel"
    39     "clear_undos"
    40     "coinductive"
    41     "commit"
    42     "constdefs"
    43     "consts"
    44     "consts_code"
    45     "context"
    46     "corollary"
    47     "datatype"
    48     "declare"
    49     "def"
    50     "defaultsort"
    51     "defer"
    52     "defer_recdef"
    53     "defs"
    54     "disable_pr"
    55     "display_drafts"
    56     "domain"
    57     "done"
    58     "enable_pr"
    59     "end"
    60     "exit"
    61     "extract"
    62     "extract_type"
    63     "finalconsts"
    64     "finally"
    65     "find_rewrites"
    66     "fix"
    67     "from"
    68     "full_prf"
    69     "generate_code"
    70     "global"
    71     "have"
    72     "header"
    73     "hence"
    74     "hide"
    75     "inductive"
    76     "inductive_cases"
    77     "init_toplevel"
    78     "instance"
    79     "instantiate"
    80     "interpret"
    81     "interpretation"
    82     "judgment"
    83     "kill"
    84     "kill_thy"
    85     "lemma"
    86     "lemmas"
    87     "let"
    88     "local"
    89     "locale"
    90     "method_setup"
    91     "moreover"
    92     "next"
    93     "nonterminals"
    94     "note"
    95     "obtain"
    96     "oops"
    97     "oracle"
    98     "parse_ast_translation"
    99     "parse_translation"
   100     "pr"
   101     "prefer"
   102     "presume"
   103     "pretty_setmargin"
   104     "prf"
   105     "primrec"
   106     "print_antiquotations"
   107     "print_ast_translation"
   108     "print_attributes"
   109     "print_binds"
   110     "print_cases"
   111     "print_claset"
   112     "print_commands"
   113     "print_context"
   114     "print_drafts"
   115     "print_facts"
   116     "print_induct_rules"
   117     "print_interps"
   118     "print_intros"
   119     "print_locale"
   120     "print_locales"
   121     "print_methods"
   122     "print_rules"
   123     "print_simpset"
   124     "print_syntax"
   125     "print_theorems"
   126     "print_theory"
   127     "print_trans_rules"
   128     "print_translation"
   129     "proof"
   130     "prop"
   131     "pwd"
   132     "qed"
   133     "quickcheck"
   134     "quickcheck_params"
   135     "quit"
   136     "realizability"
   137     "realizers"
   138     "recdef"
   139     "recdef_tc"
   140     "record"
   141     "redo"
   142     "refute"
   143     "refute_params"
   144     "remove_thy"
   145     "rep_datatype"
   146     "sect"
   147     "section"
   148     "setup"
   149     "show"
   150     "sorry"
   151     "specification"
   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     "thms_containing"
   167     "thus"
   168     "token_translation"
   169     "touch_all_thys"
   170     "touch_child_thys"
   171     "touch_thy"
   172     "translations"
   173     "txt"
   174     "txt_raw"
   175     "typ"
   176     "typed_print_translation"
   177     "typedecl"
   178     "typedef"
   179     "types"
   180     "types_code"
   181     "ultimately"
   182     "undo"
   183     "undos_proof"
   184     "update_thy"
   185     "update_thy_only"
   186     "use"
   187     "use_thy"
   188     "use_thy_only"
   189     "using"
   190     "welcome"
   191     "with"
   192     "{"
   193     "}"))
   194 
   195 (defconst isar-keywords-minor
   196   '("actions"
   197     "advanced"
   198     "and"
   199     "assumes"
   200     "begin"
   201     "binder"
   202     "compose"
   203     "concl"
   204     "congs"
   205     "defines"
   206     "distinct"
   207     "files"
   208     "fixes"
   209     "hide_action"
   210     "hints"
   211     "imports"
   212     "in"
   213     "includes"
   214     "induction"
   215     "infix"
   216     "infixl"
   217     "infixr"
   218     "initially"
   219     "inject"
   220     "inputs"
   221     "internals"
   222     "intros"
   223     "is"
   224     "lazy"
   225     "monos"
   226     "morphisms"
   227     "notes"
   228     "open"
   229     "output"
   230     "outputs"
   231     "overloaded"
   232     "permissive"
   233     "post"
   234     "pre"
   235     "rename"
   236     "restrict"
   237     "shows"
   238     "signature"
   239     "states"
   240     "structure"
   241     "to"
   242     "transitions"
   243     "transrel"
   244     "where"))
   245 
   246 (defconst isar-keywords-control
   247   '("ProofGeneral\\.context_thy_only"
   248     "ProofGeneral\\.inform_file_processed"
   249     "ProofGeneral\\.inform_file_retracted"
   250     "ProofGeneral\\.kill_proof"
   251     "ProofGeneral\\.process_pgip"
   252     "ProofGeneral\\.restart"
   253     "ProofGeneral\\.try_context_thy_only"
   254     "ProofGeneral\\.undo"
   255     "cannot_undo"
   256     "clear_undos"
   257     "exit"
   258     "init_toplevel"
   259     "kill"
   260     "quit"
   261     "redo"
   262     "undo"
   263     "undos_proof"))
   264 
   265 (defconst isar-keywords-diag
   266   '("ML"
   267     "ML_command"
   268     "cd"
   269     "commit"
   270     "disable_pr"
   271     "display_drafts"
   272     "enable_pr"
   273     "find_rewrites"
   274     "full_prf"
   275     "header"
   276     "kill_thy"
   277     "pr"
   278     "pretty_setmargin"
   279     "prf"
   280     "print_antiquotations"
   281     "print_attributes"
   282     "print_binds"
   283     "print_cases"
   284     "print_claset"
   285     "print_commands"
   286     "print_context"
   287     "print_drafts"
   288     "print_facts"
   289     "print_induct_rules"
   290     "print_interps"
   291     "print_intros"
   292     "print_locale"
   293     "print_locales"
   294     "print_methods"
   295     "print_rules"
   296     "print_simpset"
   297     "print_syntax"
   298     "print_theorems"
   299     "print_theory"
   300     "print_trans_rules"
   301     "prop"
   302     "pwd"
   303     "quickcheck"
   304     "refute"
   305     "remove_thy"
   306     "term"
   307     "thm"
   308     "thm_deps"
   309     "thms_containing"
   310     "touch_all_thys"
   311     "touch_child_thys"
   312     "touch_thy"
   313     "typ"
   314     "update_thy"
   315     "update_thy_only"
   316     "use"
   317     "use_thy"
   318     "use_thy_only"
   319     "welcome"))
   320 
   321 (defconst isar-keywords-theory-begin
   322   '("theory"))
   323 
   324 (defconst isar-keywords-theory-switch
   325   '("context"))
   326 
   327 (defconst isar-keywords-theory-end
   328   '("end"))
   329 
   330 (defconst isar-keywords-theory-heading
   331   '("chapter"
   332     "section"
   333     "subsection"
   334     "subsubsection"))
   335 
   336 (defconst isar-keywords-theory-decl
   337   '("ML_setup"
   338     "arities"
   339     "automaton"
   340     "axclass"
   341     "axioms"
   342     "classes"
   343     "classrel"
   344     "coinductive"
   345     "constdefs"
   346     "consts"
   347     "consts_code"
   348     "datatype"
   349     "defaultsort"
   350     "defer_recdef"
   351     "defs"
   352     "domain"
   353     "extract"
   354     "extract_type"
   355     "finalconsts"
   356     "generate_code"
   357     "global"
   358     "hide"
   359     "inductive"
   360     "judgment"
   361     "lemmas"
   362     "local"
   363     "locale"
   364     "method_setup"
   365     "nonterminals"
   366     "oracle"
   367     "parse_ast_translation"
   368     "parse_translation"
   369     "primrec"
   370     "print_ast_translation"
   371     "print_translation"
   372     "quickcheck_params"
   373     "realizability"
   374     "realizers"
   375     "recdef"
   376     "record"
   377     "refute_params"
   378     "rep_datatype"
   379     "setup"
   380     "syntax"
   381     "text"
   382     "text_raw"
   383     "theorems"
   384     "token_translation"
   385     "translations"
   386     "typed_print_translation"
   387     "typedecl"
   388     "types"
   389     "types_code"))
   390 
   391 (defconst isar-keywords-theory-script
   392   '("declare"
   393     "inductive_cases"))
   394 
   395 (defconst isar-keywords-theory-goal
   396   '("ax_specification"
   397     "corollary"
   398     "instance"
   399     "interpretation"
   400     "lemma"
   401     "recdef_tc"
   402     "specification"
   403     "theorem"
   404     "typedef"))
   405 
   406 (defconst isar-keywords-qed
   407   '("\\."
   408     "\\.\\."
   409     "by"
   410     "done"
   411     "sorry"))
   412 
   413 (defconst isar-keywords-qed-block
   414   '("qed"))
   415 
   416 (defconst isar-keywords-qed-global
   417   '("oops"))
   418 
   419 (defconst isar-keywords-proof-heading
   420   '("sect"
   421     "subsect"
   422     "subsubsect"))
   423 
   424 (defconst isar-keywords-proof-goal
   425   '("have"
   426     "hence"
   427     "interpret"
   428     "show"
   429     "thus"))
   430 
   431 (defconst isar-keywords-proof-block
   432   '("next"
   433     "proof"))
   434 
   435 (defconst isar-keywords-proof-open
   436   '("{"))
   437 
   438 (defconst isar-keywords-proof-close
   439   '("}"))
   440 
   441 (defconst isar-keywords-proof-chain
   442   '("finally"
   443     "from"
   444     "then"
   445     "ultimately"
   446     "with"))
   447 
   448 (defconst isar-keywords-proof-decl
   449   '("also"
   450     "instantiate"
   451     "let"
   452     "moreover"
   453     "note"
   454     "txt"
   455     "txt_raw"
   456     "using"))
   457 
   458 (defconst isar-keywords-proof-asm
   459   '("assume"
   460     "case"
   461     "def"
   462     "fix"
   463     "presume"))
   464 
   465 (defconst isar-keywords-proof-asm-goal
   466   '("obtain"))
   467 
   468 (defconst isar-keywords-proof-script
   469   '("apply"
   470     "apply_end"
   471     "back"
   472     "defer"
   473     "prefer"))
   474 
   475 (provide 'isar-keywords)