etc/isar-keywords-ZF.el
author ballarin
Tue Sep 29 22:15:54 2009 +0200 (2009-09-29)
changeset 32804 ca430e6aee1c
parent 31130 94cb206f8f6a
child 33198 bfb9a790d1e7
permissions -rw-r--r--
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
     4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     5 ;;
     6 
     7 (defconst isar-keywords-major
     8   '("\\."
     9     "\\.\\."
    10     "Isabelle\\.command"
    11     "Isar\\.begin_document"
    12     "Isar\\.command"
    13     "Isar\\.define_command"
    14     "Isar\\.edit_document"
    15     "Isar\\.end_document"
    16     "Isar\\.insert"
    17     "Isar\\.remove"
    18     "ML"
    19     "ML_command"
    20     "ML_prf"
    21     "ML_val"
    22     "ProofGeneral\\.inform_file_processed"
    23     "ProofGeneral\\.inform_file_retracted"
    24     "ProofGeneral\\.kill_proof"
    25     "ProofGeneral\\.process_pgip"
    26     "ProofGeneral\\.restart"
    27     "ProofGeneral\\.undo"
    28     "abbreviation"
    29     "also"
    30     "apply"
    31     "apply_end"
    32     "arities"
    33     "assume"
    34     "attribute_setup"
    35     "axclass"
    36     "axiomatization"
    37     "axioms"
    38     "back"
    39     "by"
    40     "cannot_undo"
    41     "case"
    42     "cd"
    43     "chapter"
    44     "class"
    45     "class_deps"
    46     "classes"
    47     "classrel"
    48     "codatatype"
    49     "code_datatype"
    50     "code_library"
    51     "code_module"
    52     "coinductive"
    53     "commit"
    54     "constdefs"
    55     "consts"
    56     "consts_code"
    57     "context"
    58     "corollary"
    59     "datatype"
    60     "declaration"
    61     "declare"
    62     "def"
    63     "defaultsort"
    64     "defer"
    65     "definition"
    66     "defs"
    67     "disable_pr"
    68     "display_drafts"
    69     "done"
    70     "enable_pr"
    71     "end"
    72     "exit"
    73     "extract"
    74     "extract_type"
    75     "finalconsts"
    76     "finally"
    77     "find_consts"
    78     "find_theorems"
    79     "fix"
    80     "from"
    81     "full_prf"
    82     "global"
    83     "guess"
    84     "have"
    85     "header"
    86     "help"
    87     "hence"
    88     "hide"
    89     "inductive"
    90     "inductive_cases"
    91     "init_toplevel"
    92     "instance"
    93     "instantiation"
    94     "interpret"
    95     "interpretation"
    96     "judgment"
    97     "kill"
    98     "kill_thy"
    99     "lemma"
   100     "lemmas"
   101     "let"
   102     "linear_undo"
   103     "local"
   104     "local_setup"
   105     "locale"
   106     "method_setup"
   107     "moreover"
   108     "next"
   109     "no_notation"
   110     "no_syntax"
   111     "no_translations"
   112     "nonterminals"
   113     "notation"
   114     "note"
   115     "obtain"
   116     "oops"
   117     "oracle"
   118     "overloading"
   119     "parse_ast_translation"
   120     "parse_translation"
   121     "pr"
   122     "prefer"
   123     "presume"
   124     "pretty_setmargin"
   125     "prf"
   126     "primrec"
   127     "print_abbrevs"
   128     "print_antiquotations"
   129     "print_ast_translation"
   130     "print_attributes"
   131     "print_binds"
   132     "print_cases"
   133     "print_claset"
   134     "print_classes"
   135     "print_codesetup"
   136     "print_commands"
   137     "print_configs"
   138     "print_context"
   139     "print_drafts"
   140     "print_facts"
   141     "print_induct_rules"
   142     "print_interps"
   143     "print_locale"
   144     "print_locales"
   145     "print_methods"
   146     "print_rules"
   147     "print_simpset"
   148     "print_statement"
   149     "print_syntax"
   150     "print_tcset"
   151     "print_theorems"
   152     "print_theory"
   153     "print_trans_rules"
   154     "print_translation"
   155     "proof"
   156     "prop"
   157     "pwd"
   158     "qed"
   159     "quit"
   160     "realizability"
   161     "realizers"
   162     "remove_thy"
   163     "rep_datatype"
   164     "sect"
   165     "section"
   166     "setup"
   167     "show"
   168     "simproc_setup"
   169     "sorry"
   170     "subclass"
   171     "sublocale"
   172     "subsect"
   173     "subsection"
   174     "subsubsect"
   175     "subsubsection"
   176     "syntax"
   177     "term"
   178     "text"
   179     "text_raw"
   180     "then"
   181     "theorem"
   182     "theorems"
   183     "theory"
   184     "thm"
   185     "thm_deps"
   186     "thus"
   187     "thy_deps"
   188     "touch_thy"
   189     "translations"
   190     "txt"
   191     "txt_raw"
   192     "typ"
   193     "typed_print_translation"
   194     "typedecl"
   195     "types"
   196     "types_code"
   197     "ultimately"
   198     "undo"
   199     "undos_proof"
   200     "unfolding"
   201     "unused_thms"
   202     "use"
   203     "use_thy"
   204     "using"
   205     "welcome"
   206     "with"
   207     "{"
   208     "}"))
   209 
   210 (defconst isar-keywords-minor
   211   '("advanced"
   212     "and"
   213     "assumes"
   214     "attach"
   215     "begin"
   216     "binder"
   217     "case_eqns"
   218     "con_defs"
   219     "constrains"
   220     "contains"
   221     "defines"
   222     "domains"
   223     "elimination"
   224     "file"
   225     "fixes"
   226     "for"
   227     "identifier"
   228     "if"
   229     "imports"
   230     "in"
   231     "induction"
   232     "infix"
   233     "infixl"
   234     "infixr"
   235     "intros"
   236     "is"
   237     "monos"
   238     "notes"
   239     "obtains"
   240     "open"
   241     "output"
   242     "overloaded"
   243     "recursor_eqns"
   244     "shows"
   245     "structure"
   246     "type_elims"
   247     "type_intros"
   248     "unchecked"
   249     "uses"
   250     "where"))
   251 
   252 (defconst isar-keywords-control
   253   '("Isabelle\\.command"
   254     "Isar\\.begin_document"
   255     "Isar\\.command"
   256     "Isar\\.define_command"
   257     "Isar\\.edit_document"
   258     "Isar\\.end_document"
   259     "Isar\\.insert"
   260     "Isar\\.remove"
   261     "ProofGeneral\\.inform_file_processed"
   262     "ProofGeneral\\.inform_file_retracted"
   263     "ProofGeneral\\.kill_proof"
   264     "ProofGeneral\\.process_pgip"
   265     "ProofGeneral\\.restart"
   266     "ProofGeneral\\.undo"
   267     "cannot_undo"
   268     "exit"
   269     "init_toplevel"
   270     "kill"
   271     "linear_undo"
   272     "quit"
   273     "undo"
   274     "undos_proof"))
   275 
   276 (defconst isar-keywords-diag
   277   '("ML_command"
   278     "ML_val"
   279     "cd"
   280     "class_deps"
   281     "commit"
   282     "disable_pr"
   283     "display_drafts"
   284     "enable_pr"
   285     "find_consts"
   286     "find_theorems"
   287     "full_prf"
   288     "header"
   289     "help"
   290     "kill_thy"
   291     "pr"
   292     "pretty_setmargin"
   293     "prf"
   294     "print_abbrevs"
   295     "print_antiquotations"
   296     "print_attributes"
   297     "print_binds"
   298     "print_cases"
   299     "print_claset"
   300     "print_classes"
   301     "print_codesetup"
   302     "print_commands"
   303     "print_configs"
   304     "print_context"
   305     "print_drafts"
   306     "print_facts"
   307     "print_induct_rules"
   308     "print_interps"
   309     "print_locale"
   310     "print_locales"
   311     "print_methods"
   312     "print_rules"
   313     "print_simpset"
   314     "print_statement"
   315     "print_syntax"
   316     "print_tcset"
   317     "print_theorems"
   318     "print_theory"
   319     "print_trans_rules"
   320     "prop"
   321     "pwd"
   322     "remove_thy"
   323     "term"
   324     "thm"
   325     "thm_deps"
   326     "thy_deps"
   327     "touch_thy"
   328     "typ"
   329     "unused_thms"
   330     "use_thy"
   331     "welcome"))
   332 
   333 (defconst isar-keywords-theory-begin
   334   '("theory"))
   335 
   336 (defconst isar-keywords-theory-switch
   337   '())
   338 
   339 (defconst isar-keywords-theory-end
   340   '("end"))
   341 
   342 (defconst isar-keywords-theory-heading
   343   '("chapter"
   344     "section"
   345     "subsection"
   346     "subsubsection"))
   347 
   348 (defconst isar-keywords-theory-decl
   349   '("ML"
   350     "abbreviation"
   351     "arities"
   352     "attribute_setup"
   353     "axclass"
   354     "axiomatization"
   355     "axioms"
   356     "class"
   357     "classes"
   358     "classrel"
   359     "codatatype"
   360     "code_datatype"
   361     "code_library"
   362     "code_module"
   363     "coinductive"
   364     "constdefs"
   365     "consts"
   366     "consts_code"
   367     "context"
   368     "datatype"
   369     "declaration"
   370     "declare"
   371     "defaultsort"
   372     "definition"
   373     "defs"
   374     "extract"
   375     "extract_type"
   376     "finalconsts"
   377     "global"
   378     "hide"
   379     "inductive"
   380     "instantiation"
   381     "judgment"
   382     "lemmas"
   383     "local"
   384     "local_setup"
   385     "locale"
   386     "method_setup"
   387     "no_notation"
   388     "no_syntax"
   389     "no_translations"
   390     "nonterminals"
   391     "notation"
   392     "oracle"
   393     "overloading"
   394     "parse_ast_translation"
   395     "parse_translation"
   396     "primrec"
   397     "print_ast_translation"
   398     "print_translation"
   399     "realizability"
   400     "realizers"
   401     "rep_datatype"
   402     "setup"
   403     "simproc_setup"
   404     "syntax"
   405     "text"
   406     "text_raw"
   407     "theorems"
   408     "translations"
   409     "typed_print_translation"
   410     "typedecl"
   411     "types"
   412     "types_code"
   413     "use"))
   414 
   415 (defconst isar-keywords-theory-script
   416   '("inductive_cases"))
   417 
   418 (defconst isar-keywords-theory-goal
   419   '("corollary"
   420     "instance"
   421     "interpretation"
   422     "lemma"
   423     "subclass"
   424     "sublocale"
   425     "theorem"))
   426 
   427 (defconst isar-keywords-qed
   428   '("\\."
   429     "\\.\\."
   430     "by"
   431     "done"
   432     "sorry"))
   433 
   434 (defconst isar-keywords-qed-block
   435   '("qed"))
   436 
   437 (defconst isar-keywords-qed-global
   438   '("oops"))
   439 
   440 (defconst isar-keywords-proof-heading
   441   '("sect"
   442     "subsect"
   443     "subsubsect"))
   444 
   445 (defconst isar-keywords-proof-goal
   446   '("have"
   447     "hence"
   448     "interpret"))
   449 
   450 (defconst isar-keywords-proof-block
   451   '("next"
   452     "proof"))
   453 
   454 (defconst isar-keywords-proof-open
   455   '("{"))
   456 
   457 (defconst isar-keywords-proof-close
   458   '("}"))
   459 
   460 (defconst isar-keywords-proof-chain
   461   '("finally"
   462     "from"
   463     "then"
   464     "ultimately"
   465     "with"))
   466 
   467 (defconst isar-keywords-proof-decl
   468   '("ML_prf"
   469     "also"
   470     "let"
   471     "moreover"
   472     "note"
   473     "txt"
   474     "txt_raw"
   475     "unfolding"
   476     "using"))
   477 
   478 (defconst isar-keywords-proof-asm
   479   '("assume"
   480     "case"
   481     "def"
   482     "fix"
   483     "presume"))
   484 
   485 (defconst isar-keywords-proof-asm-goal
   486   '("guess"
   487     "obtain"
   488     "show"
   489     "thus"))
   490 
   491 (defconst isar-keywords-proof-script
   492   '("apply"
   493     "apply_end"
   494     "back"
   495     "defer"
   496     "prefer"))
   497 
   498 (provide 'isar-keywords)