etc/isar-keywords-ZF.el
author wenzelm
Fri Aug 27 22:09:51 2010 +0200 (2010-08-27)
changeset 38837 b47ee8df7ab4
parent 38708 8915e3ce8655
child 39283 635e09dea465
permissions -rw-r--r--
discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + 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     "ML"
    12     "ML_command"
    13     "ML_prf"
    14     "ML_val"
    15     "ProofGeneral\\.inform_file_processed"
    16     "ProofGeneral\\.inform_file_retracted"
    17     "ProofGeneral\\.kill_proof"
    18     "ProofGeneral\\.pr"
    19     "ProofGeneral\\.process_pgip"
    20     "ProofGeneral\\.restart"
    21     "ProofGeneral\\.undo"
    22     "abbreviation"
    23     "also"
    24     "apply"
    25     "apply_end"
    26     "arities"
    27     "assume"
    28     "attribute_setup"
    29     "axiomatization"
    30     "axioms"
    31     "back"
    32     "by"
    33     "cannot_undo"
    34     "case"
    35     "cd"
    36     "chapter"
    37     "class"
    38     "class_deps"
    39     "classes"
    40     "classrel"
    41     "codatatype"
    42     "code_datatype"
    43     "code_library"
    44     "code_module"
    45     "coinductive"
    46     "commit"
    47     "constdefs"
    48     "consts"
    49     "consts_code"
    50     "context"
    51     "corollary"
    52     "datatype"
    53     "declaration"
    54     "declare"
    55     "def"
    56     "default_sort"
    57     "defer"
    58     "definition"
    59     "defs"
    60     "disable_pr"
    61     "display_drafts"
    62     "done"
    63     "enable_pr"
    64     "end"
    65     "example_proof"
    66     "exit"
    67     "extract"
    68     "extract_type"
    69     "finalconsts"
    70     "finally"
    71     "find_consts"
    72     "find_theorems"
    73     "fix"
    74     "from"
    75     "full_prf"
    76     "guess"
    77     "have"
    78     "header"
    79     "help"
    80     "hence"
    81     "hide_class"
    82     "hide_const"
    83     "hide_fact"
    84     "hide_type"
    85     "inductive"
    86     "inductive_cases"
    87     "init_toplevel"
    88     "instance"
    89     "instantiation"
    90     "interpret"
    91     "interpretation"
    92     "judgment"
    93     "kill"
    94     "kill_thy"
    95     "lemma"
    96     "lemmas"
    97     "let"
    98     "linear_undo"
    99     "local_setup"
   100     "locale"
   101     "method_setup"
   102     "moreover"
   103     "next"
   104     "no_notation"
   105     "no_syntax"
   106     "no_translations"
   107     "no_type_notation"
   108     "nonterminals"
   109     "notation"
   110     "note"
   111     "obtain"
   112     "oops"
   113     "oracle"
   114     "overloading"
   115     "parse_ast_translation"
   116     "parse_translation"
   117     "pr"
   118     "prefer"
   119     "presume"
   120     "pretty_setmargin"
   121     "prf"
   122     "primrec"
   123     "print_abbrevs"
   124     "print_antiquotations"
   125     "print_ast_translation"
   126     "print_attributes"
   127     "print_binds"
   128     "print_cases"
   129     "print_claset"
   130     "print_classes"
   131     "print_codesetup"
   132     "print_commands"
   133     "print_configs"
   134     "print_context"
   135     "print_drafts"
   136     "print_facts"
   137     "print_induct_rules"
   138     "print_interps"
   139     "print_locale"
   140     "print_locales"
   141     "print_methods"
   142     "print_rules"
   143     "print_simpset"
   144     "print_statement"
   145     "print_syntax"
   146     "print_tcset"
   147     "print_theorems"
   148     "print_theory"
   149     "print_trans_rules"
   150     "print_translation"
   151     "proof"
   152     "prop"
   153     "pwd"
   154     "qed"
   155     "quit"
   156     "realizability"
   157     "realizers"
   158     "remove_thy"
   159     "rep_datatype"
   160     "schematic_corollary"
   161     "schematic_lemma"
   162     "schematic_theorem"
   163     "sect"
   164     "section"
   165     "setup"
   166     "show"
   167     "simproc_setup"
   168     "sorry"
   169     "subclass"
   170     "sublocale"
   171     "subsect"
   172     "subsection"
   173     "subsubsect"
   174     "subsubsection"
   175     "syntax"
   176     "term"
   177     "text"
   178     "text_raw"
   179     "then"
   180     "theorem"
   181     "theorems"
   182     "theory"
   183     "thm"
   184     "thm_deps"
   185     "thus"
   186     "thy_deps"
   187     "translations"
   188     "txt"
   189     "txt_raw"
   190     "typ"
   191     "type_notation"
   192     "typed_print_translation"
   193     "typedecl"
   194     "types"
   195     "types_code"
   196     "ultimately"
   197     "undo"
   198     "undos_proof"
   199     "unfolding"
   200     "unused_thms"
   201     "use"
   202     "use_thy"
   203     "using"
   204     "welcome"
   205     "with"
   206     "write"
   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     "pervasive"
   244     "recursor_eqns"
   245     "shows"
   246     "structure"
   247     "type_elims"
   248     "type_intros"
   249     "unchecked"
   250     "uses"
   251     "where"))
   252 
   253 (defconst isar-keywords-control
   254   '("Isabelle\\.command"
   255     "ProofGeneral\\.inform_file_processed"
   256     "ProofGeneral\\.inform_file_retracted"
   257     "ProofGeneral\\.kill_proof"
   258     "ProofGeneral\\.process_pgip"
   259     "ProofGeneral\\.restart"
   260     "ProofGeneral\\.undo"
   261     "cannot_undo"
   262     "disable_pr"
   263     "enable_pr"
   264     "exit"
   265     "init_toplevel"
   266     "kill"
   267     "kill_thy"
   268     "linear_undo"
   269     "quit"
   270     "remove_thy"
   271     "undo"
   272     "undos_proof"
   273     "use_thy"))
   274 
   275 (defconst isar-keywords-diag
   276   '("ML_command"
   277     "ML_val"
   278     "ProofGeneral\\.pr"
   279     "cd"
   280     "class_deps"
   281     "commit"
   282     "display_drafts"
   283     "find_consts"
   284     "find_theorems"
   285     "full_prf"
   286     "header"
   287     "help"
   288     "pr"
   289     "pretty_setmargin"
   290     "prf"
   291     "print_abbrevs"
   292     "print_antiquotations"
   293     "print_attributes"
   294     "print_binds"
   295     "print_cases"
   296     "print_claset"
   297     "print_classes"
   298     "print_codesetup"
   299     "print_commands"
   300     "print_configs"
   301     "print_context"
   302     "print_drafts"
   303     "print_facts"
   304     "print_induct_rules"
   305     "print_interps"
   306     "print_locale"
   307     "print_locales"
   308     "print_methods"
   309     "print_rules"
   310     "print_simpset"
   311     "print_statement"
   312     "print_syntax"
   313     "print_tcset"
   314     "print_theorems"
   315     "print_theory"
   316     "print_trans_rules"
   317     "prop"
   318     "pwd"
   319     "term"
   320     "thm"
   321     "thm_deps"
   322     "thy_deps"
   323     "typ"
   324     "unused_thms"
   325     "welcome"))
   326 
   327 (defconst isar-keywords-theory-begin
   328   '("theory"))
   329 
   330 (defconst isar-keywords-theory-switch
   331   '())
   332 
   333 (defconst isar-keywords-theory-end
   334   '("end"))
   335 
   336 (defconst isar-keywords-theory-heading
   337   '("chapter"
   338     "section"
   339     "subsection"
   340     "subsubsection"))
   341 
   342 (defconst isar-keywords-theory-decl
   343   '("ML"
   344     "abbreviation"
   345     "arities"
   346     "attribute_setup"
   347     "axiomatization"
   348     "axioms"
   349     "class"
   350     "classes"
   351     "classrel"
   352     "codatatype"
   353     "code_datatype"
   354     "code_library"
   355     "code_module"
   356     "coinductive"
   357     "constdefs"
   358     "consts"
   359     "consts_code"
   360     "context"
   361     "datatype"
   362     "declaration"
   363     "declare"
   364     "default_sort"
   365     "definition"
   366     "defs"
   367     "extract"
   368     "extract_type"
   369     "finalconsts"
   370     "hide_class"
   371     "hide_const"
   372     "hide_fact"
   373     "hide_type"
   374     "inductive"
   375     "instantiation"
   376     "judgment"
   377     "lemmas"
   378     "local_setup"
   379     "locale"
   380     "method_setup"
   381     "no_notation"
   382     "no_syntax"
   383     "no_translations"
   384     "no_type_notation"
   385     "nonterminals"
   386     "notation"
   387     "oracle"
   388     "overloading"
   389     "parse_ast_translation"
   390     "parse_translation"
   391     "primrec"
   392     "print_ast_translation"
   393     "print_translation"
   394     "realizability"
   395     "realizers"
   396     "rep_datatype"
   397     "setup"
   398     "simproc_setup"
   399     "syntax"
   400     "text"
   401     "text_raw"
   402     "theorems"
   403     "translations"
   404     "type_notation"
   405     "typed_print_translation"
   406     "typedecl"
   407     "types"
   408     "types_code"
   409     "use"))
   410 
   411 (defconst isar-keywords-theory-script
   412   '("inductive_cases"))
   413 
   414 (defconst isar-keywords-theory-goal
   415   '("corollary"
   416     "example_proof"
   417     "instance"
   418     "interpretation"
   419     "lemma"
   420     "schematic_corollary"
   421     "schematic_lemma"
   422     "schematic_theorem"
   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     "write"))
   478 
   479 (defconst isar-keywords-proof-asm
   480   '("assume"
   481     "case"
   482     "def"
   483     "fix"
   484     "presume"))
   485 
   486 (defconst isar-keywords-proof-asm-goal
   487   '("guess"
   488     "obtain"
   489     "show"
   490     "thus"))
   491 
   492 (defconst isar-keywords-proof-script
   493   '("apply"
   494     "apply_end"
   495     "back"
   496     "defer"
   497     "prefer"))
   498 
   499 (provide 'isar-keywords)