etc/isar-keywords-ZF.el
author wenzelm
Thu Mar 15 00:10:45 2012 +0100 (2012-03-15)
changeset 46938 cda018294515
parent 45134 9b02f6665fc8
child 46974 7ca3608146d8
permissions -rw-r--r--
some support for outer syntax keyword declarations within theory header;
more uniform Thy_Header.header as argument for begin_theory etc.;
     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     "coinductive"
    44     "commit"
    45     "consts"
    46     "context"
    47     "corollary"
    48     "datatype"
    49     "declaration"
    50     "declare"
    51     "def"
    52     "default_sort"
    53     "defer"
    54     "definition"
    55     "defs"
    56     "disable_pr"
    57     "display_drafts"
    58     "done"
    59     "enable_pr"
    60     "end"
    61     "exit"
    62     "extract"
    63     "extract_type"
    64     "finalconsts"
    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     "inductive"
    81     "inductive_cases"
    82     "init_toplevel"
    83     "instance"
    84     "instantiation"
    85     "interpret"
    86     "interpretation"
    87     "judgment"
    88     "kill"
    89     "kill_thy"
    90     "lemma"
    91     "lemmas"
    92     "let"
    93     "linear_undo"
    94     "local_setup"
    95     "locale"
    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_cases"
   125     "print_claset"
   126     "print_classes"
   127     "print_codesetup"
   128     "print_commands"
   129     "print_configs"
   130     "print_context"
   131     "print_dependencies"
   132     "print_drafts"
   133     "print_facts"
   134     "print_induct_rules"
   135     "print_interps"
   136     "print_locale"
   137     "print_locales"
   138     "print_methods"
   139     "print_rules"
   140     "print_simpset"
   141     "print_statement"
   142     "print_syntax"
   143     "print_tcset"
   144     "print_theorems"
   145     "print_theory"
   146     "print_trans_rules"
   147     "print_translation"
   148     "proof"
   149     "prop"
   150     "pwd"
   151     "qed"
   152     "quit"
   153     "realizability"
   154     "realizers"
   155     "remove_thy"
   156     "rep_datatype"
   157     "schematic_corollary"
   158     "schematic_lemma"
   159     "schematic_theorem"
   160     "sect"
   161     "section"
   162     "setup"
   163     "show"
   164     "simproc_setup"
   165     "sorry"
   166     "subclass"
   167     "sublocale"
   168     "subsect"
   169     "subsection"
   170     "subsubsect"
   171     "subsubsection"
   172     "syntax"
   173     "syntax_declaration"
   174     "term"
   175     "text"
   176     "text_raw"
   177     "then"
   178     "theorem"
   179     "theorems"
   180     "theory"
   181     "thm"
   182     "thm_deps"
   183     "thus"
   184     "thy_deps"
   185     "translations"
   186     "txt"
   187     "txt_raw"
   188     "typ"
   189     "type_notation"
   190     "type_synonym"
   191     "typed_print_translation"
   192     "typedecl"
   193     "ultimately"
   194     "undo"
   195     "undos_proof"
   196     "unfolding"
   197     "unused_thms"
   198     "use"
   199     "use_thy"
   200     "using"
   201     "welcome"
   202     "with"
   203     "write"
   204     "{"
   205     "}"))
   206 
   207 (defconst isar-keywords-minor
   208   '("advanced"
   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     "induction"
   227     "infix"
   228     "infixl"
   229     "infixr"
   230     "intros"
   231     "is"
   232     "keywords"
   233     "monos"
   234     "notes"
   235     "obtains"
   236     "open"
   237     "output"
   238     "overloaded"
   239     "pervasive"
   240     "recursor_eqns"
   241     "shows"
   242     "structure"
   243     "type_elims"
   244     "type_intros"
   245     "unchecked"
   246     "uses"
   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\\.process_pgip"
   255     "ProofGeneral\\.restart"
   256     "ProofGeneral\\.undo"
   257     "cannot_undo"
   258     "cd"
   259     "commit"
   260     "disable_pr"
   261     "enable_pr"
   262     "exit"
   263     "init_toplevel"
   264     "kill"
   265     "kill_thy"
   266     "linear_undo"
   267     "quit"
   268     "remove_thy"
   269     "undo"
   270     "undos_proof"
   271     "use_thy"))
   272 
   273 (defconst isar-keywords-diag
   274   '("ML_command"
   275     "ML_val"
   276     "ProofGeneral\\.pr"
   277     "class_deps"
   278     "display_drafts"
   279     "find_consts"
   280     "find_theorems"
   281     "full_prf"
   282     "header"
   283     "help"
   284     "pr"
   285     "pretty_setmargin"
   286     "prf"
   287     "print_abbrevs"
   288     "print_antiquotations"
   289     "print_attributes"
   290     "print_binds"
   291     "print_cases"
   292     "print_claset"
   293     "print_classes"
   294     "print_codesetup"
   295     "print_commands"
   296     "print_configs"
   297     "print_context"
   298     "print_dependencies"
   299     "print_drafts"
   300     "print_facts"
   301     "print_induct_rules"
   302     "print_interps"
   303     "print_locale"
   304     "print_locales"
   305     "print_methods"
   306     "print_rules"
   307     "print_simpset"
   308     "print_statement"
   309     "print_syntax"
   310     "print_tcset"
   311     "print_theorems"
   312     "print_theory"
   313     "print_trans_rules"
   314     "prop"
   315     "pwd"
   316     "term"
   317     "thm"
   318     "thm_deps"
   319     "thy_deps"
   320     "typ"
   321     "unused_thms"
   322     "welcome"))
   323 
   324 (defconst isar-keywords-theory-begin
   325   '("theory"))
   326 
   327 (defconst isar-keywords-theory-switch
   328   '())
   329 
   330 (defconst isar-keywords-theory-end
   331   '("end"))
   332 
   333 (defconst isar-keywords-theory-heading
   334   '("chapter"
   335     "section"
   336     "subsection"
   337     "subsubsection"))
   338 
   339 (defconst isar-keywords-theory-decl
   340   '("ML"
   341     "abbreviation"
   342     "arities"
   343     "attribute_setup"
   344     "axiomatization"
   345     "axioms"
   346     "class"
   347     "classes"
   348     "classrel"
   349     "codatatype"
   350     "code_datatype"
   351     "coinductive"
   352     "consts"
   353     "context"
   354     "datatype"
   355     "declaration"
   356     "declare"
   357     "default_sort"
   358     "definition"
   359     "defs"
   360     "extract"
   361     "extract_type"
   362     "finalconsts"
   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     "use"))
   404 
   405 (defconst isar-keywords-theory-script
   406   '("inductive_cases"))
   407 
   408 (defconst isar-keywords-theory-goal
   409   '("corollary"
   410     "instance"
   411     "interpretation"
   412     "lemma"
   413     "schematic_corollary"
   414     "schematic_lemma"
   415     "schematic_theorem"
   416     "subclass"
   417     "sublocale"
   418     "theorem"))
   419 
   420 (defconst isar-keywords-qed
   421   '("\\."
   422     "\\.\\."
   423     "by"
   424     "done"
   425     "sorry"))
   426 
   427 (defconst isar-keywords-qed-block
   428   '("qed"))
   429 
   430 (defconst isar-keywords-qed-global
   431   '("oops"))
   432 
   433 (defconst isar-keywords-proof-heading
   434   '("sect"
   435     "subsect"
   436     "subsubsect"))
   437 
   438 (defconst isar-keywords-proof-goal
   439   '("have"
   440     "hence"
   441     "interpret"))
   442 
   443 (defconst isar-keywords-proof-block
   444   '("next"
   445     "proof"))
   446 
   447 (defconst isar-keywords-proof-open
   448   '("{"))
   449 
   450 (defconst isar-keywords-proof-close
   451   '("}"))
   452 
   453 (defconst isar-keywords-proof-chain
   454   '("finally"
   455     "from"
   456     "then"
   457     "ultimately"
   458     "with"))
   459 
   460 (defconst isar-keywords-proof-decl
   461   '("ML_prf"
   462     "also"
   463     "let"
   464     "moreover"
   465     "note"
   466     "txt"
   467     "txt_raw"
   468     "unfolding"
   469     "using"
   470     "write"))
   471 
   472 (defconst isar-keywords-proof-asm
   473   '("assume"
   474     "case"
   475     "def"
   476     "fix"
   477     "presume"))
   478 
   479 (defconst isar-keywords-proof-asm-goal
   480   '("guess"
   481     "obtain"
   482     "show"
   483     "thus"))
   484 
   485 (defconst isar-keywords-proof-script
   486   '("apply"
   487     "apply_end"
   488     "back"
   489     "defer"
   490     "prefer"))
   491 
   492 (provide 'isar-keywords)