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