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