etc/isar-keywords-ZF.el
author wenzelm
Wed Mar 21 17:25:35 2012 +0100 (2012-03-21)
changeset 47066 8a6124d09ff5
parent 47057 12423b36fcc4
child 47069 451fc10a81f3
permissions -rw-r--r--
basic support for nested contexts including bundles;
include multiple bundles;
renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML);
tuned signatures;
     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     "bundle"
    33     "by"
    34     "cannot_undo"
    35     "case"
    36     "cd"
    37     "chapter"
    38     "class"
    39     "class_deps"
    40     "classes"
    41     "classrel"
    42     "codatatype"
    43     "code_datatype"
    44     "coinductive"
    45     "commit"
    46     "consts"
    47     "context"
    48     "context_includes"
    49     "corollary"
    50     "datatype"
    51     "declaration"
    52     "declare"
    53     "def"
    54     "default_sort"
    55     "defer"
    56     "definition"
    57     "defs"
    58     "disable_pr"
    59     "display_drafts"
    60     "done"
    61     "enable_pr"
    62     "end"
    63     "exit"
    64     "extract"
    65     "extract_type"
    66     "finally"
    67     "find_consts"
    68     "find_theorems"
    69     "fix"
    70     "from"
    71     "full_prf"
    72     "guess"
    73     "have"
    74     "header"
    75     "help"
    76     "hence"
    77     "hide_class"
    78     "hide_const"
    79     "hide_fact"
    80     "hide_type"
    81     "include"
    82     "including"
    83     "inductive"
    84     "inductive_cases"
    85     "init_toplevel"
    86     "instance"
    87     "instantiation"
    88     "interpret"
    89     "interpretation"
    90     "judgment"
    91     "kill"
    92     "kill_thy"
    93     "lemma"
    94     "lemmas"
    95     "let"
    96     "linear_undo"
    97     "local_setup"
    98     "locale"
    99     "method_setup"
   100     "moreover"
   101     "next"
   102     "no_notation"
   103     "no_syntax"
   104     "no_translations"
   105     "no_type_notation"
   106     "nonterminal"
   107     "notation"
   108     "note"
   109     "notepad"
   110     "obtain"
   111     "oops"
   112     "oracle"
   113     "overloading"
   114     "parse_ast_translation"
   115     "parse_translation"
   116     "pr"
   117     "prefer"
   118     "presume"
   119     "pretty_setmargin"
   120     "prf"
   121     "primrec"
   122     "print_abbrevs"
   123     "print_antiquotations"
   124     "print_ast_translation"
   125     "print_attributes"
   126     "print_binds"
   127     "print_bundles"
   128     "print_cases"
   129     "print_claset"
   130     "print_classes"
   131     "print_codesetup"
   132     "print_commands"
   133     "print_configs"
   134     "print_context"
   135     "print_dependencies"
   136     "print_drafts"
   137     "print_facts"
   138     "print_induct_rules"
   139     "print_interps"
   140     "print_locale"
   141     "print_locales"
   142     "print_methods"
   143     "print_rules"
   144     "print_simpset"
   145     "print_statement"
   146     "print_syntax"
   147     "print_tcset"
   148     "print_theorems"
   149     "print_theory"
   150     "print_trans_rules"
   151     "print_translation"
   152     "proof"
   153     "prop"
   154     "pwd"
   155     "qed"
   156     "quit"
   157     "realizability"
   158     "realizers"
   159     "remove_thy"
   160     "rep_datatype"
   161     "schematic_corollary"
   162     "schematic_lemma"
   163     "schematic_theorem"
   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     "syntax_declaration"
   178     "term"
   179     "text"
   180     "text_raw"
   181     "then"
   182     "theorem"
   183     "theorems"
   184     "theory"
   185     "thm"
   186     "thm_deps"
   187     "thus"
   188     "thy_deps"
   189     "translations"
   190     "txt"
   191     "txt_raw"
   192     "typ"
   193     "type_notation"
   194     "type_synonym"
   195     "typed_print_translation"
   196     "typedecl"
   197     "ultimately"
   198     "undo"
   199     "undos_proof"
   200     "unfolding"
   201     "unused_thms"
   202     "use"
   203     "use_thy"
   204     "using"
   205     "welcome"
   206     "with"
   207     "write"
   208     "{"
   209     "}"))
   210 
   211 (defconst isar-keywords-minor
   212   '("advanced"
   213     "and"
   214     "assumes"
   215     "attach"
   216     "begin"
   217     "binder"
   218     "case_eqns"
   219     "con_defs"
   220     "constrains"
   221     "defines"
   222     "domains"
   223     "elimination"
   224     "fixes"
   225     "for"
   226     "identifier"
   227     "if"
   228     "imports"
   229     "in"
   230     "induction"
   231     "infix"
   232     "infixl"
   233     "infixr"
   234     "intros"
   235     "is"
   236     "keywords"
   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     "cd"
   263     "commit"
   264     "disable_pr"
   265     "enable_pr"
   266     "exit"
   267     "init_toplevel"
   268     "kill"
   269     "kill_thy"
   270     "linear_undo"
   271     "quit"
   272     "remove_thy"
   273     "undo"
   274     "undos_proof"
   275     "use_thy"))
   276 
   277 (defconst isar-keywords-diag
   278   '("ML_command"
   279     "ML_val"
   280     "ProofGeneral\\.pr"
   281     "class_deps"
   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_bundles"
   296     "print_cases"
   297     "print_claset"
   298     "print_classes"
   299     "print_codesetup"
   300     "print_commands"
   301     "print_configs"
   302     "print_context"
   303     "print_dependencies"
   304     "print_drafts"
   305     "print_facts"
   306     "print_induct_rules"
   307     "print_interps"
   308     "print_locale"
   309     "print_locales"
   310     "print_methods"
   311     "print_rules"
   312     "print_simpset"
   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     "abbreviation"
   347     "arities"
   348     "attribute_setup"
   349     "axiomatization"
   350     "axioms"
   351     "bundle"
   352     "class"
   353     "classes"
   354     "classrel"
   355     "codatatype"
   356     "code_datatype"
   357     "coinductive"
   358     "consts"
   359     "context"
   360     "context_includes"
   361     "datatype"
   362     "declaration"
   363     "declare"
   364     "default_sort"
   365     "definition"
   366     "defs"
   367     "extract"
   368     "extract_type"
   369     "hide_class"
   370     "hide_const"
   371     "hide_fact"
   372     "hide_type"
   373     "inductive"
   374     "instantiation"
   375     "judgment"
   376     "lemmas"
   377     "local_setup"
   378     "locale"
   379     "method_setup"
   380     "no_notation"
   381     "no_syntax"
   382     "no_translations"
   383     "no_type_notation"
   384     "nonterminal"
   385     "notation"
   386     "notepad"
   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     "syntax_declaration"
   401     "text"
   402     "text_raw"
   403     "theorems"
   404     "translations"
   405     "type_notation"
   406     "type_synonym"
   407     "typed_print_translation"
   408     "typedecl"
   409     "use"))
   410 
   411 (defconst isar-keywords-theory-script
   412   '("inductive_cases"))
   413 
   414 (defconst isar-keywords-theory-goal
   415   '("corollary"
   416     "instance"
   417     "interpretation"
   418     "lemma"
   419     "schematic_corollary"
   420     "schematic_lemma"
   421     "schematic_theorem"
   422     "subclass"
   423     "sublocale"
   424     "theorem"))
   425 
   426 (defconst isar-keywords-qed
   427   '("\\."
   428     "\\.\\."
   429     "by"
   430     "done"
   431     "sorry"))
   432 
   433 (defconst isar-keywords-qed-block
   434   '("qed"))
   435 
   436 (defconst isar-keywords-qed-global
   437   '("oops"))
   438 
   439 (defconst isar-keywords-proof-heading
   440   '("sect"
   441     "subsect"
   442     "subsubsect"))
   443 
   444 (defconst isar-keywords-proof-goal
   445   '("have"
   446     "hence"
   447     "interpret"))
   448 
   449 (defconst isar-keywords-proof-block
   450   '("next"
   451     "proof"))
   452 
   453 (defconst isar-keywords-proof-open
   454   '("{"))
   455 
   456 (defconst isar-keywords-proof-close
   457   '("}"))
   458 
   459 (defconst isar-keywords-proof-chain
   460   '("finally"
   461     "from"
   462     "then"
   463     "ultimately"
   464     "with"))
   465 
   466 (defconst isar-keywords-proof-decl
   467   '("ML_prf"
   468     "also"
   469     "include"
   470     "including"
   471     "let"
   472     "moreover"
   473     "note"
   474     "txt"
   475     "txt_raw"
   476     "unfolding"
   477     "using"
   478     "write"))
   479 
   480 (defconst isar-keywords-proof-asm
   481   '("assume"
   482     "case"
   483     "def"
   484     "fix"
   485     "presume"))
   486 
   487 (defconst isar-keywords-proof-asm-goal
   488   '("guess"
   489     "obtain"
   490     "show"
   491     "thus"))
   492 
   493 (defconst isar-keywords-proof-script
   494   '("apply"
   495     "apply_end"
   496     "back"
   497     "defer"
   498     "prefer"))
   499 
   500 (provide 'isar-keywords)