etc/isar-keywords-ZF.el
author bulwahn
Tue Dec 20 17:40:18 2011 +0100 (2011-12-20)
changeset 45928 874845660119
parent 45134 9b02f6665fc8
child 46938 cda018294515
permissions -rw-r--r--
adding quickcheck generators in some HOL-Library theories
     1 ;;
     2 ;; Keyword classification tables for Isabelle/Isar.
     3 ;; Generated from Pure + FOL + ZF.
     4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     5 ;;
     6 
     7 (defconst isar-keywords-major
     8   '("\\."
     9     "\\.\\."
    10     "Isabelle\\.command"
    11     "ML"
    12     "ML_command"
    13     "ML_prf"
    14     "ML_val"
    15     "ProofGeneral\\.inform_file_processed"
    16     "ProofGeneral\\.inform_file_retracted"
    17     "ProofGeneral\\.kill_proof"
    18     "ProofGeneral\\.pr"
    19     "ProofGeneral\\.process_pgip"
    20     "ProofGeneral\\.restart"
    21     "ProofGeneral\\.undo"
    22     "abbreviation"
    23     "also"
    24     "apply"
    25     "apply_end"
    26     "arities"
    27     "assume"
    28     "attribute_setup"
    29     "axiomatization"
    30     "axioms"
    31     "back"
    32     "by"
    33     "cannot_undo"
    34     "case"
    35     "cd"
    36     "chapter"
    37     "class"
    38     "class_deps"
    39     "classes"
    40     "classrel"
    41     "codatatype"
    42     "code_datatype"
    43     "coinductive"
    44     "commit"
    45     "consts"
    46     "context"
    47     "corollary"
    48     "datatype"
    49     "declaration"
    50     "declare"
    51     "def"
    52     "default_sort"
    53     "defer"
    54     "definition"
    55     "defs"
    56     "disable_pr"
    57     "display_drafts"
    58     "done"
    59     "enable_pr"
    60     "end"
    61     "exit"
    62     "extract"
    63     "extract_type"
    64     "finalconsts"
    65     "finally"
    66     "find_consts"
    67     "find_theorems"
    68     "fix"
    69     "from"
    70     "full_prf"
    71     "guess"
    72     "have"
    73     "header"
    74     "help"
    75     "hence"
    76     "hide_class"
    77     "hide_const"
    78     "hide_fact"
    79     "hide_type"
    80     "inductive"
    81     "inductive_cases"
    82     "init_toplevel"
    83     "instance"
    84     "instantiation"
    85     "interpret"
    86     "interpretation"
    87     "judgment"
    88     "kill"
    89     "kill_thy"
    90     "lemma"
    91     "lemmas"
    92     "let"
    93     "linear_undo"
    94     "local_setup"
    95     "locale"
    96     "method_setup"
    97     "moreover"
    98     "next"
    99     "no_notation"
   100     "no_syntax"
   101     "no_translations"
   102     "no_type_notation"
   103     "nonterminal"
   104     "notation"
   105     "note"
   106     "notepad"
   107     "obtain"
   108     "oops"
   109     "oracle"
   110     "overloading"
   111     "parse_ast_translation"
   112     "parse_translation"
   113     "pr"
   114     "prefer"
   115     "presume"
   116     "pretty_setmargin"
   117     "prf"
   118     "primrec"
   119     "print_abbrevs"
   120     "print_antiquotations"
   121     "print_ast_translation"
   122     "print_attributes"
   123     "print_binds"
   124     "print_cases"
   125     "print_claset"
   126     "print_classes"
   127     "print_codesetup"
   128     "print_commands"
   129     "print_configs"
   130     "print_context"
   131     "print_dependencies"
   132     "print_drafts"
   133     "print_facts"
   134     "print_induct_rules"
   135     "print_interps"
   136     "print_locale"
   137     "print_locales"
   138     "print_methods"
   139     "print_rules"
   140     "print_simpset"
   141     "print_statement"
   142     "print_syntax"
   143     "print_tcset"
   144     "print_theorems"
   145     "print_theory"
   146     "print_trans_rules"
   147     "print_translation"
   148     "proof"
   149     "prop"
   150     "pwd"
   151     "qed"
   152     "quit"
   153     "realizability"
   154     "realizers"
   155     "remove_thy"
   156     "rep_datatype"
   157     "schematic_corollary"
   158     "schematic_lemma"
   159     "schematic_theorem"
   160     "sect"
   161     "section"
   162     "setup"
   163     "show"
   164     "simproc_setup"
   165     "sorry"
   166     "subclass"
   167     "sublocale"
   168     "subsect"
   169     "subsection"
   170     "subsubsect"
   171     "subsubsection"
   172     "syntax"
   173     "syntax_declaration"
   174     "term"
   175     "text"
   176     "text_raw"
   177     "then"
   178     "theorem"
   179     "theorems"
   180     "theory"
   181     "thm"
   182     "thm_deps"
   183     "thus"
   184     "thy_deps"
   185     "translations"
   186     "txt"
   187     "txt_raw"
   188     "typ"
   189     "type_notation"
   190     "type_synonym"
   191     "typed_print_translation"
   192     "typedecl"
   193     "ultimately"
   194     "undo"
   195     "undos_proof"
   196     "unfolding"
   197     "unused_thms"
   198     "use"
   199     "use_thy"
   200     "using"
   201     "welcome"
   202     "with"
   203     "write"
   204     "{"
   205     "}"))
   206 
   207 (defconst isar-keywords-minor
   208   '("advanced"
   209     "and"
   210     "assumes"
   211     "attach"
   212     "begin"
   213     "binder"
   214     "case_eqns"
   215     "con_defs"
   216     "constrains"
   217     "defines"
   218     "domains"
   219     "elimination"
   220     "fixes"
   221     "for"
   222     "identifier"
   223     "if"
   224     "imports"
   225     "in"
   226     "induction"
   227     "infix"
   228     "infixl"
   229     "infixr"
   230     "intros"
   231     "is"
   232     "monos"
   233     "notes"
   234     "obtains"
   235     "open"
   236     "output"
   237     "overloaded"
   238     "pervasive"
   239     "recursor_eqns"
   240     "shows"
   241     "structure"
   242     "type_elims"
   243     "type_intros"
   244     "unchecked"
   245     "uses"
   246     "where"))
   247 
   248 (defconst isar-keywords-control
   249   '("Isabelle\\.command"
   250     "ProofGeneral\\.inform_file_processed"
   251     "ProofGeneral\\.inform_file_retracted"
   252     "ProofGeneral\\.kill_proof"
   253     "ProofGeneral\\.process_pgip"
   254     "ProofGeneral\\.restart"
   255     "ProofGeneral\\.undo"
   256     "cannot_undo"
   257     "cd"
   258     "commit"
   259     "disable_pr"
   260     "enable_pr"
   261     "exit"
   262     "init_toplevel"
   263     "kill"
   264     "kill_thy"
   265     "linear_undo"
   266     "quit"
   267     "remove_thy"
   268     "undo"
   269     "undos_proof"
   270     "use_thy"))
   271 
   272 (defconst isar-keywords-diag
   273   '("ML_command"
   274     "ML_val"
   275     "ProofGeneral\\.pr"
   276     "class_deps"
   277     "display_drafts"
   278     "find_consts"
   279     "find_theorems"
   280     "full_prf"
   281     "header"
   282     "help"
   283     "pr"
   284     "pretty_setmargin"
   285     "prf"
   286     "print_abbrevs"
   287     "print_antiquotations"
   288     "print_attributes"
   289     "print_binds"
   290     "print_cases"
   291     "print_claset"
   292     "print_classes"
   293     "print_codesetup"
   294     "print_commands"
   295     "print_configs"
   296     "print_context"
   297     "print_dependencies"
   298     "print_drafts"
   299     "print_facts"
   300     "print_induct_rules"
   301     "print_interps"
   302     "print_locale"
   303     "print_locales"
   304     "print_methods"
   305     "print_rules"
   306     "print_simpset"
   307     "print_statement"
   308     "print_syntax"
   309     "print_tcset"
   310     "print_theorems"
   311     "print_theory"
   312     "print_trans_rules"
   313     "prop"
   314     "pwd"
   315     "term"
   316     "thm"
   317     "thm_deps"
   318     "thy_deps"
   319     "typ"
   320     "unused_thms"
   321     "welcome"))
   322 
   323 (defconst isar-keywords-theory-begin
   324   '("theory"))
   325 
   326 (defconst isar-keywords-theory-switch
   327   '())
   328 
   329 (defconst isar-keywords-theory-end
   330   '("end"))
   331 
   332 (defconst isar-keywords-theory-heading
   333   '("chapter"
   334     "section"
   335     "subsection"
   336     "subsubsection"))
   337 
   338 (defconst isar-keywords-theory-decl
   339   '("ML"
   340     "abbreviation"
   341     "arities"
   342     "attribute_setup"
   343     "axiomatization"
   344     "axioms"
   345     "class"
   346     "classes"
   347     "classrel"
   348     "codatatype"
   349     "code_datatype"
   350     "coinductive"
   351     "consts"
   352     "context"
   353     "datatype"
   354     "declaration"
   355     "declare"
   356     "default_sort"
   357     "definition"
   358     "defs"
   359     "extract"
   360     "extract_type"
   361     "finalconsts"
   362     "hide_class"
   363     "hide_const"
   364     "hide_fact"
   365     "hide_type"
   366     "inductive"
   367     "instantiation"
   368     "judgment"
   369     "lemmas"
   370     "local_setup"
   371     "locale"
   372     "method_setup"
   373     "no_notation"
   374     "no_syntax"
   375     "no_translations"
   376     "no_type_notation"
   377     "nonterminal"
   378     "notation"
   379     "notepad"
   380     "oracle"
   381     "overloading"
   382     "parse_ast_translation"
   383     "parse_translation"
   384     "primrec"
   385     "print_ast_translation"
   386     "print_translation"
   387     "realizability"
   388     "realizers"
   389     "rep_datatype"
   390     "setup"
   391     "simproc_setup"
   392     "syntax"
   393     "syntax_declaration"
   394     "text"
   395     "text_raw"
   396     "theorems"
   397     "translations"
   398     "type_notation"
   399     "type_synonym"
   400     "typed_print_translation"
   401     "typedecl"
   402     "use"))
   403 
   404 (defconst isar-keywords-theory-script
   405   '("inductive_cases"))
   406 
   407 (defconst isar-keywords-theory-goal
   408   '("corollary"
   409     "instance"
   410     "interpretation"
   411     "lemma"
   412     "schematic_corollary"
   413     "schematic_lemma"
   414     "schematic_theorem"
   415     "subclass"
   416     "sublocale"
   417     "theorem"))
   418 
   419 (defconst isar-keywords-qed
   420   '("\\."
   421     "\\.\\."
   422     "by"
   423     "done"
   424     "sorry"))
   425 
   426 (defconst isar-keywords-qed-block
   427   '("qed"))
   428 
   429 (defconst isar-keywords-qed-global
   430   '("oops"))
   431 
   432 (defconst isar-keywords-proof-heading
   433   '("sect"
   434     "subsect"
   435     "subsubsect"))
   436 
   437 (defconst isar-keywords-proof-goal
   438   '("have"
   439     "hence"
   440     "interpret"))
   441 
   442 (defconst isar-keywords-proof-block
   443   '("next"
   444     "proof"))
   445 
   446 (defconst isar-keywords-proof-open
   447   '("{"))
   448 
   449 (defconst isar-keywords-proof-close
   450   '("}"))
   451 
   452 (defconst isar-keywords-proof-chain
   453   '("finally"
   454     "from"
   455     "then"
   456     "ultimately"
   457     "with"))
   458 
   459 (defconst isar-keywords-proof-decl
   460   '("ML_prf"
   461     "also"
   462     "let"
   463     "moreover"
   464     "note"
   465     "txt"
   466     "txt_raw"
   467     "unfolding"
   468     "using"
   469     "write"))
   470 
   471 (defconst isar-keywords-proof-asm
   472   '("assume"
   473     "case"
   474     "def"
   475     "fix"
   476     "presume"))
   477 
   478 (defconst isar-keywords-proof-asm-goal
   479   '("guess"
   480     "obtain"
   481     "show"
   482     "thus"))
   483 
   484 (defconst isar-keywords-proof-script
   485   '("apply"
   486     "apply_end"
   487     "back"
   488     "defer"
   489     "prefer"))
   490 
   491 (provide 'isar-keywords)