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