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