moved HOL-Nominal keywords into default collection (isar-keywords.el);
authorwenzelm
Mon Oct 08 18:13:01 2007 +0200 (2007-10-08)
changeset 2490357a33f4c2c19
parent 24902 49f002c3964e
child 24904 5b59fadfe878
moved HOL-Nominal keywords into default collection (isar-keywords.el);
Admin/update-keywords
etc/isar-keywords-HOL-Nominal.el
     1.1 --- a/Admin/update-keywords	Mon Oct 08 16:28:29 2007 +0200
     1.2 +++ b/Admin/update-keywords	Mon Oct 08 18:13:01 2007 +0200
     1.3 @@ -14,10 +14,7 @@
     1.4  cd "$ISABELLE_HOME/etc"
     1.5  
     1.6  isatool keywords -t emacs \
     1.7 -  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz"
     1.8 -
     1.9 -isatool keywords -t emacs -k HOL-Nominal \
    1.10 -  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOL-Nominal.gz"
    1.11 +  "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz"
    1.12  
    1.13  isatool keywords -t emacs -k ZF \
    1.14    "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
     2.1 --- a/etc/isar-keywords-HOL-Nominal.el	Mon Oct 08 16:28:29 2007 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,556 +0,0 @@
     2.4 -;;
     2.5 -;; Keyword classification tables for Isabelle/Isar.
     2.6 -;; This file was generated from HOL + HOL-Nominal -- DO NOT EDIT!
     2.7 -;;
     2.8 -;; $Id$
     2.9 -;;
    2.10 -
    2.11 -(defconst isar-keywords-major
    2.12 -  '("\\."
    2.13 -    "\\.\\."
    2.14 -    "ML"
    2.15 -    "ML_command"
    2.16 -    "ML_setup"
    2.17 -    "ProofGeneral\\.inform_file_processed"
    2.18 -    "ProofGeneral\\.inform_file_retracted"
    2.19 -    "ProofGeneral\\.kill_proof"
    2.20 -    "ProofGeneral\\.process_pgip"
    2.21 -    "ProofGeneral\\.restart"
    2.22 -    "ProofGeneral\\.undo"
    2.23 -    "abbreviation"
    2.24 -    "also"
    2.25 -    "apply"
    2.26 -    "apply_end"
    2.27 -    "arities"
    2.28 -    "assume"
    2.29 -    "atom_decl"
    2.30 -    "ax_specification"
    2.31 -    "axclass"
    2.32 -    "axiomatization"
    2.33 -    "axioms"
    2.34 -    "back"
    2.35 -    "by"
    2.36 -    "cannot_undo"
    2.37 -    "case"
    2.38 -    "cd"
    2.39 -    "chapter"
    2.40 -    "class"
    2.41 -    "class_deps"
    2.42 -    "classes"
    2.43 -    "classrel"
    2.44 -    "code_class"
    2.45 -    "code_const"
    2.46 -    "code_datatype"
    2.47 -    "code_deps"
    2.48 -    "code_exception"
    2.49 -    "code_instance"
    2.50 -    "code_library"
    2.51 -    "code_module"
    2.52 -    "code_modulename"
    2.53 -    "code_moduleprolog"
    2.54 -    "code_monad"
    2.55 -    "code_props"
    2.56 -    "code_reserved"
    2.57 -    "code_thms"
    2.58 -    "code_type"
    2.59 -    "coinductive"
    2.60 -    "coinductive_set"
    2.61 -    "commit"
    2.62 -    "constdefs"
    2.63 -    "consts"
    2.64 -    "consts_code"
    2.65 -    "context"
    2.66 -    "corollary"
    2.67 -    "datatype"
    2.68 -    "declaration"
    2.69 -    "declare"
    2.70 -    "def"
    2.71 -    "defaultsort"
    2.72 -    "defer"
    2.73 -    "defer_recdef"
    2.74 -    "definition"
    2.75 -    "defs"
    2.76 -    "disable_pr"
    2.77 -    "display_drafts"
    2.78 -    "done"
    2.79 -    "enable_pr"
    2.80 -    "end"
    2.81 -    "equivariance"
    2.82 -    "exit"
    2.83 -    "export_code"
    2.84 -    "extract"
    2.85 -    "extract_type"
    2.86 -    "finalconsts"
    2.87 -    "finally"
    2.88 -    "find_theorems"
    2.89 -    "fix"
    2.90 -    "from"
    2.91 -    "full_prf"
    2.92 -    "fun"
    2.93 -    "function"
    2.94 -    "global"
    2.95 -    "guess"
    2.96 -    "have"
    2.97 -    "header"
    2.98 -    "help"
    2.99 -    "hence"
   2.100 -    "hide"
   2.101 -    "inductive"
   2.102 -    "inductive_cases"
   2.103 -    "inductive_set"
   2.104 -    "init_toplevel"
   2.105 -    "instance"
   2.106 -    "instance_proof"
   2.107 -    "instantiation"
   2.108 -    "interpret"
   2.109 -    "interpretation"
   2.110 -    "invoke"
   2.111 -    "judgment"
   2.112 -    "kill"
   2.113 -    "kill_thy"
   2.114 -    "lemma"
   2.115 -    "lemmas"
   2.116 -    "let"
   2.117 -    "local"
   2.118 -    "locale"
   2.119 -    "method_setup"
   2.120 -    "moreover"
   2.121 -    "next"
   2.122 -    "no_syntax"
   2.123 -    "no_translations"
   2.124 -    "nominal_datatype"
   2.125 -    "nominal_inductive"
   2.126 -    "nominal_primrec"
   2.127 -    "nonterminals"
   2.128 -    "normal_form"
   2.129 -    "notation"
   2.130 -    "note"
   2.131 -    "obtain"
   2.132 -    "oops"
   2.133 -    "oracle"
   2.134 -    "parse_ast_translation"
   2.135 -    "parse_translation"
   2.136 -    "pr"
   2.137 -    "prefer"
   2.138 -    "presume"
   2.139 -    "pretty_setmargin"
   2.140 -    "prf"
   2.141 -    "primrec"
   2.142 -    "print_abbrevs"
   2.143 -    "print_antiquotations"
   2.144 -    "print_ast_translation"
   2.145 -    "print_atp_rules"
   2.146 -    "print_attributes"
   2.147 -    "print_binds"
   2.148 -    "print_cases"
   2.149 -    "print_claset"
   2.150 -    "print_classes"
   2.151 -    "print_codesetup"
   2.152 -    "print_commands"
   2.153 -    "print_configs"
   2.154 -    "print_context"
   2.155 -    "print_drafts"
   2.156 -    "print_facts"
   2.157 -    "print_induct_rules"
   2.158 -    "print_interps"
   2.159 -    "print_locale"
   2.160 -    "print_locales"
   2.161 -    "print_methods"
   2.162 -    "print_noatp_rules"
   2.163 -    "print_orders"
   2.164 -    "print_rules"
   2.165 -    "print_simpset"
   2.166 -    "print_statement"
   2.167 -    "print_syntax"
   2.168 -    "print_theorems"
   2.169 -    "print_theory"
   2.170 -    "print_trans_rules"
   2.171 -    "print_translation"
   2.172 -    "proof"
   2.173 -    "prop"
   2.174 -    "pwd"
   2.175 -    "qed"
   2.176 -    "quickcheck"
   2.177 -    "quickcheck_params"
   2.178 -    "quit"
   2.179 -    "realizability"
   2.180 -    "realizers"
   2.181 -    "recdef"
   2.182 -    "recdef_tc"
   2.183 -    "record"
   2.184 -    "redo"
   2.185 -    "refute"
   2.186 -    "refute_params"
   2.187 -    "remove_thy"
   2.188 -    "rep_datatype"
   2.189 -    "sect"
   2.190 -    "section"
   2.191 -    "setup"
   2.192 -    "show"
   2.193 -    "simproc_setup"
   2.194 -    "sledgehammer"
   2.195 -    "sorry"
   2.196 -    "specification"
   2.197 -    "subsect"
   2.198 -    "subsection"
   2.199 -    "subsubsect"
   2.200 -    "subsubsection"
   2.201 -    "syntax"
   2.202 -    "term"
   2.203 -    "termination"
   2.204 -    "text"
   2.205 -    "text_raw"
   2.206 -    "then"
   2.207 -    "theorem"
   2.208 -    "theorems"
   2.209 -    "theory"
   2.210 -    "thm"
   2.211 -    "thm_deps"
   2.212 -    "thus"
   2.213 -    "thy_deps"
   2.214 -    "token_translation"
   2.215 -    "touch_child_thys"
   2.216 -    "touch_thy"
   2.217 -    "translations"
   2.218 -    "txt"
   2.219 -    "txt_raw"
   2.220 -    "typ"
   2.221 -    "typed_print_translation"
   2.222 -    "typedecl"
   2.223 -    "typedef"
   2.224 -    "types"
   2.225 -    "types_code"
   2.226 -    "ultimately"
   2.227 -    "undo"
   2.228 -    "undos_proof"
   2.229 -    "unfolding"
   2.230 -    "use"
   2.231 -    "use_thy"
   2.232 -    "using"
   2.233 -    "value"
   2.234 -    "welcome"
   2.235 -    "with"
   2.236 -    "{"
   2.237 -    "}"))
   2.238 -
   2.239 -(defconst isar-keywords-minor
   2.240 -  '("advanced"
   2.241 -    "and"
   2.242 -    "assumes"
   2.243 -    "attach"
   2.244 -    "avoids"
   2.245 -    "begin"
   2.246 -    "binder"
   2.247 -    "concl"
   2.248 -    "congs"
   2.249 -    "constrains"
   2.250 -    "contains"
   2.251 -    "defines"
   2.252 -    "distinct"
   2.253 -    "file"
   2.254 -    "fixes"
   2.255 -    "for"
   2.256 -    "freshness_context"
   2.257 -    "hints"
   2.258 -    "identifier"
   2.259 -    "if"
   2.260 -    "imports"
   2.261 -    "in"
   2.262 -    "includes"
   2.263 -    "induction"
   2.264 -    "infix"
   2.265 -    "infixl"
   2.266 -    "infixr"
   2.267 -    "inject"
   2.268 -    "invariant"
   2.269 -    "is"
   2.270 -    "local_syntax"
   2.271 -    "module_name"
   2.272 -    "monos"
   2.273 -    "morphisms"
   2.274 -    "notes"
   2.275 -    "obtains"
   2.276 -    "open"
   2.277 -    "otherwise"
   2.278 -    "output"
   2.279 -    "overloaded"
   2.280 -    "permissive"
   2.281 -    "sequential"
   2.282 -    "shows"
   2.283 -    "structure"
   2.284 -    "unchecked"
   2.285 -    "uses"
   2.286 -    "where"))
   2.287 -
   2.288 -(defconst isar-keywords-control
   2.289 -  '("ProofGeneral\\.inform_file_processed"
   2.290 -    "ProofGeneral\\.inform_file_retracted"
   2.291 -    "ProofGeneral\\.kill_proof"
   2.292 -    "ProofGeneral\\.process_pgip"
   2.293 -    "ProofGeneral\\.restart"
   2.294 -    "ProofGeneral\\.undo"
   2.295 -    "cannot_undo"
   2.296 -    "exit"
   2.297 -    "init_toplevel"
   2.298 -    "kill"
   2.299 -    "quit"
   2.300 -    "redo"
   2.301 -    "undo"
   2.302 -    "undos_proof"))
   2.303 -
   2.304 -(defconst isar-keywords-diag
   2.305 -  '("ML"
   2.306 -    "ML_command"
   2.307 -    "cd"
   2.308 -    "class_deps"
   2.309 -    "code_deps"
   2.310 -    "code_thms"
   2.311 -    "commit"
   2.312 -    "disable_pr"
   2.313 -    "display_drafts"
   2.314 -    "enable_pr"
   2.315 -    "export_code"
   2.316 -    "find_theorems"
   2.317 -    "full_prf"
   2.318 -    "header"
   2.319 -    "help"
   2.320 -    "kill_thy"
   2.321 -    "normal_form"
   2.322 -    "pr"
   2.323 -    "pretty_setmargin"
   2.324 -    "prf"
   2.325 -    "print_abbrevs"
   2.326 -    "print_antiquotations"
   2.327 -    "print_atp_rules"
   2.328 -    "print_attributes"
   2.329 -    "print_binds"
   2.330 -    "print_cases"
   2.331 -    "print_claset"
   2.332 -    "print_classes"
   2.333 -    "print_codesetup"
   2.334 -    "print_commands"
   2.335 -    "print_configs"
   2.336 -    "print_context"
   2.337 -    "print_drafts"
   2.338 -    "print_facts"
   2.339 -    "print_induct_rules"
   2.340 -    "print_interps"
   2.341 -    "print_locale"
   2.342 -    "print_locales"
   2.343 -    "print_methods"
   2.344 -    "print_noatp_rules"
   2.345 -    "print_orders"
   2.346 -    "print_rules"
   2.347 -    "print_simpset"
   2.348 -    "print_statement"
   2.349 -    "print_syntax"
   2.350 -    "print_theorems"
   2.351 -    "print_theory"
   2.352 -    "print_trans_rules"
   2.353 -    "prop"
   2.354 -    "pwd"
   2.355 -    "quickcheck"
   2.356 -    "refute"
   2.357 -    "remove_thy"
   2.358 -    "sledgehammer"
   2.359 -    "term"
   2.360 -    "thm"
   2.361 -    "thm_deps"
   2.362 -    "thy_deps"
   2.363 -    "touch_child_thys"
   2.364 -    "touch_thy"
   2.365 -    "typ"
   2.366 -    "use"
   2.367 -    "use_thy"
   2.368 -    "value"
   2.369 -    "welcome"))
   2.370 -
   2.371 -(defconst isar-keywords-theory-begin
   2.372 -  '("theory"))
   2.373 -
   2.374 -(defconst isar-keywords-theory-switch
   2.375 -  '())
   2.376 -
   2.377 -(defconst isar-keywords-theory-end
   2.378 -  '("end"))
   2.379 -
   2.380 -(defconst isar-keywords-theory-heading
   2.381 -  '("chapter"
   2.382 -    "section"
   2.383 -    "subsection"
   2.384 -    "subsubsection"))
   2.385 -
   2.386 -(defconst isar-keywords-theory-decl
   2.387 -  '("ML_setup"
   2.388 -    "abbreviation"
   2.389 -    "arities"
   2.390 -    "atom_decl"
   2.391 -    "axclass"
   2.392 -    "axiomatization"
   2.393 -    "axioms"
   2.394 -    "class"
   2.395 -    "classes"
   2.396 -    "classrel"
   2.397 -    "code_class"
   2.398 -    "code_const"
   2.399 -    "code_datatype"
   2.400 -    "code_exception"
   2.401 -    "code_instance"
   2.402 -    "code_library"
   2.403 -    "code_module"
   2.404 -    "code_modulename"
   2.405 -    "code_moduleprolog"
   2.406 -    "code_monad"
   2.407 -    "code_props"
   2.408 -    "code_reserved"
   2.409 -    "code_type"
   2.410 -    "coinductive"
   2.411 -    "coinductive_set"
   2.412 -    "constdefs"
   2.413 -    "consts"
   2.414 -    "consts_code"
   2.415 -    "context"
   2.416 -    "datatype"
   2.417 -    "declaration"
   2.418 -    "declare"
   2.419 -    "defaultsort"
   2.420 -    "defer_recdef"
   2.421 -    "definition"
   2.422 -    "defs"
   2.423 -    "equivariance"
   2.424 -    "extract"
   2.425 -    "extract_type"
   2.426 -    "finalconsts"
   2.427 -    "fun"
   2.428 -    "global"
   2.429 -    "hide"
   2.430 -    "inductive"
   2.431 -    "inductive_set"
   2.432 -    "instantiation"
   2.433 -    "judgment"
   2.434 -    "lemmas"
   2.435 -    "local"
   2.436 -    "locale"
   2.437 -    "method_setup"
   2.438 -    "no_syntax"
   2.439 -    "no_translations"
   2.440 -    "nominal_datatype"
   2.441 -    "nonterminals"
   2.442 -    "notation"
   2.443 -    "oracle"
   2.444 -    "parse_ast_translation"
   2.445 -    "parse_translation"
   2.446 -    "primrec"
   2.447 -    "print_ast_translation"
   2.448 -    "print_translation"
   2.449 -    "quickcheck_params"
   2.450 -    "realizability"
   2.451 -    "realizers"
   2.452 -    "recdef"
   2.453 -    "record"
   2.454 -    "refute_params"
   2.455 -    "rep_datatype"
   2.456 -    "setup"
   2.457 -    "simproc_setup"
   2.458 -    "syntax"
   2.459 -    "text"
   2.460 -    "text_raw"
   2.461 -    "theorems"
   2.462 -    "token_translation"
   2.463 -    "translations"
   2.464 -    "typed_print_translation"
   2.465 -    "typedecl"
   2.466 -    "types"
   2.467 -    "types_code"))
   2.468 -
   2.469 -(defconst isar-keywords-theory-script
   2.470 -  '("inductive_cases"))
   2.471 -
   2.472 -(defconst isar-keywords-theory-goal
   2.473 -  '("ax_specification"
   2.474 -    "corollary"
   2.475 -    "function"
   2.476 -    "instance"
   2.477 -    "instance_proof"
   2.478 -    "interpretation"
   2.479 -    "lemma"
   2.480 -    "nominal_inductive"
   2.481 -    "nominal_primrec"
   2.482 -    "recdef_tc"
   2.483 -    "specification"
   2.484 -    "termination"
   2.485 -    "theorem"
   2.486 -    "typedef"))
   2.487 -
   2.488 -(defconst isar-keywords-qed
   2.489 -  '("\\."
   2.490 -    "\\.\\."
   2.491 -    "by"
   2.492 -    "done"
   2.493 -    "sorry"))
   2.494 -
   2.495 -(defconst isar-keywords-qed-block
   2.496 -  '("qed"))
   2.497 -
   2.498 -(defconst isar-keywords-qed-global
   2.499 -  '("oops"))
   2.500 -
   2.501 -(defconst isar-keywords-proof-heading
   2.502 -  '("sect"
   2.503 -    "subsect"
   2.504 -    "subsubsect"))
   2.505 -
   2.506 -(defconst isar-keywords-proof-goal
   2.507 -  '("have"
   2.508 -    "hence"
   2.509 -    "interpret"
   2.510 -    "invoke"))
   2.511 -
   2.512 -(defconst isar-keywords-proof-block
   2.513 -  '("next"
   2.514 -    "proof"))
   2.515 -
   2.516 -(defconst isar-keywords-proof-open
   2.517 -  '("{"))
   2.518 -
   2.519 -(defconst isar-keywords-proof-close
   2.520 -  '("}"))
   2.521 -
   2.522 -(defconst isar-keywords-proof-chain
   2.523 -  '("finally"
   2.524 -    "from"
   2.525 -    "then"
   2.526 -    "ultimately"
   2.527 -    "with"))
   2.528 -
   2.529 -(defconst isar-keywords-proof-decl
   2.530 -  '("also"
   2.531 -    "let"
   2.532 -    "moreover"
   2.533 -    "note"
   2.534 -    "txt"
   2.535 -    "txt_raw"
   2.536 -    "unfolding"
   2.537 -    "using"))
   2.538 -
   2.539 -(defconst isar-keywords-proof-asm
   2.540 -  '("assume"
   2.541 -    "case"
   2.542 -    "def"
   2.543 -    "fix"
   2.544 -    "presume"))
   2.545 -
   2.546 -(defconst isar-keywords-proof-asm-goal
   2.547 -  '("guess"
   2.548 -    "obtain"
   2.549 -    "show"
   2.550 -    "thus"))
   2.551 -
   2.552 -(defconst isar-keywords-proof-script
   2.553 -  '("apply"
   2.554 -    "apply_end"
   2.555 -    "back"
   2.556 -    "defer"
   2.557 -    "prefer"))
   2.558 -
   2.559 -(provide 'isar-keywords)