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