etc/isar-keywords-ZF.el
author wenzelm
Wed Oct 17 11:53:35 2007 +0200 (2007-10-17)
changeset 25065 25696ce6dff1
parent 24945 2c27817065bc
child 25516 ad25835675b9
permissions -rw-r--r--
updated;
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
     4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     5 ;;
     6 ;; $Id$
     7 ;;
     8 
     9 (defconst isar-keywords-major
    10   '("\\."
    11     "\\.\\."
    12     "ML"
    13     "ML_command"
    14     "ML_setup"
    15     "ProofGeneral\\.inform_file_processed"
    16     "ProofGeneral\\.inform_file_retracted"
    17     "ProofGeneral\\.kill_proof"
    18     "ProofGeneral\\.process_pgip"
    19     "ProofGeneral\\.restart"
    20     "ProofGeneral\\.undo"
    21     "abbreviation"
    22     "also"
    23     "apply"
    24     "apply_end"
    25     "arities"
    26     "assume"
    27     "axclass"
    28     "axiomatization"
    29     "axioms"
    30     "back"
    31     "by"
    32     "cannot_undo"
    33     "case"
    34     "cd"
    35     "chapter"
    36     "class"
    37     "class_deps"
    38     "classes"
    39     "classrel"
    40     "codatatype"
    41     "code_datatype"
    42     "code_library"
    43     "code_module"
    44     "coinductive"
    45     "commit"
    46     "constdefs"
    47     "consts"
    48     "consts_code"
    49     "context"
    50     "corollary"
    51     "datatype"
    52     "declaration"
    53     "declare"
    54     "def"
    55     "defaultsort"
    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_theorems"
    70     "fix"
    71     "from"
    72     "full_prf"
    73     "global"
    74     "guess"
    75     "have"
    76     "header"
    77     "help"
    78     "hence"
    79     "hide"
    80     "inductive"
    81     "inductive_cases"
    82     "init_toplevel"
    83     "instance"
    84     "instance_proof"
    85     "instantiation"
    86     "interpret"
    87     "interpretation"
    88     "invoke"
    89     "judgment"
    90     "kill"
    91     "kill_thy"
    92     "lemma"
    93     "lemmas"
    94     "let"
    95     "local"
    96     "locale"
    97     "method_setup"
    98     "moreover"
    99     "next"
   100     "no_notation"
   101     "no_syntax"
   102     "no_translations"
   103     "nonterminals"
   104     "notation"
   105     "note"
   106     "obtain"
   107     "oops"
   108     "oracle"
   109     "parse_ast_translation"
   110     "parse_translation"
   111     "pr"
   112     "prefer"
   113     "presume"
   114     "pretty_setmargin"
   115     "prf"
   116     "primrec"
   117     "print_abbrevs"
   118     "print_antiquotations"
   119     "print_ast_translation"
   120     "print_attributes"
   121     "print_binds"
   122     "print_cases"
   123     "print_claset"
   124     "print_classes"
   125     "print_codesetup"
   126     "print_commands"
   127     "print_configs"
   128     "print_context"
   129     "print_drafts"
   130     "print_facts"
   131     "print_induct_rules"
   132     "print_interps"
   133     "print_locale"
   134     "print_locales"
   135     "print_methods"
   136     "print_rules"
   137     "print_simpset"
   138     "print_statement"
   139     "print_syntax"
   140     "print_tcset"
   141     "print_theorems"
   142     "print_theory"
   143     "print_trans_rules"
   144     "print_translation"
   145     "proof"
   146     "prop"
   147     "pwd"
   148     "qed"
   149     "quickcheck"
   150     "quickcheck_params"
   151     "quit"
   152     "realizability"
   153     "realizers"
   154     "redo"
   155     "remove_thy"
   156     "rep_datatype"
   157     "sect"
   158     "section"
   159     "setup"
   160     "show"
   161     "simproc_setup"
   162     "sorry"
   163     "subclass"
   164     "subsect"
   165     "subsection"
   166     "subsubsect"
   167     "subsubsection"
   168     "syntax"
   169     "term"
   170     "text"
   171     "text_raw"
   172     "then"
   173     "theorem"
   174     "theorems"
   175     "theory"
   176     "thm"
   177     "thm_deps"
   178     "thus"
   179     "thy_deps"
   180     "token_translation"
   181     "touch_child_thys"
   182     "touch_thy"
   183     "translations"
   184     "txt"
   185     "txt_raw"
   186     "typ"
   187     "typed_print_translation"
   188     "typedecl"
   189     "types"
   190     "types_code"
   191     "ultimately"
   192     "undo"
   193     "undos_proof"
   194     "unfolding"
   195     "use"
   196     "use_thy"
   197     "using"
   198     "value"
   199     "welcome"
   200     "with"
   201     "{"
   202     "}"))
   203 
   204 (defconst isar-keywords-minor
   205   '("advanced"
   206     "and"
   207     "assumes"
   208     "attach"
   209     "begin"
   210     "binder"
   211     "case_eqns"
   212     "con_defs"
   213     "concl"
   214     "constrains"
   215     "contains"
   216     "defines"
   217     "domains"
   218     "elimination"
   219     "file"
   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     "monos"
   234     "notes"
   235     "obtains"
   236     "open"
   237     "output"
   238     "overloaded"
   239     "recursor_eqns"
   240     "shows"
   241     "structure"
   242     "type_elims"
   243     "type_intros"
   244     "unchecked"
   245     "uses"
   246     "where"))
   247 
   248 (defconst isar-keywords-control
   249   '("ProofGeneral\\.inform_file_processed"
   250     "ProofGeneral\\.inform_file_retracted"
   251     "ProofGeneral\\.kill_proof"
   252     "ProofGeneral\\.process_pgip"
   253     "ProofGeneral\\.restart"
   254     "ProofGeneral\\.undo"
   255     "cannot_undo"
   256     "exit"
   257     "init_toplevel"
   258     "kill"
   259     "quit"
   260     "redo"
   261     "undo"
   262     "undos_proof"))
   263 
   264 (defconst isar-keywords-diag
   265   '("ML"
   266     "ML_command"
   267     "cd"
   268     "class_deps"
   269     "commit"
   270     "disable_pr"
   271     "display_drafts"
   272     "enable_pr"
   273     "find_theorems"
   274     "full_prf"
   275     "header"
   276     "help"
   277     "kill_thy"
   278     "pr"
   279     "pretty_setmargin"
   280     "prf"
   281     "print_abbrevs"
   282     "print_antiquotations"
   283     "print_attributes"
   284     "print_binds"
   285     "print_cases"
   286     "print_claset"
   287     "print_classes"
   288     "print_codesetup"
   289     "print_commands"
   290     "print_configs"
   291     "print_context"
   292     "print_drafts"
   293     "print_facts"
   294     "print_induct_rules"
   295     "print_interps"
   296     "print_locale"
   297     "print_locales"
   298     "print_methods"
   299     "print_rules"
   300     "print_simpset"
   301     "print_statement"
   302     "print_syntax"
   303     "print_tcset"
   304     "print_theorems"
   305     "print_theory"
   306     "print_trans_rules"
   307     "prop"
   308     "pwd"
   309     "quickcheck"
   310     "remove_thy"
   311     "term"
   312     "thm"
   313     "thm_deps"
   314     "thy_deps"
   315     "touch_child_thys"
   316     "touch_thy"
   317     "typ"
   318     "use"
   319     "use_thy"
   320     "value"
   321     "welcome"))
   322 
   323 (defconst isar-keywords-theory-begin
   324   '("theory"))
   325 
   326 (defconst isar-keywords-theory-switch
   327   '())
   328 
   329 (defconst isar-keywords-theory-end
   330   '("end"))
   331 
   332 (defconst isar-keywords-theory-heading
   333   '("chapter"
   334     "section"
   335     "subsection"
   336     "subsubsection"))
   337 
   338 (defconst isar-keywords-theory-decl
   339   '("ML_setup"
   340     "abbreviation"
   341     "arities"
   342     "axclass"
   343     "axiomatization"
   344     "axioms"
   345     "class"
   346     "classes"
   347     "classrel"
   348     "codatatype"
   349     "code_datatype"
   350     "code_library"
   351     "code_module"
   352     "coinductive"
   353     "constdefs"
   354     "consts"
   355     "consts_code"
   356     "context"
   357     "datatype"
   358     "declaration"
   359     "declare"
   360     "defaultsort"
   361     "definition"
   362     "defs"
   363     "extract"
   364     "extract_type"
   365     "finalconsts"
   366     "global"
   367     "hide"
   368     "inductive"
   369     "instantiation"
   370     "judgment"
   371     "lemmas"
   372     "local"
   373     "locale"
   374     "method_setup"
   375     "no_notation"
   376     "no_syntax"
   377     "no_translations"
   378     "nonterminals"
   379     "notation"
   380     "oracle"
   381     "parse_ast_translation"
   382     "parse_translation"
   383     "primrec"
   384     "print_ast_translation"
   385     "print_translation"
   386     "quickcheck_params"
   387     "realizability"
   388     "realizers"
   389     "rep_datatype"
   390     "setup"
   391     "simproc_setup"
   392     "syntax"
   393     "text"
   394     "text_raw"
   395     "theorems"
   396     "token_translation"
   397     "translations"
   398     "typed_print_translation"
   399     "typedecl"
   400     "types"
   401     "types_code"))
   402 
   403 (defconst isar-keywords-theory-script
   404   '("inductive_cases"))
   405 
   406 (defconst isar-keywords-theory-goal
   407   '("corollary"
   408     "instance"
   409     "instance_proof"
   410     "interpretation"
   411     "lemma"
   412     "subclass"
   413     "theorem"))
   414 
   415 (defconst isar-keywords-qed
   416   '("\\."
   417     "\\.\\."
   418     "by"
   419     "done"
   420     "sorry"))
   421 
   422 (defconst isar-keywords-qed-block
   423   '("qed"))
   424 
   425 (defconst isar-keywords-qed-global
   426   '("oops"))
   427 
   428 (defconst isar-keywords-proof-heading
   429   '("sect"
   430     "subsect"
   431     "subsubsect"))
   432 
   433 (defconst isar-keywords-proof-goal
   434   '("have"
   435     "hence"
   436     "interpret"
   437     "invoke"))
   438 
   439 (defconst isar-keywords-proof-block
   440   '("next"
   441     "proof"))
   442 
   443 (defconst isar-keywords-proof-open
   444   '("{"))
   445 
   446 (defconst isar-keywords-proof-close
   447   '("}"))
   448 
   449 (defconst isar-keywords-proof-chain
   450   '("finally"
   451     "from"
   452     "then"
   453     "ultimately"
   454     "with"))
   455 
   456 (defconst isar-keywords-proof-decl
   457   '("also"
   458     "let"
   459     "moreover"
   460     "note"
   461     "txt"
   462     "txt_raw"
   463     "unfolding"
   464     "using"))
   465 
   466 (defconst isar-keywords-proof-asm
   467   '("assume"
   468     "case"
   469     "def"
   470     "fix"
   471     "presume"))
   472 
   473 (defconst isar-keywords-proof-asm-goal
   474   '("guess"
   475     "obtain"
   476     "show"
   477     "thus"))
   478 
   479 (defconst isar-keywords-proof-script
   480   '("apply"
   481     "apply_end"
   482     "back"
   483     "defer"
   484     "prefer"))
   485 
   486 (provide 'isar-keywords)