etc/isar-keywords-ZF.el
author wenzelm
Sun Apr 17 19:40:43 2005 +0200 (2005-04-17)
changeset 15762 13d1ec61bc89
parent 15624 484178635bd8
child 16034 6ccd552ee366
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\\.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     "axclass"
    29     "axioms"
    30     "back"
    31     "by"
    32     "cannot_undo"
    33     "case"
    34     "cd"
    35     "chapter"
    36     "classes"
    37     "classrel"
    38     "clear_undos"
    39     "codatatype"
    40     "coinductive"
    41     "commit"
    42     "constdefs"
    43     "consts"
    44     "consts_code"
    45     "context"
    46     "corollary"
    47     "datatype"
    48     "declare"
    49     "def"
    50     "defaultsort"
    51     "defer"
    52     "defs"
    53     "disable_pr"
    54     "display_drafts"
    55     "done"
    56     "enable_pr"
    57     "end"
    58     "exit"
    59     "extract"
    60     "extract_type"
    61     "finalconsts"
    62     "finally"
    63     "find_rewrites"
    64     "fix"
    65     "from"
    66     "full_prf"
    67     "generate_code"
    68     "global"
    69     "have"
    70     "header"
    71     "hence"
    72     "hide"
    73     "inductive"
    74     "inductive_cases"
    75     "init_toplevel"
    76     "instance"
    77     "instantiate"
    78     "interpret"
    79     "interpretation"
    80     "judgment"
    81     "kill"
    82     "kill_thy"
    83     "lemma"
    84     "lemmas"
    85     "let"
    86     "local"
    87     "locale"
    88     "method_setup"
    89     "moreover"
    90     "next"
    91     "no_syntax"
    92     "nonterminals"
    93     "note"
    94     "obtain"
    95     "oops"
    96     "oracle"
    97     "parse_ast_translation"
    98     "parse_translation"
    99     "pr"
   100     "prefer"
   101     "presume"
   102     "pretty_setmargin"
   103     "prf"
   104     "primrec"
   105     "print_antiquotations"
   106     "print_ast_translation"
   107     "print_attributes"
   108     "print_binds"
   109     "print_cases"
   110     "print_claset"
   111     "print_commands"
   112     "print_context"
   113     "print_drafts"
   114     "print_facts"
   115     "print_induct_rules"
   116     "print_interps"
   117     "print_intros"
   118     "print_locale"
   119     "print_locales"
   120     "print_methods"
   121     "print_rules"
   122     "print_simpset"
   123     "print_syntax"
   124     "print_tcset"
   125     "print_theorems"
   126     "print_theory"
   127     "print_trans_rules"
   128     "print_translation"
   129     "proof"
   130     "prop"
   131     "pwd"
   132     "qed"
   133     "quickcheck"
   134     "quickcheck_params"
   135     "quit"
   136     "realizability"
   137     "realizers"
   138     "redo"
   139     "remove_thy"
   140     "rep_datatype"
   141     "sect"
   142     "section"
   143     "setup"
   144     "show"
   145     "sorry"
   146     "subsect"
   147     "subsection"
   148     "subsubsect"
   149     "subsubsection"
   150     "syntax"
   151     "term"
   152     "text"
   153     "text_raw"
   154     "then"
   155     "theorem"
   156     "theorems"
   157     "theory"
   158     "thm"
   159     "thm_deps"
   160     "thms_containing"
   161     "thus"
   162     "token_translation"
   163     "touch_all_thys"
   164     "touch_child_thys"
   165     "touch_thy"
   166     "translations"
   167     "txt"
   168     "txt_raw"
   169     "typ"
   170     "typed_print_translation"
   171     "typedecl"
   172     "types"
   173     "types_code"
   174     "ultimately"
   175     "undo"
   176     "undos_proof"
   177     "update_thy"
   178     "update_thy_only"
   179     "use"
   180     "use_thy"
   181     "use_thy_only"
   182     "using"
   183     "welcome"
   184     "with"
   185     "{"
   186     "}"))
   187 
   188 (defconst isar-keywords-minor
   189   '("advanced"
   190     "and"
   191     "assumes"
   192     "begin"
   193     "binder"
   194     "case_eqns"
   195     "con_defs"
   196     "concl"
   197     "defines"
   198     "domains"
   199     "elimination"
   200     "files"
   201     "fixes"
   202     "imports"
   203     "in"
   204     "includes"
   205     "induction"
   206     "infix"
   207     "infixl"
   208     "infixr"
   209     "intros"
   210     "is"
   211     "monos"
   212     "notes"
   213     "open"
   214     "output"
   215     "overloaded"
   216     "recursor_eqns"
   217     "shows"
   218     "structure"
   219     "type_elims"
   220     "type_intros"
   221     "where"))
   222 
   223 (defconst isar-keywords-control
   224   '("ProofGeneral\\.context_thy_only"
   225     "ProofGeneral\\.inform_file_processed"
   226     "ProofGeneral\\.inform_file_retracted"
   227     "ProofGeneral\\.kill_proof"
   228     "ProofGeneral\\.process_pgip"
   229     "ProofGeneral\\.redo"
   230     "ProofGeneral\\.restart"
   231     "ProofGeneral\\.try_context_thy_only"
   232     "ProofGeneral\\.undo"
   233     "cannot_undo"
   234     "clear_undos"
   235     "exit"
   236     "init_toplevel"
   237     "kill"
   238     "quit"
   239     "redo"
   240     "undo"
   241     "undos_proof"))
   242 
   243 (defconst isar-keywords-diag
   244   '("ML"
   245     "ML_command"
   246     "cd"
   247     "commit"
   248     "disable_pr"
   249     "display_drafts"
   250     "enable_pr"
   251     "find_rewrites"
   252     "full_prf"
   253     "header"
   254     "kill_thy"
   255     "pr"
   256     "pretty_setmargin"
   257     "prf"
   258     "print_antiquotations"
   259     "print_attributes"
   260     "print_binds"
   261     "print_cases"
   262     "print_claset"
   263     "print_commands"
   264     "print_context"
   265     "print_drafts"
   266     "print_facts"
   267     "print_induct_rules"
   268     "print_interps"
   269     "print_intros"
   270     "print_locale"
   271     "print_locales"
   272     "print_methods"
   273     "print_rules"
   274     "print_simpset"
   275     "print_syntax"
   276     "print_tcset"
   277     "print_theorems"
   278     "print_theory"
   279     "print_trans_rules"
   280     "prop"
   281     "pwd"
   282     "quickcheck"
   283     "remove_thy"
   284     "term"
   285     "thm"
   286     "thm_deps"
   287     "thms_containing"
   288     "touch_all_thys"
   289     "touch_child_thys"
   290     "touch_thy"
   291     "typ"
   292     "update_thy"
   293     "update_thy_only"
   294     "use"
   295     "use_thy"
   296     "use_thy_only"
   297     "welcome"))
   298 
   299 (defconst isar-keywords-theory-begin
   300   '("theory"))
   301 
   302 (defconst isar-keywords-theory-switch
   303   '("context"))
   304 
   305 (defconst isar-keywords-theory-end
   306   '("end"))
   307 
   308 (defconst isar-keywords-theory-heading
   309   '("chapter"
   310     "section"
   311     "subsection"
   312     "subsubsection"))
   313 
   314 (defconst isar-keywords-theory-decl
   315   '("ML_setup"
   316     "arities"
   317     "axclass"
   318     "axioms"
   319     "classes"
   320     "classrel"
   321     "codatatype"
   322     "coinductive"
   323     "constdefs"
   324     "consts"
   325     "consts_code"
   326     "datatype"
   327     "defaultsort"
   328     "defs"
   329     "extract"
   330     "extract_type"
   331     "finalconsts"
   332     "generate_code"
   333     "global"
   334     "hide"
   335     "inductive"
   336     "judgment"
   337     "lemmas"
   338     "local"
   339     "locale"
   340     "method_setup"
   341     "no_syntax"
   342     "nonterminals"
   343     "oracle"
   344     "parse_ast_translation"
   345     "parse_translation"
   346     "primrec"
   347     "print_ast_translation"
   348     "print_translation"
   349     "quickcheck_params"
   350     "realizability"
   351     "realizers"
   352     "rep_datatype"
   353     "setup"
   354     "syntax"
   355     "text"
   356     "text_raw"
   357     "theorems"
   358     "token_translation"
   359     "translations"
   360     "typed_print_translation"
   361     "typedecl"
   362     "types"
   363     "types_code"))
   364 
   365 (defconst isar-keywords-theory-script
   366   '("declare"
   367     "inductive_cases"))
   368 
   369 (defconst isar-keywords-theory-goal
   370   '("corollary"
   371     "instance"
   372     "interpretation"
   373     "lemma"
   374     "theorem"))
   375 
   376 (defconst isar-keywords-qed
   377   '("\\."
   378     "\\.\\."
   379     "by"
   380     "done"
   381     "sorry"))
   382 
   383 (defconst isar-keywords-qed-block
   384   '("qed"))
   385 
   386 (defconst isar-keywords-qed-global
   387   '("oops"))
   388 
   389 (defconst isar-keywords-proof-heading
   390   '("sect"
   391     "subsect"
   392     "subsubsect"))
   393 
   394 (defconst isar-keywords-proof-goal
   395   '("have"
   396     "hence"
   397     "interpret"
   398     "show"
   399     "thus"))
   400 
   401 (defconst isar-keywords-proof-block
   402   '("next"
   403     "proof"))
   404 
   405 (defconst isar-keywords-proof-open
   406   '("{"))
   407 
   408 (defconst isar-keywords-proof-close
   409   '("}"))
   410 
   411 (defconst isar-keywords-proof-chain
   412   '("finally"
   413     "from"
   414     "then"
   415     "ultimately"
   416     "with"))
   417 
   418 (defconst isar-keywords-proof-decl
   419   '("also"
   420     "instantiate"
   421     "let"
   422     "moreover"
   423     "note"
   424     "txt"
   425     "txt_raw"
   426     "using"))
   427 
   428 (defconst isar-keywords-proof-asm
   429   '("assume"
   430     "case"
   431     "def"
   432     "fix"
   433     "presume"))
   434 
   435 (defconst isar-keywords-proof-asm-goal
   436   '("obtain"))
   437 
   438 (defconst isar-keywords-proof-script
   439   '("apply"
   440     "apply_end"
   441     "back"
   442     "defer"
   443     "prefer"))
   444 
   445 (provide 'isar-keywords)