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