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