keyword classification tables for Isabelle/Isar Proof General
authorwenzelm
Fri Aug 31 18:43:27 2001 +0200 (2001-08-31)
changeset 11538f8588786cc9c
parent 11537 e007d35359c3
child 11539 0f17da240450
keyword classification tables for Isabelle/Isar Proof General
(generated by ProofGeneral.write_keywords from Isabelle/HOLCF/IOA);
etc/isar-keywords.el
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/etc/isar-keywords.el	Fri Aug 31 18:43:27 2001 +0200
     1.3 @@ -0,0 +1,406 @@
     1.4 +;;
     1.5 +;; Keyword classification tables for Isabelle/Isar.
     1.6 +;; This file was generated by Isabelle/HOLCF/IOA -- 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\\.context_thy_only"
    1.18 +    "ProofGeneral\\.inform_file_processed"
    1.19 +    "ProofGeneral\\.inform_file_retracted"
    1.20 +    "ProofGeneral\\.kill_proof"
    1.21 +    "ProofGeneral\\.restart"
    1.22 +    "ProofGeneral\\.try_context_thy_only"
    1.23 +    "ProofGeneral\\.undo"
    1.24 +    "also"
    1.25 +    "apply"
    1.26 +    "apply_end"
    1.27 +    "arities"
    1.28 +    "assume"
    1.29 +    "automaton"
    1.30 +    "axclass"
    1.31 +    "axioms"
    1.32 +    "back"
    1.33 +    "by"
    1.34 +    "cannot_undo"
    1.35 +    "case"
    1.36 +    "cd"
    1.37 +    "chapter"
    1.38 +    "classes"
    1.39 +    "classrel"
    1.40 +    "clear_undos"
    1.41 +    "coinductive"
    1.42 +    "commit"
    1.43 +    "constdefs"
    1.44 +    "consts"
    1.45 +    "consts_code"
    1.46 +    "context"
    1.47 +    "datatype"
    1.48 +    "declare"
    1.49 +    "def"
    1.50 +    "defaultsort"
    1.51 +    "defer"
    1.52 +    "defer_recdef"
    1.53 +    "defs"
    1.54 +    "disable_pr"
    1.55 +    "done"
    1.56 +    "enable_pr"
    1.57 +    "end"
    1.58 +    "exit"
    1.59 +    "finally"
    1.60 +    "fix"
    1.61 +    "from"
    1.62 +    "full_prf"
    1.63 +    "generate_code"
    1.64 +    "global"
    1.65 +    "have"
    1.66 +    "header"
    1.67 +    "hence"
    1.68 +    "hide"
    1.69 +    "inductive"
    1.70 +    "inductive_cases"
    1.71 +    "init_toplevel"
    1.72 +    "instance"
    1.73 +    "judgment"
    1.74 +    "kill"
    1.75 +    "kill_thy"
    1.76 +    "lemma"
    1.77 +    "lemmas"
    1.78 +    "let"
    1.79 +    "local"
    1.80 +    "method_setup"
    1.81 +    "moreover"
    1.82 +    "next"
    1.83 +    "nonterminals"
    1.84 +    "note"
    1.85 +    "obtain"
    1.86 +    "oops"
    1.87 +    "oracle"
    1.88 +    "parse_ast_translation"
    1.89 +    "parse_translation"
    1.90 +    "pr"
    1.91 +    "prefer"
    1.92 +    "presume"
    1.93 +    "pretty_setmargin"
    1.94 +    "prf"
    1.95 +    "primrec"
    1.96 +    "print_antiquotations"
    1.97 +    "print_ast_translation"
    1.98 +    "print_attributes"
    1.99 +    "print_binds"
   1.100 +    "print_cases"
   1.101 +    "print_claset"
   1.102 +    "print_commands"
   1.103 +    "print_context"
   1.104 +    "print_facts"
   1.105 +    "print_methods"
   1.106 +    "print_simpset"
   1.107 +    "print_syntax"
   1.108 +    "print_theorems"
   1.109 +    "print_theory"
   1.110 +    "print_trans_rules"
   1.111 +    "print_translation"
   1.112 +    "proof"
   1.113 +    "prop"
   1.114 +    "pwd"
   1.115 +    "qed"
   1.116 +    "quit"
   1.117 +    "recdef"
   1.118 +    "recdef_tc"
   1.119 +    "record"
   1.120 +    "redo"
   1.121 +    "remove_thy"
   1.122 +    "rep_datatype"
   1.123 +    "sect"
   1.124 +    "section"
   1.125 +    "setup"
   1.126 +    "show"
   1.127 +    "sorry"
   1.128 +    "subsect"
   1.129 +    "subsection"
   1.130 +    "subsubsect"
   1.131 +    "subsubsection"
   1.132 +    "syntax"
   1.133 +    "term"
   1.134 +    "text"
   1.135 +    "text_raw"
   1.136 +    "then"
   1.137 +    "theorem"
   1.138 +    "theorems"
   1.139 +    "theory"
   1.140 +    "thm"
   1.141 +    "thm_deps"
   1.142 +    "thms_containing"
   1.143 +    "thus"
   1.144 +    "token_translation"
   1.145 +    "touch_all_thys"
   1.146 +    "touch_child_thys"
   1.147 +    "touch_thy"
   1.148 +    "translations"
   1.149 +    "txt"
   1.150 +    "txt_raw"
   1.151 +    "typ"
   1.152 +    "typed_print_translation"
   1.153 +    "typedecl"
   1.154 +    "typedef"
   1.155 +    "types"
   1.156 +    "types_code"
   1.157 +    "ultimately"
   1.158 +    "undo"
   1.159 +    "undos_proof"
   1.160 +    "update_thy"
   1.161 +    "update_thy_only"
   1.162 +    "use"
   1.163 +    "use_thy"
   1.164 +    "use_thy_only"
   1.165 +    "welcome"
   1.166 +    "with"
   1.167 +    "{"
   1.168 +    "}"))
   1.169 +
   1.170 +(defconst isar-keywords-minor
   1.171 +  '("actions"
   1.172 +    "and"
   1.173 +    "binder"
   1.174 +    "compose"
   1.175 +    "con_defs"
   1.176 +    "concl"
   1.177 +    "congs"
   1.178 +    "distinct"
   1.179 +    "files"
   1.180 +    "hide_action"
   1.181 +    "hints"
   1.182 +    "in"
   1.183 +    "induction"
   1.184 +    "infixl"
   1.185 +    "infixr"
   1.186 +    "initially"
   1.187 +    "inject"
   1.188 +    "inputs"
   1.189 +    "internals"
   1.190 +    "intros"
   1.191 +    "is"
   1.192 +    "monos"
   1.193 +    "output"
   1.194 +    "outputs"
   1.195 +    "overloaded"
   1.196 +    "post"
   1.197 +    "pre"
   1.198 +    "rename"
   1.199 +    "restrict"
   1.200 +    "signature"
   1.201 +    "states"
   1.202 +    "to"
   1.203 +    "transitions"
   1.204 +    "transrel"
   1.205 +    "using"
   1.206 +    "where"))
   1.207 +
   1.208 +(defconst isar-keywords-control
   1.209 +  '("ProofGeneral\\.context_thy_only"
   1.210 +    "ProofGeneral\\.inform_file_processed"
   1.211 +    "ProofGeneral\\.inform_file_retracted"
   1.212 +    "ProofGeneral\\.kill_proof"
   1.213 +    "ProofGeneral\\.restart"
   1.214 +    "ProofGeneral\\.try_context_thy_only"
   1.215 +    "ProofGeneral\\.undo"
   1.216 +    "cannot_undo"
   1.217 +    "clear_undos"
   1.218 +    "exit"
   1.219 +    "init_toplevel"
   1.220 +    "kill"
   1.221 +    "quit"
   1.222 +    "redo"
   1.223 +    "undo"
   1.224 +    "undos_proof"))
   1.225 +
   1.226 +(defconst isar-keywords-diag
   1.227 +  '("ML"
   1.228 +    "ML_command"
   1.229 +    "cd"
   1.230 +    "commit"
   1.231 +    "disable_pr"
   1.232 +    "enable_pr"
   1.233 +    "full_prf"
   1.234 +    "header"
   1.235 +    "kill_thy"
   1.236 +    "pr"
   1.237 +    "pretty_setmargin"
   1.238 +    "prf"
   1.239 +    "print_antiquotations"
   1.240 +    "print_attributes"
   1.241 +    "print_binds"
   1.242 +    "print_cases"
   1.243 +    "print_claset"
   1.244 +    "print_commands"
   1.245 +    "print_context"
   1.246 +    "print_facts"
   1.247 +    "print_methods"
   1.248 +    "print_simpset"
   1.249 +    "print_syntax"
   1.250 +    "print_theorems"
   1.251 +    "print_theory"
   1.252 +    "print_trans_rules"
   1.253 +    "prop"
   1.254 +    "pwd"
   1.255 +    "remove_thy"
   1.256 +    "term"
   1.257 +    "thm"
   1.258 +    "thm_deps"
   1.259 +    "thms_containing"
   1.260 +    "touch_all_thys"
   1.261 +    "touch_child_thys"
   1.262 +    "touch_thy"
   1.263 +    "typ"
   1.264 +    "update_thy"
   1.265 +    "update_thy_only"
   1.266 +    "use"
   1.267 +    "use_thy"
   1.268 +    "use_thy_only"
   1.269 +    "welcome"))
   1.270 +
   1.271 +(defconst isar-keywords-theory-begin
   1.272 +  '("theory"))
   1.273 +
   1.274 +(defconst isar-keywords-theory-switch
   1.275 +  '("context"))
   1.276 +
   1.277 +(defconst isar-keywords-theory-end
   1.278 +  '("end"))
   1.279 +
   1.280 +(defconst isar-keywords-theory-heading
   1.281 +  '("chapter"
   1.282 +    "section"
   1.283 +    "subsection"
   1.284 +    "subsubsection"))
   1.285 +
   1.286 +(defconst isar-keywords-theory-decl
   1.287 +  '("ML_setup"
   1.288 +    "arities"
   1.289 +    "automaton"
   1.290 +    "axclass"
   1.291 +    "axioms"
   1.292 +    "classes"
   1.293 +    "classrel"
   1.294 +    "coinductive"
   1.295 +    "constdefs"
   1.296 +    "consts"
   1.297 +    "consts_code"
   1.298 +    "datatype"
   1.299 +    "defaultsort"
   1.300 +    "defer_recdef"
   1.301 +    "defs"
   1.302 +    "generate_code"
   1.303 +    "global"
   1.304 +    "hide"
   1.305 +    "inductive"
   1.306 +    "judgment"
   1.307 +    "lemmas"
   1.308 +    "local"
   1.309 +    "method_setup"
   1.310 +    "nonterminals"
   1.311 +    "oracle"
   1.312 +    "parse_ast_translation"
   1.313 +    "parse_translation"
   1.314 +    "primrec"
   1.315 +    "print_ast_translation"
   1.316 +    "print_translation"
   1.317 +    "recdef"
   1.318 +    "record"
   1.319 +    "rep_datatype"
   1.320 +    "setup"
   1.321 +    "syntax"
   1.322 +    "text"
   1.323 +    "text_raw"
   1.324 +    "theorems"
   1.325 +    "token_translation"
   1.326 +    "translations"
   1.327 +    "typed_print_translation"
   1.328 +    "typedecl"
   1.329 +    "types"
   1.330 +    "types_code"))
   1.331 +
   1.332 +(defconst isar-keywords-theory-script
   1.333 +  '("declare"
   1.334 +    "inductive_cases"))
   1.335 +
   1.336 +(defconst isar-keywords-theory-goal
   1.337 +  '("instance"
   1.338 +    "lemma"
   1.339 +    "recdef_tc"
   1.340 +    "theorem"
   1.341 +    "typedef"))
   1.342 +
   1.343 +(defconst isar-keywords-qed
   1.344 +  '("\\."
   1.345 +    "\\.\\."
   1.346 +    "by"
   1.347 +    "done"
   1.348 +    "sorry"))
   1.349 +
   1.350 +(defconst isar-keywords-qed-block
   1.351 +  '("qed"))
   1.352 +
   1.353 +(defconst isar-keywords-qed-global
   1.354 +  '("oops"))
   1.355 +
   1.356 +(defconst isar-keywords-proof-heading
   1.357 +  '("sect"
   1.358 +    "subsect"
   1.359 +    "subsubsect"))
   1.360 +
   1.361 +(defconst isar-keywords-proof-goal
   1.362 +  '("have"
   1.363 +    "hence"
   1.364 +    "show"
   1.365 +    "thus"))
   1.366 +
   1.367 +(defconst isar-keywords-proof-block
   1.368 +  '("next"
   1.369 +    "proof"))
   1.370 +
   1.371 +(defconst isar-keywords-proof-open
   1.372 +  '("{"))
   1.373 +
   1.374 +(defconst isar-keywords-proof-close
   1.375 +  '("}"))
   1.376 +
   1.377 +(defconst isar-keywords-proof-chain
   1.378 +  '("finally"
   1.379 +    "from"
   1.380 +    "then"
   1.381 +    "ultimately"
   1.382 +    "with"))
   1.383 +
   1.384 +(defconst isar-keywords-proof-decl
   1.385 +  '("also"
   1.386 +    "let"
   1.387 +    "moreover"
   1.388 +    "note"
   1.389 +    "txt"
   1.390 +    "txt_raw"))
   1.391 +
   1.392 +(defconst isar-keywords-proof-asm
   1.393 +  '("assume"
   1.394 +    "case"
   1.395 +    "def"
   1.396 +    "fix"
   1.397 +    "presume"))
   1.398 +
   1.399 +(defconst isar-keywords-proof-asm-goal
   1.400 +  '("obtain"))
   1.401 +
   1.402 +(defconst isar-keywords-proof-script
   1.403 +  '("apply"
   1.404 +    "apply_end"
   1.405 +    "back"
   1.406 +    "defer"
   1.407 +    "prefer"))
   1.408 +
   1.409 +(provide 'isar-keywords)