etc/isar-keywords-ZF.el
author wenzelm
Mon Jun 24 17:17:17 2013 +0200 (2013-06-24)
changeset 52438 7b5a5116f3af
parent 52437 c88354589b43
child 52439 4cf3f6153eb8
permissions -rw-r--r--
back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from 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     "arities"
    28     "assume"
    29     "attribute_setup"
    30     "axiomatization"
    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     "corollary"
    49     "datatype"
    50     "declaration"
    51     "declare"
    52     "def"
    53     "default_sort"
    54     "defer"
    55     "definition"
    56     "defs"
    57     "disable_pr"
    58     "display_drafts"
    59     "done"
    60     "enable_pr"
    61     "end"
    62     "exit"
    63     "extract"
    64     "extract_type"
    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     "include"
    81     "including"
    82     "inductive"
    83     "inductive_cases"
    84     "init_toplevel"
    85     "instance"
    86     "instantiation"
    87     "interpret"
    88     "interpretation"
    89     "judgment"
    90     "kill"
    91     "kill_thy"
    92     "lemma"
    93     "lemmas"
    94     "let"
    95     "linear_undo"
    96     "local_setup"
    97     "locale"
    98     "locale_deps"
    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_context"
   134     "print_defn_rules"
   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_options"
   144     "print_rules"
   145     "print_simpset"
   146     "print_state"
   147     "print_statement"
   148     "print_syntax"
   149     "print_tcset"
   150     "print_theorems"
   151     "print_theory"
   152     "print_trans_rules"
   153     "print_translation"
   154     "proof"
   155     "prop"
   156     "pwd"
   157     "qed"
   158     "quit"
   159     "realizability"
   160     "realizers"
   161     "remove_thy"
   162     "rep_datatype"
   163     "schematic_corollary"
   164     "schematic_lemma"
   165     "schematic_theorem"
   166     "sect"
   167     "section"
   168     "setup"
   169     "show"
   170     "simproc_setup"
   171     "sorry"
   172     "subclass"
   173     "sublocale"
   174     "subsect"
   175     "subsection"
   176     "subsubsect"
   177     "subsubsection"
   178     "syntax"
   179     "syntax_declaration"
   180     "term"
   181     "text"
   182     "text_raw"
   183     "then"
   184     "theorem"
   185     "theorems"
   186     "theory"
   187     "thm"
   188     "thm_deps"
   189     "thus"
   190     "thy_deps"
   191     "translations"
   192     "txt"
   193     "txt_raw"
   194     "typ"
   195     "type_notation"
   196     "type_synonym"
   197     "typed_print_translation"
   198     "typedecl"
   199     "ultimately"
   200     "undo"
   201     "undos_proof"
   202     "unfolding"
   203     "unused_thms"
   204     "use_thy"
   205     "using"
   206     "welcome"
   207     "with"
   208     "write"
   209     "{"
   210     "}"))
   211 
   212 (defconst isar-keywords-minor
   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     "includes"
   231     "induction"
   232     "infix"
   233     "infixl"
   234     "infixr"
   235     "intros"
   236     "is"
   237     "keywords"
   238     "monos"
   239     "notes"
   240     "obtains"
   241     "open"
   242     "output"
   243     "overloaded"
   244     "pervasive"
   245     "recursor_eqns"
   246     "shows"
   247     "structure"
   248     "type_elims"
   249     "type_intros"
   250     "unchecked"
   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\\.pr"
   259     "ProofGeneral\\.process_pgip"
   260     "ProofGeneral\\.restart"
   261     "ProofGeneral\\.undo"
   262     "cannot_undo"
   263     "cd"
   264     "commit"
   265     "disable_pr"
   266     "enable_pr"
   267     "exit"
   268     "init_toplevel"
   269     "kill"
   270     "kill_thy"
   271     "linear_undo"
   272     "pretty_setmargin"
   273     "quit"
   274     "remove_thy"
   275     "undo"
   276     "undos_proof"
   277     "use_thy"))
   278 
   279 (defconst isar-keywords-diag
   280   '("ML_command"
   281     "ML_val"
   282     "class_deps"
   283     "display_drafts"
   284     "find_consts"
   285     "find_theorems"
   286     "full_prf"
   287     "header"
   288     "help"
   289     "locale_deps"
   290     "pr"
   291     "prf"
   292     "print_abbrevs"
   293     "print_antiquotations"
   294     "print_attributes"
   295     "print_binds"
   296     "print_bundles"
   297     "print_cases"
   298     "print_claset"
   299     "print_classes"
   300     "print_codesetup"
   301     "print_commands"
   302     "print_context"
   303     "print_defn_rules"
   304     "print_dependencies"
   305     "print_drafts"
   306     "print_facts"
   307     "print_induct_rules"
   308     "print_interps"
   309     "print_locale"
   310     "print_locales"
   311     "print_methods"
   312     "print_options"
   313     "print_rules"
   314     "print_simpset"
   315     "print_state"
   316     "print_statement"
   317     "print_syntax"
   318     "print_tcset"
   319     "print_theorems"
   320     "print_theory"
   321     "print_trans_rules"
   322     "prop"
   323     "pwd"
   324     "term"
   325     "thm"
   326     "thm_deps"
   327     "thy_deps"
   328     "typ"
   329     "unused_thms"
   330     "welcome"))
   331 
   332 (defconst isar-keywords-theory-begin
   333   '("theory"))
   334 
   335 (defconst isar-keywords-theory-switch
   336   '())
   337 
   338 (defconst isar-keywords-theory-end
   339   '("end"))
   340 
   341 (defconst isar-keywords-theory-heading
   342   '("chapter"
   343     "section"
   344     "subsection"
   345     "subsubsection"))
   346 
   347 (defconst isar-keywords-theory-decl
   348   '("ML"
   349     "ML_file"
   350     "abbreviation"
   351     "arities"
   352     "attribute_setup"
   353     "axiomatization"
   354     "bundle"
   355     "class"
   356     "classes"
   357     "classrel"
   358     "codatatype"
   359     "code_datatype"
   360     "coinductive"
   361     "consts"
   362     "context"
   363     "datatype"
   364     "declaration"
   365     "declare"
   366     "default_sort"
   367     "definition"
   368     "defs"
   369     "extract"
   370     "extract_type"
   371     "hide_class"
   372     "hide_const"
   373     "hide_fact"
   374     "hide_type"
   375     "inductive"
   376     "instantiation"
   377     "judgment"
   378     "lemmas"
   379     "local_setup"
   380     "locale"
   381     "method_setup"
   382     "no_notation"
   383     "no_syntax"
   384     "no_translations"
   385     "no_type_notation"
   386     "nonterminal"
   387     "notation"
   388     "notepad"
   389     "oracle"
   390     "overloading"
   391     "parse_ast_translation"
   392     "parse_translation"
   393     "primrec"
   394     "print_ast_translation"
   395     "print_translation"
   396     "realizability"
   397     "realizers"
   398     "rep_datatype"
   399     "setup"
   400     "simproc_setup"
   401     "syntax"
   402     "syntax_declaration"
   403     "text"
   404     "text_raw"
   405     "theorems"
   406     "translations"
   407     "type_notation"
   408     "type_synonym"
   409     "typed_print_translation"
   410     "typedecl"))
   411 
   412 (defconst isar-keywords-theory-script
   413   '("inductive_cases"))
   414 
   415 (defconst isar-keywords-theory-goal
   416   '("corollary"
   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     "include"
   471     "including"
   472     "let"
   473     "moreover"
   474     "note"
   475     "txt"
   476     "txt_raw"
   477     "unfolding"
   478     "using"
   479     "write"))
   480 
   481 (defconst isar-keywords-proof-asm
   482   '("assume"
   483     "case"
   484     "def"
   485     "fix"
   486     "presume"))
   487 
   488 (defconst isar-keywords-proof-asm-goal
   489   '("guess"
   490     "obtain"
   491     "show"
   492     "thus"))
   493 
   494 (defconst isar-keywords-proof-script
   495   '("apply"
   496     "apply_end"
   497     "back"
   498     "defer"
   499     "prefer"))
   500 
   501 (provide 'isar-keywords)