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