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