etc/isar-keywords-ZF.el
author wenzelm
Thu Mar 06 12:43:29 2014 +0100 (2014-03-06)
changeset 55952 2f85cc6c27d4
parent 55385 169e12bbf9a3
child 56069 451d5b73f8cf
permissions -rw-r--r--
more rigid type_name demands, based on educated guesses about the tools involved here;
     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_abbrevs"
   120     "print_antiquotations"
   121     "print_ast_translation"
   122     "print_attributes"
   123     "print_binds"
   124     "print_bundles"
   125     "print_cases"
   126     "print_claset"
   127     "print_classes"
   128     "print_codesetup"
   129     "print_commands"
   130     "print_context"
   131     "print_defn_rules"
   132     "print_dependencies"
   133     "print_facts"
   134     "print_induct_rules"
   135     "print_interps"
   136     "print_locale"
   137     "print_locales"
   138     "print_methods"
   139     "print_options"
   140     "print_rules"
   141     "print_simpset"
   142     "print_state"
   143     "print_statement"
   144     "print_syntax"
   145     "print_tcset"
   146     "print_theorems"
   147     "print_theory"
   148     "print_trans_rules"
   149     "print_translation"
   150     "proof"
   151     "prop"
   152     "pwd"
   153     "qed"
   154     "quit"
   155     "realizability"
   156     "realizers"
   157     "remove_thy"
   158     "rep_datatype"
   159     "schematic_corollary"
   160     "schematic_lemma"
   161     "schematic_theorem"
   162     "sect"
   163     "section"
   164     "setup"
   165     "show"
   166     "simproc_setup"
   167     "sorry"
   168     "subclass"
   169     "sublocale"
   170     "subsect"
   171     "subsection"
   172     "subsubsect"
   173     "subsubsection"
   174     "syntax"
   175     "syntax_declaration"
   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     "type_synonym"
   193     "typed_print_translation"
   194     "typedecl"
   195     "ultimately"
   196     "undo"
   197     "undos_proof"
   198     "unfolding"
   199     "unused_thms"
   200     "use_thy"
   201     "using"
   202     "welcome"
   203     "with"
   204     "write"
   205     "{"
   206     "}"))
   207 
   208 (defconst isar-keywords-minor
   209   '("and"
   210     "assumes"
   211     "attach"
   212     "begin"
   213     "binder"
   214     "case_eqns"
   215     "con_defs"
   216     "constrains"
   217     "defines"
   218     "domains"
   219     "elimination"
   220     "fixes"
   221     "for"
   222     "identifier"
   223     "if"
   224     "imports"
   225     "in"
   226     "includes"
   227     "induction"
   228     "infix"
   229     "infixl"
   230     "infixr"
   231     "intros"
   232     "is"
   233     "keywords"
   234     "monos"
   235     "notes"
   236     "obtains"
   237     "open"
   238     "output"
   239     "overloaded"
   240     "pervasive"
   241     "recursor_eqns"
   242     "shows"
   243     "structure"
   244     "type_elims"
   245     "type_intros"
   246     "unchecked"
   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\\.pr"
   255     "ProofGeneral\\.process_pgip"
   256     "ProofGeneral\\.restart"
   257     "ProofGeneral\\.undo"
   258     "cannot_undo"
   259     "cd"
   260     "commit"
   261     "disable_pr"
   262     "enable_pr"
   263     "exit"
   264     "init_toplevel"
   265     "kill"
   266     "kill_thy"
   267     "linear_undo"
   268     "pretty_setmargin"
   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     "class_deps"
   279     "display_drafts"
   280     "find_consts"
   281     "find_theorems"
   282     "full_prf"
   283     "header"
   284     "help"
   285     "locale_deps"
   286     "pr"
   287     "prf"
   288     "print_abbrevs"
   289     "print_antiquotations"
   290     "print_attributes"
   291     "print_binds"
   292     "print_bundles"
   293     "print_cases"
   294     "print_claset"
   295     "print_classes"
   296     "print_codesetup"
   297     "print_commands"
   298     "print_context"
   299     "print_defn_rules"
   300     "print_dependencies"
   301     "print_facts"
   302     "print_induct_rules"
   303     "print_interps"
   304     "print_locale"
   305     "print_locales"
   306     "print_methods"
   307     "print_options"
   308     "print_rules"
   309     "print_simpset"
   310     "print_state"
   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     "ML_file"
   345     "abbreviation"
   346     "attribute_setup"
   347     "axiomatization"
   348     "bundle"
   349     "class"
   350     "codatatype"
   351     "code_datatype"
   352     "coinductive"
   353     "consts"
   354     "context"
   355     "datatype"
   356     "declaration"
   357     "declare"
   358     "default_sort"
   359     "definition"
   360     "defs"
   361     "extract"
   362     "extract_type"
   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 
   404 (defconst isar-keywords-theory-script
   405   '("inductive_cases"))
   406 
   407 (defconst isar-keywords-theory-goal
   408   '("corollary"
   409     "instance"
   410     "interpretation"
   411     "lemma"
   412     "schematic_corollary"
   413     "schematic_lemma"
   414     "schematic_theorem"
   415     "subclass"
   416     "sublocale"
   417     "theorem"))
   418 
   419 (defconst isar-keywords-qed
   420   '("\\."
   421     "\\.\\."
   422     "by"
   423     "done"
   424     "sorry"))
   425 
   426 (defconst isar-keywords-qed-block
   427   '("qed"))
   428 
   429 (defconst isar-keywords-qed-global
   430   '("oops"))
   431 
   432 (defconst isar-keywords-proof-heading
   433   '("sect"
   434     "subsect"
   435     "subsubsect"))
   436 
   437 (defconst isar-keywords-proof-goal
   438   '("have"
   439     "hence"
   440     "interpret"))
   441 
   442 (defconst isar-keywords-proof-block
   443   '("next"
   444     "proof"))
   445 
   446 (defconst isar-keywords-proof-open
   447   '("{"))
   448 
   449 (defconst isar-keywords-proof-close
   450   '("}"))
   451 
   452 (defconst isar-keywords-proof-chain
   453   '("finally"
   454     "from"
   455     "then"
   456     "ultimately"
   457     "with"))
   458 
   459 (defconst isar-keywords-proof-decl
   460   '("ML_prf"
   461     "also"
   462     "include"
   463     "including"
   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)