etc/isar-keywords-ZF.el
author bulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 42023 1bd4b6d1c482
parent 41435 12585dfb86fe
child 44232 d5f689c534c5
permissions -rw-r--r--
adding minimalistic setup and transformation to handle functions as data to enable naive function generation for Quickcheck_Narrowing
     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     "code_library"
    44     "code_module"
    45     "coinductive"
    46     "commit"
    47     "consts"
    48     "consts_code"
    49     "context"
    50     "corollary"
    51     "datatype"
    52     "declaration"
    53     "declare"
    54     "def"
    55     "default_sort"
    56     "defer"
    57     "definition"
    58     "defs"
    59     "disable_pr"
    60     "display_drafts"
    61     "done"
    62     "enable_pr"
    63     "end"
    64     "exit"
    65     "extract"
    66     "extract_type"
    67     "finalconsts"
    68     "finally"
    69     "find_consts"
    70     "find_theorems"
    71     "fix"
    72     "from"
    73     "full_prf"
    74     "guess"
    75     "have"
    76     "header"
    77     "help"
    78     "hence"
    79     "hide_class"
    80     "hide_const"
    81     "hide_fact"
    82     "hide_type"
    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_cases"
   128     "print_claset"
   129     "print_classes"
   130     "print_codesetup"
   131     "print_commands"
   132     "print_configs"
   133     "print_context"
   134     "print_dependencies"
   135     "print_drafts"
   136     "print_facts"
   137     "print_induct_rules"
   138     "print_interps"
   139     "print_locale"
   140     "print_locales"
   141     "print_methods"
   142     "print_rules"
   143     "print_simpset"
   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     "types"
   197     "types_code"
   198     "ultimately"
   199     "undo"
   200     "undos_proof"
   201     "unfolding"
   202     "unused_thms"
   203     "use"
   204     "use_thy"
   205     "using"
   206     "welcome"
   207     "with"
   208     "write"
   209     "{"
   210     "}"))
   211 
   212 (defconst isar-keywords-minor
   213   '("advanced"
   214     "and"
   215     "assumes"
   216     "attach"
   217     "begin"
   218     "binder"
   219     "case_eqns"
   220     "con_defs"
   221     "constrains"
   222     "contains"
   223     "defines"
   224     "domains"
   225     "elimination"
   226     "file"
   227     "fixes"
   228     "for"
   229     "identifier"
   230     "if"
   231     "imports"
   232     "in"
   233     "induction"
   234     "infix"
   235     "infixl"
   236     "infixr"
   237     "intros"
   238     "is"
   239     "monos"
   240     "notes"
   241     "obtains"
   242     "open"
   243     "output"
   244     "overloaded"
   245     "pervasive"
   246     "recursor_eqns"
   247     "shows"
   248     "structure"
   249     "type_elims"
   250     "type_intros"
   251     "unchecked"
   252     "uses"
   253     "where"))
   254 
   255 (defconst isar-keywords-control
   256   '("Isabelle\\.command"
   257     "ProofGeneral\\.inform_file_processed"
   258     "ProofGeneral\\.inform_file_retracted"
   259     "ProofGeneral\\.kill_proof"
   260     "ProofGeneral\\.process_pgip"
   261     "ProofGeneral\\.restart"
   262     "ProofGeneral\\.undo"
   263     "cannot_undo"
   264     "cd"
   265     "commit"
   266     "disable_pr"
   267     "enable_pr"
   268     "exit"
   269     "init_toplevel"
   270     "kill"
   271     "kill_thy"
   272     "linear_undo"
   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     "ProofGeneral\\.pr"
   283     "class_deps"
   284     "display_drafts"
   285     "find_consts"
   286     "find_theorems"
   287     "full_prf"
   288     "header"
   289     "help"
   290     "pr"
   291     "pretty_setmargin"
   292     "prf"
   293     "print_abbrevs"
   294     "print_antiquotations"
   295     "print_attributes"
   296     "print_binds"
   297     "print_cases"
   298     "print_claset"
   299     "print_classes"
   300     "print_codesetup"
   301     "print_commands"
   302     "print_configs"
   303     "print_context"
   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_rules"
   313     "print_simpset"
   314     "print_statement"
   315     "print_syntax"
   316     "print_tcset"
   317     "print_theorems"
   318     "print_theory"
   319     "print_trans_rules"
   320     "prop"
   321     "pwd"
   322     "term"
   323     "thm"
   324     "thm_deps"
   325     "thy_deps"
   326     "typ"
   327     "unused_thms"
   328     "welcome"))
   329 
   330 (defconst isar-keywords-theory-begin
   331   '("theory"))
   332 
   333 (defconst isar-keywords-theory-switch
   334   '())
   335 
   336 (defconst isar-keywords-theory-end
   337   '("end"))
   338 
   339 (defconst isar-keywords-theory-heading
   340   '("chapter"
   341     "section"
   342     "subsection"
   343     "subsubsection"))
   344 
   345 (defconst isar-keywords-theory-decl
   346   '("ML"
   347     "abbreviation"
   348     "arities"
   349     "attribute_setup"
   350     "axiomatization"
   351     "axioms"
   352     "class"
   353     "classes"
   354     "classrel"
   355     "codatatype"
   356     "code_datatype"
   357     "code_library"
   358     "code_module"
   359     "coinductive"
   360     "consts"
   361     "consts_code"
   362     "context"
   363     "datatype"
   364     "declaration"
   365     "declare"
   366     "default_sort"
   367     "definition"
   368     "defs"
   369     "extract"
   370     "extract_type"
   371     "finalconsts"
   372     "hide_class"
   373     "hide_const"
   374     "hide_fact"
   375     "hide_type"
   376     "inductive"
   377     "instantiation"
   378     "judgment"
   379     "lemmas"
   380     "local_setup"
   381     "locale"
   382     "method_setup"
   383     "no_notation"
   384     "no_syntax"
   385     "no_translations"
   386     "no_type_notation"
   387     "nonterminal"
   388     "notation"
   389     "notepad"
   390     "oracle"
   391     "overloading"
   392     "parse_ast_translation"
   393     "parse_translation"
   394     "primrec"
   395     "print_ast_translation"
   396     "print_translation"
   397     "realizability"
   398     "realizers"
   399     "rep_datatype"
   400     "setup"
   401     "simproc_setup"
   402     "syntax"
   403     "syntax_declaration"
   404     "text"
   405     "text_raw"
   406     "theorems"
   407     "translations"
   408     "type_notation"
   409     "type_synonym"
   410     "typed_print_translation"
   411     "typedecl"
   412     "types"
   413     "types_code"
   414     "use"))
   415 
   416 (defconst isar-keywords-theory-script
   417   '("inductive_cases"))
   418 
   419 (defconst isar-keywords-theory-goal
   420   '("corollary"
   421     "instance"
   422     "interpretation"
   423     "lemma"
   424     "schematic_corollary"
   425     "schematic_lemma"
   426     "schematic_theorem"
   427     "subclass"
   428     "sublocale"
   429     "theorem"))
   430 
   431 (defconst isar-keywords-qed
   432   '("\\."
   433     "\\.\\."
   434     "by"
   435     "done"
   436     "sorry"))
   437 
   438 (defconst isar-keywords-qed-block
   439   '("qed"))
   440 
   441 (defconst isar-keywords-qed-global
   442   '("oops"))
   443 
   444 (defconst isar-keywords-proof-heading
   445   '("sect"
   446     "subsect"
   447     "subsubsect"))
   448 
   449 (defconst isar-keywords-proof-goal
   450   '("have"
   451     "hence"
   452     "interpret"))
   453 
   454 (defconst isar-keywords-proof-block
   455   '("next"
   456     "proof"))
   457 
   458 (defconst isar-keywords-proof-open
   459   '("{"))
   460 
   461 (defconst isar-keywords-proof-close
   462   '("}"))
   463 
   464 (defconst isar-keywords-proof-chain
   465   '("finally"
   466     "from"
   467     "then"
   468     "ultimately"
   469     "with"))
   470 
   471 (defconst isar-keywords-proof-decl
   472   '("ML_prf"
   473     "also"
   474     "let"
   475     "moreover"
   476     "note"
   477     "txt"
   478     "txt_raw"
   479     "unfolding"
   480     "using"
   481     "write"))
   482 
   483 (defconst isar-keywords-proof-asm
   484   '("assume"
   485     "case"
   486     "def"
   487     "fix"
   488     "presume"))
   489 
   490 (defconst isar-keywords-proof-asm-goal
   491   '("guess"
   492     "obtain"
   493     "show"
   494     "thus"))
   495 
   496 (defconst isar-keywords-proof-script
   497   '("apply"
   498     "apply_end"
   499     "back"
   500     "defer"
   501     "prefer"))
   502 
   503 (provide 'isar-keywords)