etc/isar-keywords-ZF.el
author ballarin
Wed Mar 09 18:44:52 2005 +0100 (2005-03-09)
changeset 15596 8665d08085df
parent 15407 9e85d2b04867
child 15598 4ab52355bb53
permissions -rw-r--r--
First version of global registration command.
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; This file was generated by Isabelle/ZF -- DO NOT EDIT!
     4 ;;
     5 ;; $Id$
     6 ;;
     7 
     8 (defconst isar-keywords-major
     9   '("\\."
    10     "\\.\\."
    11     "ML"
    12     "ML_command"
    13     "ML_setup"
    14     "ProofGeneral\\.context_thy_only"
    15     "ProofGeneral\\.inform_file_processed"
    16     "ProofGeneral\\.inform_file_retracted"
    17     "ProofGeneral\\.kill_proof"
    18     "ProofGeneral\\.process_pgip"
    19     "ProofGeneral\\.restart"
    20     "ProofGeneral\\.try_context_thy_only"
    21     "ProofGeneral\\.undo"
    22     "also"
    23     "apply"
    24     "apply_end"
    25     "arities"
    26     "assume"
    27     "axclass"
    28     "axioms"
    29     "back"
    30     "by"
    31     "cannot_undo"
    32     "case"
    33     "cd"
    34     "chapter"
    35     "classes"
    36     "classrel"
    37     "clear_undos"
    38     "codatatype"
    39     "coinductive"
    40     "commit"
    41     "constdefs"
    42     "consts"
    43     "consts_code"
    44     "context"
    45     "corollary"
    46     "datatype"
    47     "declare"
    48     "def"
    49     "defaultsort"
    50     "defer"
    51     "defs"
    52     "disable_pr"
    53     "display_drafts"
    54     "done"
    55     "enable_pr"
    56     "end"
    57     "exit"
    58     "extract"
    59     "extract_type"
    60     "finalconsts"
    61     "finally"
    62     "find_rewrites"
    63     "fix"
    64     "from"
    65     "full_prf"
    66     "generate_code"
    67     "global"
    68     "have"
    69     "header"
    70     "hence"
    71     "hide"
    72     "inductive"
    73     "inductive_cases"
    74     "init_toplevel"
    75     "instance"
    76     "instantiate"
    77     "judgment"
    78     "kill"
    79     "kill_thy"
    80     "lemma"
    81     "lemmas"
    82     "let"
    83     "local"
    84     "locale"
    85     "method_setup"
    86     "moreover"
    87     "next"
    88     "nonterminals"
    89     "note"
    90     "obtain"
    91     "oops"
    92     "oracle"
    93     "parse_ast_translation"
    94     "parse_translation"
    95     "pr"
    96     "prefer"
    97     "presume"
    98     "pretty_setmargin"
    99     "prf"
   100     "primrec"
   101     "print_antiquotations"
   102     "print_ast_translation"
   103     "print_attributes"
   104     "print_binds"
   105     "print_cases"
   106     "print_claset"
   107     "print_commands"
   108     "print_context"
   109     "print_drafts"
   110     "print_facts"
   111     "print_induct_rules"
   112     "print_intros"
   113     "print_locale"
   114     "print_locales"
   115     "print_methods"
   116     "print_registrations"
   117     "print_rules"
   118     "print_simpset"
   119     "print_syntax"
   120     "print_tcset"
   121     "print_theorems"
   122     "print_theory"
   123     "print_trans_rules"
   124     "print_translation"
   125     "proof"
   126     "prop"
   127     "pwd"
   128     "qed"
   129     "quickcheck"
   130     "quickcheck_params"
   131     "quit"
   132     "realizability"
   133     "realizers"
   134     "redo"
   135     "registration"
   136     "remove_thy"
   137     "rep_datatype"
   138     "sect"
   139     "section"
   140     "setup"
   141     "show"
   142     "sorry"
   143     "subsect"
   144     "subsection"
   145     "subsubsect"
   146     "subsubsection"
   147     "syntax"
   148     "term"
   149     "text"
   150     "text_raw"
   151     "then"
   152     "theorem"
   153     "theorems"
   154     "theory"
   155     "thm"
   156     "thm_deps"
   157     "thms_containing"
   158     "thus"
   159     "token_translation"
   160     "touch_all_thys"
   161     "touch_child_thys"
   162     "touch_thy"
   163     "translations"
   164     "txt"
   165     "txt_raw"
   166     "typ"
   167     "typed_print_translation"
   168     "typedecl"
   169     "types"
   170     "types_code"
   171     "ultimately"
   172     "undo"
   173     "undos_proof"
   174     "update_thy"
   175     "update_thy_only"
   176     "use"
   177     "use_thy"
   178     "use_thy_only"
   179     "using"
   180     "welcome"
   181     "with"
   182     "{"
   183     "}"))
   184 
   185 (defconst isar-keywords-minor
   186   '("advanced"
   187     "and"
   188     "assumes"
   189     "begin"
   190     "binder"
   191     "case_eqns"
   192     "con_defs"
   193     "concl"
   194     "defines"
   195     "domains"
   196     "elimination"
   197     "files"
   198     "fixes"
   199     "imports"
   200     "in"
   201     "includes"
   202     "induction"
   203     "infix"
   204     "infixl"
   205     "infixr"
   206     "intros"
   207     "is"
   208     "monos"
   209     "notes"
   210     "open"
   211     "output"
   212     "overloaded"
   213     "recursor_eqns"
   214     "shows"
   215     "structure"
   216     "type_elims"
   217     "type_intros"
   218     "where"))
   219 
   220 (defconst isar-keywords-control
   221   '("ProofGeneral\\.context_thy_only"
   222     "ProofGeneral\\.inform_file_processed"
   223     "ProofGeneral\\.inform_file_retracted"
   224     "ProofGeneral\\.kill_proof"
   225     "ProofGeneral\\.process_pgip"
   226     "ProofGeneral\\.restart"
   227     "ProofGeneral\\.try_context_thy_only"
   228     "ProofGeneral\\.undo"
   229     "cannot_undo"
   230     "clear_undos"
   231     "exit"
   232     "init_toplevel"
   233     "kill"
   234     "quit"
   235     "redo"
   236     "undo"
   237     "undos_proof"))
   238 
   239 (defconst isar-keywords-diag
   240   '("ML"
   241     "ML_command"
   242     "cd"
   243     "commit"
   244     "disable_pr"
   245     "display_drafts"
   246     "enable_pr"
   247     "find_rewrites"
   248     "full_prf"
   249     "header"
   250     "kill_thy"
   251     "pr"
   252     "pretty_setmargin"
   253     "prf"
   254     "print_antiquotations"
   255     "print_attributes"
   256     "print_binds"
   257     "print_cases"
   258     "print_claset"
   259     "print_commands"
   260     "print_context"
   261     "print_drafts"
   262     "print_facts"
   263     "print_induct_rules"
   264     "print_intros"
   265     "print_locale"
   266     "print_locales"
   267     "print_methods"
   268     "print_registrations"
   269     "print_rules"
   270     "print_simpset"
   271     "print_syntax"
   272     "print_tcset"
   273     "print_theorems"
   274     "print_theory"
   275     "print_trans_rules"
   276     "prop"
   277     "pwd"
   278     "quickcheck"
   279     "remove_thy"
   280     "term"
   281     "thm"
   282     "thm_deps"
   283     "thms_containing"
   284     "touch_all_thys"
   285     "touch_child_thys"
   286     "touch_thy"
   287     "typ"
   288     "update_thy"
   289     "update_thy_only"
   290     "use"
   291     "use_thy"
   292     "use_thy_only"
   293     "welcome"))
   294 
   295 (defconst isar-keywords-theory-begin
   296   '("theory"))
   297 
   298 (defconst isar-keywords-theory-switch
   299   '("context"))
   300 
   301 (defconst isar-keywords-theory-end
   302   '("end"))
   303 
   304 (defconst isar-keywords-theory-heading
   305   '("chapter"
   306     "section"
   307     "subsection"
   308     "subsubsection"))
   309 
   310 (defconst isar-keywords-theory-decl
   311   '("ML_setup"
   312     "arities"
   313     "axclass"
   314     "axioms"
   315     "classes"
   316     "classrel"
   317     "codatatype"
   318     "coinductive"
   319     "constdefs"
   320     "consts"
   321     "consts_code"
   322     "datatype"
   323     "defaultsort"
   324     "defs"
   325     "extract"
   326     "extract_type"
   327     "finalconsts"
   328     "generate_code"
   329     "global"
   330     "hide"
   331     "inductive"
   332     "judgment"
   333     "lemmas"
   334     "local"
   335     "locale"
   336     "method_setup"
   337     "nonterminals"
   338     "oracle"
   339     "parse_ast_translation"
   340     "parse_translation"
   341     "primrec"
   342     "print_ast_translation"
   343     "print_translation"
   344     "quickcheck_params"
   345     "realizability"
   346     "realizers"
   347     "rep_datatype"
   348     "setup"
   349     "syntax"
   350     "text"
   351     "text_raw"
   352     "theorems"
   353     "token_translation"
   354     "translations"
   355     "typed_print_translation"
   356     "typedecl"
   357     "types"
   358     "types_code"))
   359 
   360 (defconst isar-keywords-theory-script
   361   '("declare"
   362     "inductive_cases"))
   363 
   364 (defconst isar-keywords-theory-goal
   365   '("corollary"
   366     "instance"
   367     "lemma"
   368     "registration"
   369     "theorem"))
   370 
   371 (defconst isar-keywords-qed
   372   '("\\."
   373     "\\.\\."
   374     "by"
   375     "done"
   376     "sorry"))
   377 
   378 (defconst isar-keywords-qed-block
   379   '("qed"))
   380 
   381 (defconst isar-keywords-qed-global
   382   '("oops"))
   383 
   384 (defconst isar-keywords-proof-heading
   385   '("sect"
   386     "subsect"
   387     "subsubsect"))
   388 
   389 (defconst isar-keywords-proof-goal
   390   '("have"
   391     "hence"
   392     "show"
   393     "thus"))
   394 
   395 (defconst isar-keywords-proof-block
   396   '("next"
   397     "proof"))
   398 
   399 (defconst isar-keywords-proof-open
   400   '("{"))
   401 
   402 (defconst isar-keywords-proof-close
   403   '("}"))
   404 
   405 (defconst isar-keywords-proof-chain
   406   '("finally"
   407     "from"
   408     "then"
   409     "ultimately"
   410     "with"))
   411 
   412 (defconst isar-keywords-proof-decl
   413   '("also"
   414     "instantiate"
   415     "let"
   416     "moreover"
   417     "note"
   418     "txt"
   419     "txt_raw"
   420     "using"))
   421 
   422 (defconst isar-keywords-proof-asm
   423   '("assume"
   424     "case"
   425     "def"
   426     "fix"
   427     "presume"))
   428 
   429 (defconst isar-keywords-proof-asm-goal
   430   '("obtain"))
   431 
   432 (defconst isar-keywords-proof-script
   433   '("apply"
   434     "apply_end"
   435     "back"
   436     "defer"
   437     "prefer"))
   438 
   439 (provide 'isar-keywords)