etc/isar-keywords-ZF.el
author haftmann
Thu Dec 29 16:10:58 2005 +0100 (2005-12-29)
changeset 18520 428c79932b53
parent 18519 b963eb11b3b4
child 18541 00890455e95f
permissions -rw-r--r--
added atom keyword
     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     "update_thy"
   187     "update_thy_only"
   188     "use"
   189     "use_thy"
   190     "use_thy_only"
   191     "using"
   192     "value"
   193     "welcome"
   194     "with"
   195     "{"
   196     "}"))
   197 
   198 (defconst isar-keywords-minor
   199   '("advanced"
   200     "and"
   201     "assumes"
   202     "atom"
   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     "using"))
   454 
   455 (defconst isar-keywords-proof-asm
   456   '("assume"
   457     "case"
   458     "def"
   459     "fix"
   460     "presume"))
   461 
   462 (defconst isar-keywords-proof-asm-goal
   463   '("guess"
   464     "obtain"))
   465 
   466 (defconst isar-keywords-proof-script
   467   '("apply"
   468     "apply_end"
   469     "back"
   470     "defer"
   471     "prefer"))
   472 
   473 (provide 'isar-keywords)