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