etc/isar-keywords.el
author wenzelm
Fri Apr 23 20:47:48 2004 +0200 (2004-04-23)
changeset 14660 934e03881ad6
parent 14508 859b11514537
child 14938 393b75c92c07
permissions -rw-r--r--
updated -- too late for Isabelle2004!
     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     "advanced"
   191     "and"
   192     "assumes"
   193     "binder"
   194     "compose"
   195     "concl"
   196     "congs"
   197     "defines"
   198     "distinct"
   199     "files"
   200     "fixes"
   201     "hide_action"
   202     "hints"
   203     "in"
   204     "includes"
   205     "induction"
   206     "infix"
   207     "infixl"
   208     "infixr"
   209     "initially"
   210     "inject"
   211     "inputs"
   212     "internals"
   213     "intros"
   214     "is"
   215     "lazy"
   216     "monos"
   217     "morphisms"
   218     "notes"
   219     "open"
   220     "output"
   221     "outputs"
   222     "overloaded"
   223     "permissive"
   224     "post"
   225     "pre"
   226     "rename"
   227     "restrict"
   228     "shows"
   229     "signature"
   230     "states"
   231     "structure"
   232     "to"
   233     "transitions"
   234     "transrel"
   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\\.restart"
   243     "ProofGeneral\\.try_context_thy_only"
   244     "ProofGeneral\\.undo"
   245     "cannot_undo"
   246     "clear_undos"
   247     "exit"
   248     "init_toplevel"
   249     "kill"
   250     "quit"
   251     "redo"
   252     "undo"
   253     "undos_proof"))
   254 
   255 (defconst isar-keywords-diag
   256   '("ML"
   257     "ML_command"
   258     "cd"
   259     "commit"
   260     "disable_pr"
   261     "enable_pr"
   262     "full_prf"
   263     "header"
   264     "kill_thy"
   265     "pr"
   266     "pretty_setmargin"
   267     "prf"
   268     "print_antiquotations"
   269     "print_attributes"
   270     "print_binds"
   271     "print_cases"
   272     "print_claset"
   273     "print_commands"
   274     "print_context"
   275     "print_facts"
   276     "print_induct_rules"
   277     "print_intros"
   278     "print_locale"
   279     "print_locales"
   280     "print_methods"
   281     "print_rules"
   282     "print_simpset"
   283     "print_syntax"
   284     "print_theorems"
   285     "print_theory"
   286     "print_trans_rules"
   287     "prop"
   288     "pwd"
   289     "quickcheck"
   290     "refute"
   291     "remove_thy"
   292     "term"
   293     "thm"
   294     "thm_deps"
   295     "thms_containing"
   296     "touch_all_thys"
   297     "touch_child_thys"
   298     "touch_thy"
   299     "typ"
   300     "update_thy"
   301     "update_thy_only"
   302     "use"
   303     "use_thy"
   304     "use_thy_only"
   305     "welcome"))
   306 
   307 (defconst isar-keywords-theory-begin
   308   '("theory"))
   309 
   310 (defconst isar-keywords-theory-switch
   311   '("context"))
   312 
   313 (defconst isar-keywords-theory-end
   314   '("end"))
   315 
   316 (defconst isar-keywords-theory-heading
   317   '("chapter"
   318     "section"
   319     "subsection"
   320     "subsubsection"))
   321 
   322 (defconst isar-keywords-theory-decl
   323   '("ML_setup"
   324     "arities"
   325     "automaton"
   326     "axclass"
   327     "axioms"
   328     "classes"
   329     "classrel"
   330     "coinductive"
   331     "constdefs"
   332     "consts"
   333     "consts_code"
   334     "datatype"
   335     "defaultsort"
   336     "defer_recdef"
   337     "defs"
   338     "domain"
   339     "extract"
   340     "extract_type"
   341     "finalconsts"
   342     "generate_code"
   343     "global"
   344     "hide"
   345     "inductive"
   346     "judgment"
   347     "lemmas"
   348     "local"
   349     "locale"
   350     "method_setup"
   351     "nonterminals"
   352     "oracle"
   353     "parse_ast_translation"
   354     "parse_translation"
   355     "primrec"
   356     "print_ast_translation"
   357     "print_translation"
   358     "quickcheck_params"
   359     "realizability"
   360     "realizers"
   361     "recdef"
   362     "record"
   363     "refute_params"
   364     "rep_datatype"
   365     "setup"
   366     "syntax"
   367     "text"
   368     "text_raw"
   369     "theorems"
   370     "token_translation"
   371     "translations"
   372     "typed_print_translation"
   373     "typedecl"
   374     "types"
   375     "types_code"))
   376 
   377 (defconst isar-keywords-theory-script
   378   '("declare"
   379     "inductive_cases"))
   380 
   381 (defconst isar-keywords-theory-goal
   382   '("ax_specification"
   383     "corollary"
   384     "instance"
   385     "lemma"
   386     "recdef_tc"
   387     "specification"
   388     "theorem"
   389     "typedef"))
   390 
   391 (defconst isar-keywords-qed
   392   '("\\."
   393     "\\.\\."
   394     "by"
   395     "done"
   396     "sorry"))
   397 
   398 (defconst isar-keywords-qed-block
   399   '("qed"))
   400 
   401 (defconst isar-keywords-qed-global
   402   '("oops"))
   403 
   404 (defconst isar-keywords-proof-heading
   405   '("sect"
   406     "subsect"
   407     "subsubsect"))
   408 
   409 (defconst isar-keywords-proof-goal
   410   '("have"
   411     "hence"
   412     "show"
   413     "thus"))
   414 
   415 (defconst isar-keywords-proof-block
   416   '("next"
   417     "proof"))
   418 
   419 (defconst isar-keywords-proof-open
   420   '("{"))
   421 
   422 (defconst isar-keywords-proof-close
   423   '("}"))
   424 
   425 (defconst isar-keywords-proof-chain
   426   '("finally"
   427     "from"
   428     "then"
   429     "ultimately"
   430     "with"))
   431 
   432 (defconst isar-keywords-proof-decl
   433   '("also"
   434     "instantiate"
   435     "let"
   436     "moreover"
   437     "note"
   438     "txt"
   439     "txt_raw"
   440     "using"))
   441 
   442 (defconst isar-keywords-proof-asm
   443   '("assume"
   444     "case"
   445     "def"
   446     "fix"
   447     "presume"))
   448 
   449 (defconst isar-keywords-proof-asm-goal
   450   '("obtain"))
   451 
   452 (defconst isar-keywords-proof-script
   453   '("apply"
   454     "apply_end"
   455     "back"
   456     "defer"
   457     "prefer"))
   458 
   459 (provide 'isar-keywords)