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