etc/isar-keywords.el
author ballarin
Wed Jun 01 12:30:49 2005 +0200 (2005-06-01)
changeset 16168 adb83939177f
parent 16034 6ccd552ee366
child 16231 91c0a3e253b1
permissions -rw-r--r--
Locales: new element constrains, parameter renaming with syntax,
experimental command instantiate withdrawn.
     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\\.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     "automaton"
    29     "ax_specification"
    30     "axclass"
    31     "axioms"
    32     "back"
    33     "by"
    34     "cannot_undo"
    35     "case"
    36     "cd"
    37     "chapter"
    38     "classes"
    39     "classrel"
    40     "clear_undos"
    41     "coinductive"
    42     "commit"
    43     "constdefs"
    44     "consts"
    45     "consts_code"
    46     "context"
    47     "corollary"
    48     "datatype"
    49     "declare"
    50     "def"
    51     "defaultsort"
    52     "defer"
    53     "defer_recdef"
    54     "defs"
    55     "disable_pr"
    56     "display_drafts"
    57     "domain"
    58     "done"
    59     "enable_pr"
    60     "end"
    61     "exit"
    62     "extract"
    63     "extract_type"
    64     "finalconsts"
    65     "finally"
    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     "interpret"
    80     "interpretation"
    81     "judgment"
    82     "kill"
    83     "kill_thy"
    84     "lemma"
    85     "lemmas"
    86     "let"
    87     "local"
    88     "locale"
    89     "method_setup"
    90     "moreover"
    91     "next"
    92     "no_syntax"
    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_locale"
   119     "print_locales"
   120     "print_methods"
   121     "print_rules"
   122     "print_simpset"
   123     "print_syntax"
   124     "print_theorems"
   125     "print_theory"
   126     "print_trans_rules"
   127     "print_translation"
   128     "proof"
   129     "prop"
   130     "pwd"
   131     "qed"
   132     "quickcheck"
   133     "quickcheck_params"
   134     "quit"
   135     "realizability"
   136     "realizers"
   137     "recdef"
   138     "recdef_tc"
   139     "record"
   140     "redo"
   141     "refute"
   142     "refute_params"
   143     "remove_thy"
   144     "rep_datatype"
   145     "sect"
   146     "section"
   147     "setup"
   148     "show"
   149     "sorry"
   150     "specification"
   151     "subsect"
   152     "subsection"
   153     "subsubsect"
   154     "subsubsection"
   155     "syntax"
   156     "term"
   157     "text"
   158     "text_raw"
   159     "then"
   160     "theorem"
   161     "theorems"
   162     "theory"
   163     "thm"
   164     "thm_deps"
   165     "thms_containing"
   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     "typedef"
   178     "types"
   179     "types_code"
   180     "ultimately"
   181     "undo"
   182     "undos_proof"
   183     "update_thy"
   184     "update_thy_only"
   185     "use"
   186     "use_thy"
   187     "use_thy_only"
   188     "using"
   189     "welcome"
   190     "with"
   191     "{"
   192     "}"))
   193 
   194 (defconst isar-keywords-minor
   195   '("actions"
   196     "advanced"
   197     "and"
   198     "assumes"
   199     "begin"
   200     "binder"
   201     "compose"
   202     "concl"
   203     "congs"
   204     "constrains"
   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\\.redo"
   253     "ProofGeneral\\.restart"
   254     "ProofGeneral\\.try_context_thy_only"
   255     "ProofGeneral\\.undo"
   256     "cannot_undo"
   257     "clear_undos"
   258     "exit"
   259     "init_toplevel"
   260     "kill"
   261     "quit"
   262     "redo"
   263     "undo"
   264     "undos_proof"))
   265 
   266 (defconst isar-keywords-diag
   267   '("ML"
   268     "ML_command"
   269     "cd"
   270     "commit"
   271     "disable_pr"
   272     "display_drafts"
   273     "enable_pr"
   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_locale"
   292     "print_locales"
   293     "print_methods"
   294     "print_rules"
   295     "print_simpset"
   296     "print_syntax"
   297     "print_theorems"
   298     "print_theory"
   299     "print_trans_rules"
   300     "prop"
   301     "pwd"
   302     "quickcheck"
   303     "refute"
   304     "remove_thy"
   305     "term"
   306     "thm"
   307     "thm_deps"
   308     "thms_containing"
   309     "touch_all_thys"
   310     "touch_child_thys"
   311     "touch_thy"
   312     "typ"
   313     "update_thy"
   314     "update_thy_only"
   315     "use"
   316     "use_thy"
   317     "use_thy_only"
   318     "welcome"))
   319 
   320 (defconst isar-keywords-theory-begin
   321   '("theory"))
   322 
   323 (defconst isar-keywords-theory-switch
   324   '("context"))
   325 
   326 (defconst isar-keywords-theory-end
   327   '("end"))
   328 
   329 (defconst isar-keywords-theory-heading
   330   '("chapter"
   331     "section"
   332     "subsection"
   333     "subsubsection"))
   334 
   335 (defconst isar-keywords-theory-decl
   336   '("ML_setup"
   337     "arities"
   338     "automaton"
   339     "axclass"
   340     "axioms"
   341     "classes"
   342     "classrel"
   343     "coinductive"
   344     "constdefs"
   345     "consts"
   346     "consts_code"
   347     "datatype"
   348     "defaultsort"
   349     "defer_recdef"
   350     "defs"
   351     "domain"
   352     "extract"
   353     "extract_type"
   354     "finalconsts"
   355     "generate_code"
   356     "global"
   357     "hide"
   358     "inductive"
   359     "judgment"
   360     "lemmas"
   361     "local"
   362     "locale"
   363     "method_setup"
   364     "no_syntax"
   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     "let"
   451     "moreover"
   452     "note"
   453     "txt"
   454     "txt_raw"
   455     "using"))
   456 
   457 (defconst isar-keywords-proof-asm
   458   '("assume"
   459     "case"
   460     "def"
   461     "fix"
   462     "presume"))
   463 
   464 (defconst isar-keywords-proof-asm-goal
   465   '("obtain"))
   466 
   467 (defconst isar-keywords-proof-script
   468   '("apply"
   469     "apply_end"
   470     "back"
   471     "defer"
   472     "prefer"))
   473 
   474 (provide 'isar-keywords)