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