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