etc/isar-keywords-ZF.el
author ballarin
Wed Jun 01 12:30:49 2005 +0200 (2005-06-01)
changeset 16168 adb83939177f
parent 16034 6ccd552ee366
child 16419 0c3db621bbbd
permissions -rw-r--r--
Locales: new element constrains, parameter renaming with syntax,
experimental command instantiate withdrawn.
     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     "coinductive"
    41     "commit"
    42     "constdefs"
    43     "consts"
    44     "consts_code"
    45     "context"
    46     "corollary"
    47     "datatype"
    48     "declare"
    49     "def"
    50     "defaultsort"
    51     "defer"
    52     "defs"
    53     "disable_pr"
    54     "display_drafts"
    55     "done"
    56     "enable_pr"
    57     "end"
    58     "exit"
    59     "extract"
    60     "extract_type"
    61     "finalconsts"
    62     "finally"
    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     "interpret"
    77     "interpretation"
    78     "judgment"
    79     "kill"
    80     "kill_thy"
    81     "lemma"
    82     "lemmas"
    83     "let"
    84     "local"
    85     "locale"
    86     "method_setup"
    87     "moreover"
    88     "next"
    89     "no_syntax"
    90     "nonterminals"
    91     "note"
    92     "obtain"
    93     "oops"
    94     "oracle"
    95     "parse_ast_translation"
    96     "parse_translation"
    97     "pr"
    98     "prefer"
    99     "presume"
   100     "pretty_setmargin"
   101     "prf"
   102     "primrec"
   103     "print_antiquotations"
   104     "print_ast_translation"
   105     "print_attributes"
   106     "print_binds"
   107     "print_cases"
   108     "print_claset"
   109     "print_commands"
   110     "print_context"
   111     "print_drafts"
   112     "print_facts"
   113     "print_induct_rules"
   114     "print_interps"
   115     "print_locale"
   116     "print_locales"
   117     "print_methods"
   118     "print_rules"
   119     "print_simpset"
   120     "print_syntax"
   121     "print_tcset"
   122     "print_theorems"
   123     "print_theory"
   124     "print_trans_rules"
   125     "print_translation"
   126     "proof"
   127     "prop"
   128     "pwd"
   129     "qed"
   130     "quickcheck"
   131     "quickcheck_params"
   132     "quit"
   133     "realizability"
   134     "realizers"
   135     "redo"
   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     "constrains"
   195     "defines"
   196     "domains"
   197     "elimination"
   198     "files"
   199     "fixes"
   200     "imports"
   201     "in"
   202     "includes"
   203     "induction"
   204     "infix"
   205     "infixl"
   206     "infixr"
   207     "intros"
   208     "is"
   209     "monos"
   210     "notes"
   211     "open"
   212     "output"
   213     "overloaded"
   214     "recursor_eqns"
   215     "shows"
   216     "structure"
   217     "type_elims"
   218     "type_intros"
   219     "where"))
   220 
   221 (defconst isar-keywords-control
   222   '("ProofGeneral\\.context_thy_only"
   223     "ProofGeneral\\.inform_file_processed"
   224     "ProofGeneral\\.inform_file_retracted"
   225     "ProofGeneral\\.kill_proof"
   226     "ProofGeneral\\.process_pgip"
   227     "ProofGeneral\\.redo"
   228     "ProofGeneral\\.restart"
   229     "ProofGeneral\\.try_context_thy_only"
   230     "ProofGeneral\\.undo"
   231     "cannot_undo"
   232     "clear_undos"
   233     "exit"
   234     "init_toplevel"
   235     "kill"
   236     "quit"
   237     "redo"
   238     "undo"
   239     "undos_proof"))
   240 
   241 (defconst isar-keywords-diag
   242   '("ML"
   243     "ML_command"
   244     "cd"
   245     "commit"
   246     "disable_pr"
   247     "display_drafts"
   248     "enable_pr"
   249     "full_prf"
   250     "header"
   251     "kill_thy"
   252     "pr"
   253     "pretty_setmargin"
   254     "prf"
   255     "print_antiquotations"
   256     "print_attributes"
   257     "print_binds"
   258     "print_cases"
   259     "print_claset"
   260     "print_commands"
   261     "print_context"
   262     "print_drafts"
   263     "print_facts"
   264     "print_induct_rules"
   265     "print_interps"
   266     "print_locale"
   267     "print_locales"
   268     "print_methods"
   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     "no_syntax"
   338     "nonterminals"
   339     "oracle"
   340     "parse_ast_translation"
   341     "parse_translation"
   342     "primrec"
   343     "print_ast_translation"
   344     "print_translation"
   345     "quickcheck_params"
   346     "realizability"
   347     "realizers"
   348     "rep_datatype"
   349     "setup"
   350     "syntax"
   351     "text"
   352     "text_raw"
   353     "theorems"
   354     "token_translation"
   355     "translations"
   356     "typed_print_translation"
   357     "typedecl"
   358     "types"
   359     "types_code"))
   360 
   361 (defconst isar-keywords-theory-script
   362   '("declare"
   363     "inductive_cases"))
   364 
   365 (defconst isar-keywords-theory-goal
   366   '("corollary"
   367     "instance"
   368     "interpretation"
   369     "lemma"
   370     "theorem"))
   371 
   372 (defconst isar-keywords-qed
   373   '("\\."
   374     "\\.\\."
   375     "by"
   376     "done"
   377     "sorry"))
   378 
   379 (defconst isar-keywords-qed-block
   380   '("qed"))
   381 
   382 (defconst isar-keywords-qed-global
   383   '("oops"))
   384 
   385 (defconst isar-keywords-proof-heading
   386   '("sect"
   387     "subsect"
   388     "subsubsect"))
   389 
   390 (defconst isar-keywords-proof-goal
   391   '("have"
   392     "hence"
   393     "interpret"
   394     "show"
   395     "thus"))
   396 
   397 (defconst isar-keywords-proof-block
   398   '("next"
   399     "proof"))
   400 
   401 (defconst isar-keywords-proof-open
   402   '("{"))
   403 
   404 (defconst isar-keywords-proof-close
   405   '("}"))
   406 
   407 (defconst isar-keywords-proof-chain
   408   '("finally"
   409     "from"
   410     "then"
   411     "ultimately"
   412     "with"))
   413 
   414 (defconst isar-keywords-proof-decl
   415   '("also"
   416     "let"
   417     "moreover"
   418     "note"
   419     "txt"
   420     "txt_raw"
   421     "using"))
   422 
   423 (defconst isar-keywords-proof-asm
   424   '("assume"
   425     "case"
   426     "def"
   427     "fix"
   428     "presume"))
   429 
   430 (defconst isar-keywords-proof-asm-goal
   431   '("obtain"))
   432 
   433 (defconst isar-keywords-proof-script
   434   '("apply"
   435     "apply_end"
   436     "back"
   437     "defer"
   438     "prefer"))
   439 
   440 (provide 'isar-keywords)