etc/isar-keywords-ZF.el
author wenzelm
Wed Mar 12 21:58:48 2014 +0100 (2014-03-12)
changeset 56069 451d5b73f8cf
parent 55385 169e12bbf9a3
child 56146 8453d35e4684
permissions -rw-r--r--
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
added command 'print_ML_antiquotations';
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + 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_file"
    14     "ML_prf"
    15     "ML_val"
    16     "ProofGeneral\\.inform_file_processed"
    17     "ProofGeneral\\.inform_file_retracted"
    18     "ProofGeneral\\.kill_proof"
    19     "ProofGeneral\\.pr"
    20     "ProofGeneral\\.process_pgip"
    21     "ProofGeneral\\.restart"
    22     "ProofGeneral\\.undo"
    23     "abbreviation"
    24     "also"
    25     "apply"
    26     "apply_end"
    27     "assume"
    28     "attribute_setup"
    29     "axiomatization"
    30     "back"
    31     "bundle"
    32     "by"
    33     "cannot_undo"
    34     "case"
    35     "cd"
    36     "chapter"
    37     "class"
    38     "class_deps"
    39     "codatatype"
    40     "code_datatype"
    41     "coinductive"
    42     "commit"
    43     "consts"
    44     "context"
    45     "corollary"
    46     "datatype"
    47     "declaration"
    48     "declare"
    49     "def"
    50     "default_sort"
    51     "defer"
    52     "definition"
    53     "defs"
    54     "disable_pr"
    55     "display_drafts"
    56     "done"
    57     "enable_pr"
    58     "end"
    59     "exit"
    60     "extract"
    61     "extract_type"
    62     "finally"
    63     "find_consts"
    64     "find_theorems"
    65     "fix"
    66     "from"
    67     "full_prf"
    68     "guess"
    69     "have"
    70     "header"
    71     "help"
    72     "hence"
    73     "hide_class"
    74     "hide_const"
    75     "hide_fact"
    76     "hide_type"
    77     "include"
    78     "including"
    79     "inductive"
    80     "inductive_cases"
    81     "init_toplevel"
    82     "instance"
    83     "instantiation"
    84     "interpret"
    85     "interpretation"
    86     "judgment"
    87     "kill"
    88     "kill_thy"
    89     "lemma"
    90     "lemmas"
    91     "let"
    92     "linear_undo"
    93     "local_setup"
    94     "locale"
    95     "locale_deps"
    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_ML_antiquotations"
   120     "print_abbrevs"
   121     "print_antiquotations"
   122     "print_ast_translation"
   123     "print_attributes"
   124     "print_binds"
   125     "print_bundles"
   126     "print_cases"
   127     "print_claset"
   128     "print_classes"
   129     "print_codesetup"
   130     "print_commands"
   131     "print_context"
   132     "print_defn_rules"
   133     "print_dependencies"
   134     "print_facts"
   135     "print_induct_rules"
   136     "print_interps"
   137     "print_locale"
   138     "print_locales"
   139     "print_methods"
   140     "print_options"
   141     "print_rules"
   142     "print_simpset"
   143     "print_state"
   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     "syntax_declaration"
   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     "translations"
   189     "txt"
   190     "txt_raw"
   191     "typ"
   192     "type_notation"
   193     "type_synonym"
   194     "typed_print_translation"
   195     "typedecl"
   196     "ultimately"
   197     "undo"
   198     "undos_proof"
   199     "unfolding"
   200     "unused_thms"
   201     "use_thy"
   202     "using"
   203     "welcome"
   204     "with"
   205     "write"
   206     "{"
   207     "}"))
   208 
   209 (defconst isar-keywords-minor
   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     "includes"
   228     "induction"
   229     "infix"
   230     "infixl"
   231     "infixr"
   232     "intros"
   233     "is"
   234     "keywords"
   235     "monos"
   236     "notes"
   237     "obtains"
   238     "open"
   239     "output"
   240     "overloaded"
   241     "pervasive"
   242     "recursor_eqns"
   243     "shows"
   244     "structure"
   245     "type_elims"
   246     "type_intros"
   247     "unchecked"
   248     "where"))
   249 
   250 (defconst isar-keywords-control
   251   '("Isabelle\\.command"
   252     "ProofGeneral\\.inform_file_processed"
   253     "ProofGeneral\\.inform_file_retracted"
   254     "ProofGeneral\\.kill_proof"
   255     "ProofGeneral\\.pr"
   256     "ProofGeneral\\.process_pgip"
   257     "ProofGeneral\\.restart"
   258     "ProofGeneral\\.undo"
   259     "cannot_undo"
   260     "cd"
   261     "commit"
   262     "disable_pr"
   263     "enable_pr"
   264     "exit"
   265     "init_toplevel"
   266     "kill"
   267     "kill_thy"
   268     "linear_undo"
   269     "pretty_setmargin"
   270     "quit"
   271     "remove_thy"
   272     "undo"
   273     "undos_proof"
   274     "use_thy"))
   275 
   276 (defconst isar-keywords-diag
   277   '("ML_command"
   278     "ML_val"
   279     "class_deps"
   280     "display_drafts"
   281     "find_consts"
   282     "find_theorems"
   283     "full_prf"
   284     "header"
   285     "help"
   286     "locale_deps"
   287     "pr"
   288     "prf"
   289     "print_ML_antiquotations"
   290     "print_abbrevs"
   291     "print_antiquotations"
   292     "print_attributes"
   293     "print_binds"
   294     "print_bundles"
   295     "print_cases"
   296     "print_claset"
   297     "print_classes"
   298     "print_codesetup"
   299     "print_commands"
   300     "print_context"
   301     "print_defn_rules"
   302     "print_dependencies"
   303     "print_facts"
   304     "print_induct_rules"
   305     "print_interps"
   306     "print_locale"
   307     "print_locales"
   308     "print_methods"
   309     "print_options"
   310     "print_rules"
   311     "print_simpset"
   312     "print_state"
   313     "print_statement"
   314     "print_syntax"
   315     "print_tcset"
   316     "print_theorems"
   317     "print_theory"
   318     "print_trans_rules"
   319     "prop"
   320     "pwd"
   321     "term"
   322     "thm"
   323     "thm_deps"
   324     "thy_deps"
   325     "typ"
   326     "unused_thms"
   327     "welcome"))
   328 
   329 (defconst isar-keywords-theory-begin
   330   '("theory"))
   331 
   332 (defconst isar-keywords-theory-switch
   333   '())
   334 
   335 (defconst isar-keywords-theory-end
   336   '("end"))
   337 
   338 (defconst isar-keywords-theory-heading
   339   '("chapter"
   340     "section"
   341     "subsection"
   342     "subsubsection"))
   343 
   344 (defconst isar-keywords-theory-decl
   345   '("ML"
   346     "ML_file"
   347     "abbreviation"
   348     "attribute_setup"
   349     "axiomatization"
   350     "bundle"
   351     "class"
   352     "codatatype"
   353     "code_datatype"
   354     "coinductive"
   355     "consts"
   356     "context"
   357     "datatype"
   358     "declaration"
   359     "declare"
   360     "default_sort"
   361     "definition"
   362     "defs"
   363     "extract"
   364     "extract_type"
   365     "hide_class"
   366     "hide_const"
   367     "hide_fact"
   368     "hide_type"
   369     "inductive"
   370     "instantiation"
   371     "judgment"
   372     "lemmas"
   373     "local_setup"
   374     "locale"
   375     "method_setup"
   376     "no_notation"
   377     "no_syntax"
   378     "no_translations"
   379     "no_type_notation"
   380     "nonterminal"
   381     "notation"
   382     "notepad"
   383     "oracle"
   384     "overloading"
   385     "parse_ast_translation"
   386     "parse_translation"
   387     "primrec"
   388     "print_ast_translation"
   389     "print_translation"
   390     "realizability"
   391     "realizers"
   392     "rep_datatype"
   393     "setup"
   394     "simproc_setup"
   395     "syntax"
   396     "syntax_declaration"
   397     "text"
   398     "text_raw"
   399     "theorems"
   400     "translations"
   401     "type_notation"
   402     "type_synonym"
   403     "typed_print_translation"
   404     "typedecl"))
   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     "include"
   465     "including"
   466     "let"
   467     "moreover"
   468     "note"
   469     "txt"
   470     "txt_raw"
   471     "unfolding"
   472     "using"
   473     "write"))
   474 
   475 (defconst isar-keywords-proof-asm
   476   '("assume"
   477     "case"
   478     "def"
   479     "fix"
   480     "presume"))
   481 
   482 (defconst isar-keywords-proof-asm-goal
   483   '("guess"
   484     "obtain"
   485     "show"
   486     "thus"))
   487 
   488 (defconst isar-keywords-proof-script
   489   '("apply"
   490     "apply_end"
   491     "back"
   492     "defer"
   493     "prefer"))
   494 
   495 (provide 'isar-keywords)