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