etc/isar-keywords-ZF.el
author wenzelm
Tue Feb 26 21:44:06 2002 +0100 (2002-02-26)
changeset 12954 850609c057e2
parent 12935 d697091d1591
child 13364 d3c7d05d8839
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     "using"
   165     "welcome"
   166     "with"
   167     "{"
   168     "}"))
   169 
   170 (defconst isar-keywords-minor
   171   '("and"
   172     "assumes"
   173     "binder"
   174     "case_eqns"
   175     "con_defs"
   176     "concl"
   177     "defines"
   178     "domains"
   179     "elimination"
   180     "files"
   181     "fixes"
   182     "in"
   183     "includes"
   184     "induction"
   185     "infix"
   186     "infixl"
   187     "infixr"
   188     "intros"
   189     "is"
   190     "monos"
   191     "notes"
   192     "output"
   193     "overloaded"
   194     "recursor_eqns"
   195     "shows"
   196     "structure"
   197     "type_elims"
   198     "type_intros"
   199     "where"))
   200 
   201 (defconst isar-keywords-control
   202   '("ProofGeneral\\.context_thy_only"
   203     "ProofGeneral\\.inform_file_processed"
   204     "ProofGeneral\\.inform_file_retracted"
   205     "ProofGeneral\\.kill_proof"
   206     "ProofGeneral\\.restart"
   207     "ProofGeneral\\.try_context_thy_only"
   208     "ProofGeneral\\.undo"
   209     "cannot_undo"
   210     "clear_undos"
   211     "exit"
   212     "init_toplevel"
   213     "kill"
   214     "quit"
   215     "redo"
   216     "undo"
   217     "undos_proof"))
   218 
   219 (defconst isar-keywords-diag
   220   '("ML"
   221     "ML_command"
   222     "cd"
   223     "commit"
   224     "disable_pr"
   225     "enable_pr"
   226     "full_prf"
   227     "header"
   228     "kill_thy"
   229     "pr"
   230     "pretty_setmargin"
   231     "prf"
   232     "print_antiquotations"
   233     "print_attributes"
   234     "print_binds"
   235     "print_cases"
   236     "print_claset"
   237     "print_commands"
   238     "print_context"
   239     "print_facts"
   240     "print_induct_rules"
   241     "print_locale"
   242     "print_locales"
   243     "print_methods"
   244     "print_rules"
   245     "print_simpset"
   246     "print_syntax"
   247     "print_tcset"
   248     "print_theorems"
   249     "print_theory"
   250     "print_trans_rules"
   251     "prop"
   252     "pwd"
   253     "remove_thy"
   254     "term"
   255     "thm"
   256     "thm_deps"
   257     "thms_containing"
   258     "touch_all_thys"
   259     "touch_child_thys"
   260     "touch_thy"
   261     "typ"
   262     "update_thy"
   263     "update_thy_only"
   264     "use"
   265     "use_thy"
   266     "use_thy_only"
   267     "welcome"))
   268 
   269 (defconst isar-keywords-theory-begin
   270   '("theory"))
   271 
   272 (defconst isar-keywords-theory-switch
   273   '("context"))
   274 
   275 (defconst isar-keywords-theory-end
   276   '("end"))
   277 
   278 (defconst isar-keywords-theory-heading
   279   '("chapter"
   280     "section"
   281     "subsection"
   282     "subsubsection"))
   283 
   284 (defconst isar-keywords-theory-decl
   285   '("ML_setup"
   286     "arities"
   287     "axclass"
   288     "axioms"
   289     "classes"
   290     "classrel"
   291     "codatatype"
   292     "coinductive"
   293     "constdefs"
   294     "consts"
   295     "consts_code"
   296     "datatype"
   297     "defaultsort"
   298     "defs"
   299     "generate_code"
   300     "global"
   301     "hide"
   302     "inductive"
   303     "judgment"
   304     "lemmas"
   305     "local"
   306     "locale"
   307     "method_setup"
   308     "nonterminals"
   309     "oracle"
   310     "parse_ast_translation"
   311     "parse_translation"
   312     "primrec"
   313     "print_ast_translation"
   314     "print_translation"
   315     "rep_datatype"
   316     "setup"
   317     "syntax"
   318     "text"
   319     "text_raw"
   320     "theorems"
   321     "token_translation"
   322     "translations"
   323     "typed_print_translation"
   324     "typedecl"
   325     "types"
   326     "types_code"))
   327 
   328 (defconst isar-keywords-theory-script
   329   '("declare"
   330     "inductive_cases"))
   331 
   332 (defconst isar-keywords-theory-goal
   333   '("corollary"
   334     "instance"
   335     "lemma"
   336     "theorem"))
   337 
   338 (defconst isar-keywords-qed
   339   '("\\."
   340     "\\.\\."
   341     "by"
   342     "done"
   343     "sorry"))
   344 
   345 (defconst isar-keywords-qed-block
   346   '("qed"))
   347 
   348 (defconst isar-keywords-qed-global
   349   '("oops"))
   350 
   351 (defconst isar-keywords-proof-heading
   352   '("sect"
   353     "subsect"
   354     "subsubsect"))
   355 
   356 (defconst isar-keywords-proof-goal
   357   '("have"
   358     "hence"
   359     "show"
   360     "thus"))
   361 
   362 (defconst isar-keywords-proof-block
   363   '("next"
   364     "proof"))
   365 
   366 (defconst isar-keywords-proof-open
   367   '("{"))
   368 
   369 (defconst isar-keywords-proof-close
   370   '("}"))
   371 
   372 (defconst isar-keywords-proof-chain
   373   '("finally"
   374     "from"
   375     "then"
   376     "ultimately"
   377     "with"))
   378 
   379 (defconst isar-keywords-proof-decl
   380   '("also"
   381     "let"
   382     "moreover"
   383     "note"
   384     "txt"
   385     "txt_raw"
   386     "using"))
   387 
   388 (defconst isar-keywords-proof-asm
   389   '("assume"
   390     "case"
   391     "def"
   392     "fix"
   393     "presume"))
   394 
   395 (defconst isar-keywords-proof-asm-goal
   396   '("obtain"))
   397 
   398 (defconst isar-keywords-proof-script
   399   '("apply"
   400     "apply_end"
   401     "back"
   402     "defer"
   403     "prefer"))
   404 
   405 (provide 'isar-keywords)