1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/etc/isar-keywords-HOL-Nominal.el Fri Apr 28 16:04:57 2006 +0200
1.3 @@ -0,0 +1,504 @@
1.4 +;;
1.5 +;; Keyword classification tables for Isabelle/Isar.
1.6 +;; This file was generated by Isabelle/HOL/HOL-Nominal -- DO NOT EDIT!
1.7 +;;
1.8 +;; $Id$
1.9 +;;
1.10 +
1.11 +(defconst isar-keywords-major
1.12 + '("\\."
1.13 + "\\.\\."
1.14 + "ML"
1.15 + "ML_command"
1.16 + "ML_setup"
1.17 + "ProofGeneral\\.call_atp"
1.18 + "ProofGeneral\\.context_thy_only"
1.19 + "ProofGeneral\\.inform_file_processed"
1.20 + "ProofGeneral\\.inform_file_retracted"
1.21 + "ProofGeneral\\.kill_proof"
1.22 + "ProofGeneral\\.process_pgip"
1.23 + "ProofGeneral\\.redo"
1.24 + "ProofGeneral\\.restart"
1.25 + "ProofGeneral\\.try_context_thy_only"
1.26 + "ProofGeneral\\.undo"
1.27 + "abbreviation"
1.28 + "also"
1.29 + "apply"
1.30 + "apply_end"
1.31 + "arities"
1.32 + "assume"
1.33 + "atom_decl"
1.34 + "ax_specification"
1.35 + "axclass"
1.36 + "axiomatization"
1.37 + "axioms"
1.38 + "back"
1.39 + "by"
1.40 + "cannot_undo"
1.41 + "case"
1.42 + "cd"
1.43 + "chapter"
1.44 + "class"
1.45 + "classes"
1.46 + "classrel"
1.47 + "clear_undos"
1.48 + "code_alias"
1.49 + "code_generate"
1.50 + "code_library"
1.51 + "code_module"
1.52 + "code_primclass"
1.53 + "code_primconst"
1.54 + "code_primtyco"
1.55 + "code_purge"
1.56 + "code_serialize"
1.57 + "code_syntax_const"
1.58 + "code_syntax_tyco"
1.59 + "coinductive"
1.60 + "commit"
1.61 + "constdefs"
1.62 + "consts"
1.63 + "consts_code"
1.64 + "context"
1.65 + "corollary"
1.66 + "datatype"
1.67 + "declare"
1.68 + "def"
1.69 + "defaultsort"
1.70 + "defer"
1.71 + "defer_recdef"
1.72 + "definition"
1.73 + "defs"
1.74 + "disable_pr"
1.75 + "display_drafts"
1.76 + "done"
1.77 + "enable_pr"
1.78 + "end"
1.79 + "exit"
1.80 + "extract"
1.81 + "extract_type"
1.82 + "finalconsts"
1.83 + "finally"
1.84 + "find_theorems"
1.85 + "fix"
1.86 + "from"
1.87 + "full_prf"
1.88 + "global"
1.89 + "guess"
1.90 + "have"
1.91 + "header"
1.92 + "hence"
1.93 + "hide"
1.94 + "inductive"
1.95 + "inductive_cases"
1.96 + "init_toplevel"
1.97 + "instance"
1.98 + "interpret"
1.99 + "interpretation"
1.100 + "judgment"
1.101 + "kill"
1.102 + "kill_thy"
1.103 + "lemma"
1.104 + "lemmas"
1.105 + "let"
1.106 + "local"
1.107 + "locale"
1.108 + "method_setup"
1.109 + "moreover"
1.110 + "next"
1.111 + "no_syntax"
1.112 + "no_translations"
1.113 + "nominal_datatype"
1.114 + "nonterminals"
1.115 + "norm_by_eval"
1.116 + "note"
1.117 + "obtain"
1.118 + "oops"
1.119 + "oracle"
1.120 + "parse_ast_translation"
1.121 + "parse_translation"
1.122 + "pr"
1.123 + "prefer"
1.124 + "presume"
1.125 + "pretty_setmargin"
1.126 + "prf"
1.127 + "primrec"
1.128 + "print_antiquotations"
1.129 + "print_ast_translation"
1.130 + "print_attributes"
1.131 + "print_binds"
1.132 + "print_cases"
1.133 + "print_claset"
1.134 + "print_commands"
1.135 + "print_context"
1.136 + "print_drafts"
1.137 + "print_facts"
1.138 + "print_induct_rules"
1.139 + "print_interps"
1.140 + "print_locale"
1.141 + "print_locales"
1.142 + "print_methods"
1.143 + "print_rules"
1.144 + "print_simpset"
1.145 + "print_statement"
1.146 + "print_syntax"
1.147 + "print_theorems"
1.148 + "print_theory"
1.149 + "print_trans_rules"
1.150 + "print_translation"
1.151 + "proof"
1.152 + "prop"
1.153 + "pwd"
1.154 + "qed"
1.155 + "quickcheck"
1.156 + "quickcheck_params"
1.157 + "quit"
1.158 + "realizability"
1.159 + "realizers"
1.160 + "recdef"
1.161 + "recdef_tc"
1.162 + "record"
1.163 + "redo"
1.164 + "refute"
1.165 + "refute_params"
1.166 + "remove_thy"
1.167 + "rep_datatype"
1.168 + "sect"
1.169 + "section"
1.170 + "setup"
1.171 + "show"
1.172 + "sorry"
1.173 + "specification"
1.174 + "subsect"
1.175 + "subsection"
1.176 + "subsubsect"
1.177 + "subsubsection"
1.178 + "syntax"
1.179 + "term"
1.180 + "text"
1.181 + "text_raw"
1.182 + "then"
1.183 + "theorem"
1.184 + "theorems"
1.185 + "theory"
1.186 + "thm"
1.187 + "thm_deps"
1.188 + "thus"
1.189 + "token_translation"
1.190 + "touch_all_thys"
1.191 + "touch_child_thys"
1.192 + "touch_thy"
1.193 + "translations"
1.194 + "txt"
1.195 + "txt_raw"
1.196 + "typ"
1.197 + "typed_print_translation"
1.198 + "typedecl"
1.199 + "typedef"
1.200 + "types"
1.201 + "types_code"
1.202 + "ultimately"
1.203 + "undo"
1.204 + "undos_proof"
1.205 + "unfolding"
1.206 + "update_thy"
1.207 + "update_thy_only"
1.208 + "use"
1.209 + "use_thy"
1.210 + "use_thy_only"
1.211 + "using"
1.212 + "value"
1.213 + "welcome"
1.214 + "with"
1.215 + "{"
1.216 + "}"))
1.217 +
1.218 +(defconst isar-keywords-minor
1.219 + '("advanced"
1.220 + "and"
1.221 + "assumes"
1.222 + "attach"
1.223 + "begin"
1.224 + "binder"
1.225 + "concl"
1.226 + "congs"
1.227 + "constrains"
1.228 + "contains"
1.229 + "defines"
1.230 + "distinct"
1.231 + "file"
1.232 + "fixes"
1.233 + "hints"
1.234 + "imports"
1.235 + "in"
1.236 + "includes"
1.237 + "induction"
1.238 + "infix"
1.239 + "infixl"
1.240 + "infixr"
1.241 + "inject"
1.242 + "intros"
1.243 + "is"
1.244 + "monos"
1.245 + "morphisms"
1.246 + "notes"
1.247 + "obtains"
1.248 + "open"
1.249 + "output"
1.250 + "overloaded"
1.251 + "permissive"
1.252 + "shows"
1.253 + "structure"
1.254 + "target_atom"
1.255 + "uses"
1.256 + "where"))
1.257 +
1.258 +(defconst isar-keywords-control
1.259 + '("ProofGeneral\\.context_thy_only"
1.260 + "ProofGeneral\\.inform_file_processed"
1.261 + "ProofGeneral\\.inform_file_retracted"
1.262 + "ProofGeneral\\.kill_proof"
1.263 + "ProofGeneral\\.process_pgip"
1.264 + "ProofGeneral\\.redo"
1.265 + "ProofGeneral\\.restart"
1.266 + "ProofGeneral\\.try_context_thy_only"
1.267 + "ProofGeneral\\.undo"
1.268 + "cannot_undo"
1.269 + "clear_undos"
1.270 + "exit"
1.271 + "init_toplevel"
1.272 + "kill"
1.273 + "quit"
1.274 + "redo"
1.275 + "undo"
1.276 + "undos_proof"))
1.277 +
1.278 +(defconst isar-keywords-diag
1.279 + '("ML"
1.280 + "ML_command"
1.281 + "ProofGeneral\\.call_atp"
1.282 + "cd"
1.283 + "commit"
1.284 + "disable_pr"
1.285 + "display_drafts"
1.286 + "enable_pr"
1.287 + "find_theorems"
1.288 + "full_prf"
1.289 + "header"
1.290 + "kill_thy"
1.291 + "pr"
1.292 + "pretty_setmargin"
1.293 + "prf"
1.294 + "print_antiquotations"
1.295 + "print_attributes"
1.296 + "print_binds"
1.297 + "print_cases"
1.298 + "print_claset"
1.299 + "print_commands"
1.300 + "print_context"
1.301 + "print_drafts"
1.302 + "print_facts"
1.303 + "print_induct_rules"
1.304 + "print_interps"
1.305 + "print_locale"
1.306 + "print_locales"
1.307 + "print_methods"
1.308 + "print_rules"
1.309 + "print_simpset"
1.310 + "print_statement"
1.311 + "print_syntax"
1.312 + "print_theorems"
1.313 + "print_theory"
1.314 + "print_trans_rules"
1.315 + "prop"
1.316 + "pwd"
1.317 + "quickcheck"
1.318 + "refute"
1.319 + "remove_thy"
1.320 + "term"
1.321 + "thm"
1.322 + "thm_deps"
1.323 + "touch_all_thys"
1.324 + "touch_child_thys"
1.325 + "touch_thy"
1.326 + "typ"
1.327 + "update_thy"
1.328 + "update_thy_only"
1.329 + "use"
1.330 + "use_thy"
1.331 + "use_thy_only"
1.332 + "value"
1.333 + "welcome"))
1.334 +
1.335 +(defconst isar-keywords-theory-begin
1.336 + '("theory"))
1.337 +
1.338 +(defconst isar-keywords-theory-switch
1.339 + '("context"))
1.340 +
1.341 +(defconst isar-keywords-theory-end
1.342 + '("end"))
1.343 +
1.344 +(defconst isar-keywords-theory-heading
1.345 + '("chapter"
1.346 + "section"
1.347 + "subsection"
1.348 + "subsubsection"))
1.349 +
1.350 +(defconst isar-keywords-theory-decl
1.351 + '("ML_setup"
1.352 + "abbreviation"
1.353 + "arities"
1.354 + "atom_decl"
1.355 + "axclass"
1.356 + "axiomatization"
1.357 + "axioms"
1.358 + "class"
1.359 + "classes"
1.360 + "classrel"
1.361 + "code_alias"
1.362 + "code_generate"
1.363 + "code_library"
1.364 + "code_module"
1.365 + "code_primclass"
1.366 + "code_primconst"
1.367 + "code_primtyco"
1.368 + "code_purge"
1.369 + "code_serialize"
1.370 + "code_syntax_const"
1.371 + "code_syntax_tyco"
1.372 + "coinductive"
1.373 + "constdefs"
1.374 + "consts"
1.375 + "consts_code"
1.376 + "datatype"
1.377 + "defaultsort"
1.378 + "defer_recdef"
1.379 + "definition"
1.380 + "defs"
1.381 + "extract"
1.382 + "extract_type"
1.383 + "finalconsts"
1.384 + "global"
1.385 + "hide"
1.386 + "inductive"
1.387 + "judgment"
1.388 + "lemmas"
1.389 + "local"
1.390 + "locale"
1.391 + "method_setup"
1.392 + "no_syntax"
1.393 + "no_translations"
1.394 + "nominal_datatype"
1.395 + "nonterminals"
1.396 + "norm_by_eval"
1.397 + "oracle"
1.398 + "parse_ast_translation"
1.399 + "parse_translation"
1.400 + "primrec"
1.401 + "print_ast_translation"
1.402 + "print_translation"
1.403 + "quickcheck_params"
1.404 + "realizability"
1.405 + "realizers"
1.406 + "recdef"
1.407 + "record"
1.408 + "refute_params"
1.409 + "rep_datatype"
1.410 + "setup"
1.411 + "syntax"
1.412 + "text"
1.413 + "text_raw"
1.414 + "theorems"
1.415 + "token_translation"
1.416 + "translations"
1.417 + "typed_print_translation"
1.418 + "typedecl"
1.419 + "types"
1.420 + "types_code"))
1.421 +
1.422 +(defconst isar-keywords-theory-script
1.423 + '("declare"
1.424 + "inductive_cases"))
1.425 +
1.426 +(defconst isar-keywords-theory-goal
1.427 + '("ax_specification"
1.428 + "corollary"
1.429 + "instance"
1.430 + "interpretation"
1.431 + "lemma"
1.432 + "recdef_tc"
1.433 + "specification"
1.434 + "theorem"
1.435 + "typedef"))
1.436 +
1.437 +(defconst isar-keywords-qed
1.438 + '("\\."
1.439 + "\\.\\."
1.440 + "by"
1.441 + "done"
1.442 + "sorry"))
1.443 +
1.444 +(defconst isar-keywords-qed-block
1.445 + '("qed"))
1.446 +
1.447 +(defconst isar-keywords-qed-global
1.448 + '("oops"))
1.449 +
1.450 +(defconst isar-keywords-proof-heading
1.451 + '("sect"
1.452 + "subsect"
1.453 + "subsubsect"))
1.454 +
1.455 +(defconst isar-keywords-proof-goal
1.456 + '("have"
1.457 + "hence"
1.458 + "interpret"
1.459 + "show"
1.460 + "thus"))
1.461 +
1.462 +(defconst isar-keywords-proof-block
1.463 + '("next"
1.464 + "proof"))
1.465 +
1.466 +(defconst isar-keywords-proof-open
1.467 + '("{"))
1.468 +
1.469 +(defconst isar-keywords-proof-close
1.470 + '("}"))
1.471 +
1.472 +(defconst isar-keywords-proof-chain
1.473 + '("finally"
1.474 + "from"
1.475 + "then"
1.476 + "ultimately"
1.477 + "with"))
1.478 +
1.479 +(defconst isar-keywords-proof-decl
1.480 + '("also"
1.481 + "let"
1.482 + "moreover"
1.483 + "note"
1.484 + "txt"
1.485 + "txt_raw"
1.486 + "unfolding"
1.487 + "using"))
1.488 +
1.489 +(defconst isar-keywords-proof-asm
1.490 + '("assume"
1.491 + "case"
1.492 + "def"
1.493 + "fix"
1.494 + "presume"))
1.495 +
1.496 +(defconst isar-keywords-proof-asm-goal
1.497 + '("guess"
1.498 + "obtain"))
1.499 +
1.500 +(defconst isar-keywords-proof-script
1.501 + '("apply"
1.502 + "apply_end"
1.503 + "back"
1.504 + "defer"
1.505 + "prefer"))
1.506 +
1.507 +(provide 'isar-keywords)