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