wenzelm@11538: ;; wenzelm@11538: ;; Keyword classification tables for Isabelle/Isar. blanchet@49510: ;; Generated from HOLCF + HOL-BNF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import. wenzelm@24904: ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** wenzelm@11538: ;; wenzelm@11538: wenzelm@11538: (defconst isar-keywords-major wenzelm@11538: '("\\." wenzelm@15762: "\\.\\." wenzelm@25577: "Isabelle\\.command" wenzelm@11538: "ML" wenzelm@11538: "ML_command" wenzelm@48867: "ML_file" wenzelm@28280: "ML_prf" wenzelm@26394: "ML_val" wenzelm@11538: "ProofGeneral\\.inform_file_processed" wenzelm@11538: "ProofGeneral\\.inform_file_retracted" wenzelm@11538: "ProofGeneral\\.kill_proof" wenzelm@33874: "ProofGeneral\\.pr" wenzelm@14938: "ProofGeneral\\.process_pgip" wenzelm@11538: "ProofGeneral\\.restart" wenzelm@11538: "ProofGeneral\\.undo" wenzelm@19069: "abbreviation" wenzelm@11538: "also" wenzelm@11538: "apply" wenzelm@11538: "apply_end" wenzelm@11538: "arities" wenzelm@11538: "assume" wenzelm@24904: "atom_decl" wenzelm@30527: "attribute_setup" skalberg@14223: "ax_specification" wenzelm@18612: "axiomatization" wenzelm@11538: "axioms" wenzelm@11538: "back" blanchet@48981: "bnf_def" wenzelm@33687: "boogie_end" wenzelm@33687: "boogie_open" wenzelm@33687: "boogie_status" wenzelm@33687: "boogie_vc" wenzelm@47057: "bundle" wenzelm@11538: "by" wenzelm@11538: "cannot_undo" wenzelm@11538: "case" wenzelm@11538: "cd" wenzelm@11538: "chapter" haftmann@18552: "class" wenzelm@20568: "class_deps" wenzelm@11538: "classes" wenzelm@11538: "classrel" blanchet@49112: "codata" haftmann@27102: "code_abort" haftmann@20424: "code_class" haftmann@20453: "code_const" haftmann@22486: "code_datatype" wenzelm@22864: "code_deps" haftmann@24997: "code_include" haftmann@20424: "code_instance" wenzelm@21203: "code_modulename" wenzelm@22084: "code_monad" bulwahn@31106: "code_pred" haftmann@36472: "code_reflect" wenzelm@21028: "code_reserved" haftmann@22288: "code_thms" haftmann@20453: "code_type" wenzelm@11538: "coinductive" berghofe@23732: "coinductive_set" wenzelm@11538: "commit" wenzelm@11538: "consts" wenzelm@11538: "context" wenzelm@11746: "corollary" huffman@16701: "cpodef" blanchet@49112: "data" wenzelm@11538: "datatype" wenzelm@22084: "declaration" wenzelm@11538: "declare" wenzelm@11538: "def" wenzelm@36455: "default_sort" wenzelm@11538: "defer" wenzelm@11538: "defer_recdef" wenzelm@18775: "definition" wenzelm@11538: "defs" wenzelm@11538: "disable_pr" wenzelm@14938: "display_drafts" wenzelm@12040: "domain" wenzelm@33840: "domain_isomorphism" haftmann@40585: "domaindef" wenzelm@11538: "done" wenzelm@11538: "enable_pr" wenzelm@11538: "end" wenzelm@41530: "enriched_type" wenzelm@24904: "equivariance" wenzelm@11538: "exit" haftmann@24343: "export_code" berghofe@13407: "extract" berghofe@13407: "extract_type" wenzelm@11538: "finally" kleing@29882: "find_consts" wenzelm@17220: "find_theorems" bulwahn@46589: "find_unused_assms" wenzelm@11538: "fix" huffman@16231: "fixrec" wenzelm@11538: "from" wenzelm@11538: "full_prf" krauss@20523: "fun" krauss@19564: "function" wenzelm@17850: "guess" wenzelm@11538: "have" wenzelm@11538: "header" wenzelm@21732: "help" wenzelm@11538: "hence" wenzelm@36180: "hide_class" wenzelm@36180: "hide_const" wenzelm@36180: "hide_fact" wenzelm@36180: "hide_type" wenzelm@47262: "import_const_map" wenzelm@47262: "import_file" wenzelm@46951: "import_tptp" wenzelm@47262: "import_type_map" wenzelm@47057: "include" wenzelm@47057: "including" wenzelm@11538: "inductive" wenzelm@11538: "inductive_cases" berghofe@23732: "inductive_set" bulwahn@37734: "inductive_simps" wenzelm@11538: "init_toplevel" wenzelm@11538: "instance" haftmann@24437: "instantiation" ballarin@15624: "interpret" ballarin@15598: "interpretation" wenzelm@11538: "judgment" wenzelm@11538: "kill" wenzelm@11538: "kill_thy" wenzelm@11538: "lemma" wenzelm@11538: "lemmas" wenzelm@11538: "let" huffman@47354: "lift_definition" wenzelm@27538: "linear_undo" wenzelm@30463: "local_setup" wenzelm@12059: "locale" wenzelm@49571: "locale_deps" wenzelm@11538: "method_setup" wenzelm@11538: "moreover" wenzelm@11538: "next" blanchet@33198: "nitpick" blanchet@33198: "nitpick_params" wenzelm@24945: "no_notation" wenzelm@15703: "no_syntax" wenzelm@19255: "no_translations" wenzelm@35414: "no_type_notation" wenzelm@24904: "nominal_datatype" wenzelm@24904: "nominal_inductive" berghofe@28656: "nominal_inductive2" wenzelm@24904: "nominal_primrec" wenzelm@41229: "nonterminal" wenzelm@21203: "notation" wenzelm@11538: "note" wenzelm@40960: "notepad" wenzelm@11538: "obtain" wenzelm@11538: "oops" wenzelm@11538: "oracle" haftmann@25516: "overloading" wenzelm@11538: "parse_ast_translation" wenzelm@11538: "parse_translation" wenzelm@40109: "partial_function" huffman@16701: "pcpodef" wenzelm@11538: "pr" wenzelm@11538: "prefer" wenzelm@11538: "presume" wenzelm@11538: "pretty_setmargin" wenzelm@11538: "prf" wenzelm@11538: "primrec" wenzelm@21732: "print_abbrevs" wenzelm@11538: "print_antiquotations" wenzelm@11538: "print_ast_translation" wenzelm@11538: "print_attributes" wenzelm@11538: "print_binds" blanchet@48981: "print_bnfs" wenzelm@47057: "print_bundles" wenzelm@11538: "print_cases" wenzelm@11538: "print_claset" haftmann@20378: "print_classes" haftmann@31130: "print_codeproc" haftmann@22288: "print_codesetup" berghofe@45061: "print_coercion_maps" berghofe@45061: "print_coercions" wenzelm@11538: "print_commands" wenzelm@24120: "print_configs" wenzelm@11538: "print_context" ballarin@41435: "print_dependencies" wenzelm@14938: "print_drafts" wenzelm@11538: "print_facts" wenzelm@11661: "print_induct_rules" ballarin@32804: "print_interps" wenzelm@12059: "print_locale" wenzelm@12059: "print_locales" wenzelm@11538: "print_methods" ballarin@24642: "print_orders" kaliszyk@35279: "print_quotconsts" kaliszyk@35279: "print_quotients" kuncar@47308: "print_quotientsQ3" kaliszyk@35279: "print_quotmaps" kuncar@47308: "print_quotmapsQ3" wenzelm@12365: "print_rules" wenzelm@11538: "print_simpset" wenzelm@19272: "print_statement" wenzelm@11538: "print_syntax" wenzelm@11538: "print_theorems" wenzelm@11538: "print_theory" wenzelm@11538: "print_trans_rules" wenzelm@11538: "print_translation" wenzelm@11538: "proof" wenzelm@11538: "prop" wenzelm@11538: "pwd" wenzelm@11538: "qed" berghofe@14109: "quickcheck" bulwahn@45926: "quickcheck_generator" berghofe@14109: "quickcheck_params" wenzelm@11538: "quit" kaliszyk@35279: "quotient_definition" kaliszyk@35279: "quotient_type" berghofe@13407: "realizability" berghofe@13407: "realizers" wenzelm@11538: "recdef" wenzelm@11538: "recdef_tc" wenzelm@11538: "record" webertj@14349: "refute" webertj@14349: "refute_params" wenzelm@11538: "remove_thy" wenzelm@11538: "rep_datatype" wenzelm@36321: "schematic_corollary" wenzelm@36321: "schematic_lemma" wenzelm@36321: "schematic_theorem" wenzelm@11538: "sect" wenzelm@11538: "section" wenzelm@11538: "setup" kuncar@47098: "setup_lifting" wenzelm@11538: "show" wenzelm@22200: "simproc_setup" wenzelm@22864: "sledgehammer" haftmann@36114: "sledgehammer_params" wenzelm@33898: "smt_status" blanchet@40117: "solve_direct" wenzelm@11538: "sorry" berghofe@41564: "spark_end" berghofe@41564: "spark_open" wenzelm@48908: "spark_open_siv" wenzelm@48908: "spark_open_vcg" berghofe@41564: "spark_proof_functions" berghofe@41564: "spark_status" berghofe@42356: "spark_types" berghofe@41564: "spark_vc" skalberg@14115: "specification" wenzelm@25176: "statespace" haftmann@24919: "subclass" ballarin@28895: "sublocale" wenzelm@11538: "subsect" wenzelm@11538: "subsection" wenzelm@11538: "subsubsect" wenzelm@11538: "subsubsection" wenzelm@11538: "syntax" wenzelm@40784: "syntax_declaration" wenzelm@11538: "term" krauss@19564: "termination" wenzelm@11538: "text" wenzelm@11538: "text_raw" wenzelm@11538: "then" wenzelm@11538: "theorem" wenzelm@11538: "theorems" wenzelm@11538: "theory" wenzelm@11538: "thm" wenzelm@11538: "thm_deps" wenzelm@11538: "thus" haftmann@22486: "thy_deps" wenzelm@11538: "translations" blanchet@38943: "try" blanchet@46641: "try0" wenzelm@11538: "txt" wenzelm@11538: "txt_raw" wenzelm@11538: "typ" wenzelm@35414: "type_notation" wenzelm@41249: "type_synonym" wenzelm@11538: "typed_print_translation" wenzelm@11538: "typedecl" wenzelm@11538: "typedef" wenzelm@11538: "ultimately" wenzelm@11538: "undo" wenzelm@11538: "undos_proof" wenzelm@18541: "unfolding" berghofe@26184: "unused_thms" wenzelm@11538: "use" wenzelm@11538: "use_thy" wenzelm@12926: "using" berghofe@17552: "value" haftmann@31130: "values" wenzelm@11538: "welcome" wenzelm@11538: "with" blanchet@49074: "wrap_data" wenzelm@36505: "write" wenzelm@11538: "{" wenzelm@11538: "}")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-minor wenzelm@37785: '("advanced" wenzelm@12040: "and" wenzelm@12042: "assumes" berghofe@16771: "attach" wenzelm@24904: "avoids" nipkow@15135: "begin" wenzelm@11538: "binder" haftmann@37824: "checking" wenzelm@11538: "congs" ballarin@16168: "constrains" haftmann@36472: "datatypes" wenzelm@49292: "defaults" wenzelm@12042: "defines" berghofe@17147: "file" wenzelm@12042: "fixes" wenzelm@19797: "for" haftmann@36472: "functions" wenzelm@11538: "hints" haftmann@22288: "identifier" wenzelm@19797: "if" nipkow@15141: "imports" wenzelm@11538: "in" wenzelm@47069: "includes" wenzelm@11661: "infix" wenzelm@11538: "infixl" wenzelm@11538: "infixr" wenzelm@11538: "is" wenzelm@46938: "keywords" wenzelm@12040: "lazy" haftmann@24249: "module_name" wenzelm@11538: "monos" wenzelm@11746: "morphisms" wenzelm@49292: "no_dests" wenzelm@12042: "notes" wenzelm@18888: "obtains" wenzelm@13364: "open" wenzelm@11538: "output" wenzelm@11538: "overloaded" wenzelm@11618: "permissive" wenzelm@33685: "pervasive" blanchet@49633: "rep_compat" wenzelm@12935: "shows" wenzelm@12042: "structure" wenzelm@19633: "unchecked" wenzelm@40386: "unsafe" wenzelm@16419: "uses" wenzelm@11538: "where")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-control wenzelm@25577: '("Isabelle\\.command" wenzelm@25577: "ProofGeneral\\.inform_file_processed" wenzelm@11538: "ProofGeneral\\.inform_file_retracted" wenzelm@11538: "ProofGeneral\\.kill_proof" wenzelm@14938: "ProofGeneral\\.process_pgip" wenzelm@11538: "ProofGeneral\\.restart" wenzelm@11538: "ProofGeneral\\.undo" wenzelm@11538: "cannot_undo" wenzelm@40396: "cd" wenzelm@40396: "commit" wenzelm@37987: "disable_pr" wenzelm@37987: "enable_pr" wenzelm@11538: "exit" wenzelm@11538: "init_toplevel" wenzelm@11538: "kill" wenzelm@37987: "kill_thy" wenzelm@27538: "linear_undo" wenzelm@11538: "quit" wenzelm@37987: "remove_thy" wenzelm@11538: "undo" wenzelm@37987: "undos_proof" wenzelm@37987: "use_thy")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-diag wenzelm@26482: '("ML_command" wenzelm@26394: "ML_val" wenzelm@33874: "ProofGeneral\\.pr" wenzelm@33687: "boogie_status" wenzelm@20568: "class_deps" wenzelm@22864: "code_deps" haftmann@22288: "code_thms" wenzelm@14938: "display_drafts" haftmann@24343: "export_code" kleing@29882: "find_consts" wenzelm@17220: "find_theorems" bulwahn@46589: "find_unused_assms" wenzelm@11538: "full_prf" wenzelm@11538: "header" wenzelm@21732: "help" wenzelm@49571: "locale_deps" blanchet@33198: "nitpick" wenzelm@11538: "pr" wenzelm@11538: "pretty_setmargin" wenzelm@11538: "prf" wenzelm@21732: "print_abbrevs" wenzelm@11538: "print_antiquotations" wenzelm@11538: "print_attributes" wenzelm@11538: "print_binds" blanchet@48981: "print_bnfs" wenzelm@47057: "print_bundles" wenzelm@11538: "print_cases" wenzelm@11538: "print_claset" haftmann@20378: "print_classes" haftmann@31130: "print_codeproc" haftmann@22288: "print_codesetup" berghofe@45061: "print_coercion_maps" berghofe@45061: "print_coercions" wenzelm@11538: "print_commands" wenzelm@24120: "print_configs" wenzelm@11538: "print_context" ballarin@41435: "print_dependencies" wenzelm@14938: "print_drafts" wenzelm@11538: "print_facts" wenzelm@11661: "print_induct_rules" ballarin@32804: "print_interps" wenzelm@12059: "print_locale" wenzelm@12059: "print_locales" wenzelm@11538: "print_methods" ballarin@24642: "print_orders" kaliszyk@35279: "print_quotconsts" kaliszyk@35279: "print_quotients" kuncar@47308: "print_quotientsQ3" kaliszyk@35279: "print_quotmaps" kuncar@47308: "print_quotmapsQ3" wenzelm@12365: "print_rules" wenzelm@11538: "print_simpset" wenzelm@19272: "print_statement" wenzelm@11538: "print_syntax" wenzelm@11538: "print_theorems" wenzelm@11538: "print_theory" wenzelm@11538: "print_trans_rules" wenzelm@11538: "prop" wenzelm@11538: "pwd" berghofe@14109: "quickcheck" webertj@14349: "refute" wenzelm@22864: "sledgehammer" wenzelm@33898: "smt_status" blanchet@40117: "solve_direct" berghofe@41564: "spark_status" wenzelm@11538: "term" wenzelm@11538: "thm" wenzelm@11538: "thm_deps" haftmann@22486: "thy_deps" blanchet@38943: "try" blanchet@46641: "try0" wenzelm@11538: "typ" berghofe@26184: "unused_thms" berghofe@17552: "value" haftmann@31130: "values" wenzelm@11538: "welcome")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-begin wenzelm@11538: '("theory")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-switch wenzelm@21302: '()) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-end wenzelm@11538: '("end")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-heading wenzelm@11538: '("chapter" wenzelm@11538: "section" wenzelm@11538: "subsection" wenzelm@11538: "subsubsection")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-decl wenzelm@26482: '("ML" wenzelm@48867: "ML_file" wenzelm@19069: "abbreviation" wenzelm@11538: "arities" wenzelm@24904: "atom_decl" wenzelm@30527: "attribute_setup" wenzelm@18612: "axiomatization" wenzelm@11538: "axioms" wenzelm@33687: "boogie_end" wenzelm@33687: "boogie_open" wenzelm@47057: "bundle" haftmann@18552: "class" wenzelm@11538: "classes" wenzelm@11538: "classrel" blanchet@49112: "codata" haftmann@27102: "code_abort" haftmann@20424: "code_class" haftmann@20453: "code_const" haftmann@22486: "code_datatype" haftmann@24997: "code_include" haftmann@20424: "code_instance" wenzelm@21203: "code_modulename" wenzelm@22084: "code_monad" haftmann@36472: "code_reflect" wenzelm@21028: "code_reserved" haftmann@20453: "code_type" wenzelm@11538: "coinductive" berghofe@23732: "coinductive_set" wenzelm@11538: "consts" wenzelm@21302: "context" blanchet@49112: "data" wenzelm@11538: "datatype" wenzelm@22084: "declaration" wenzelm@23804: "declare" wenzelm@36455: "default_sort" wenzelm@11538: "defer_recdef" wenzelm@18775: "definition" wenzelm@11538: "defs" wenzelm@12040: "domain" wenzelm@33840: "domain_isomorphism" haftmann@40585: "domaindef" wenzelm@24904: "equivariance" berghofe@13407: "extract" berghofe@13407: "extract_type" huffman@16231: "fixrec" krauss@20523: "fun" wenzelm@36180: "hide_class" wenzelm@36180: "hide_const" wenzelm@36180: "hide_fact" wenzelm@36180: "hide_type" wenzelm@47262: "import_const_map" wenzelm@47262: "import_file" wenzelm@46951: "import_tptp" wenzelm@47262: "import_type_map" wenzelm@11538: "inductive" berghofe@23732: "inductive_set" haftmann@24437: "instantiation" wenzelm@11538: "judgment" wenzelm@11538: "lemmas" wenzelm@30463: "local_setup" wenzelm@12059: "locale" wenzelm@11538: "method_setup" blanchet@33198: "nitpick_params" wenzelm@24945: "no_notation" wenzelm@15703: "no_syntax" wenzelm@19255: "no_translations" wenzelm@35414: "no_type_notation" wenzelm@24904: "nominal_datatype" wenzelm@41229: "nonterminal" wenzelm@21203: "notation" wenzelm@40960: "notepad" wenzelm@11538: "oracle" haftmann@25516: "overloading" wenzelm@11538: "parse_ast_translation" wenzelm@11538: "parse_translation" krauss@40209: "partial_function" wenzelm@11538: "primrec" wenzelm@11538: "print_ast_translation" wenzelm@11538: "print_translation" bulwahn@45926: "quickcheck_generator" berghofe@14109: "quickcheck_params" berghofe@13407: "realizability" berghofe@13407: "realizers" wenzelm@11538: "recdef" wenzelm@11538: "record" webertj@14349: "refute_params" wenzelm@11538: "setup" kuncar@47098: "setup_lifting" wenzelm@22200: "simproc_setup" haftmann@36114: "sledgehammer_params" berghofe@41564: "spark_end" berghofe@41564: "spark_open" wenzelm@48908: "spark_open_siv" wenzelm@48908: "spark_open_vcg" berghofe@41564: "spark_proof_functions" berghofe@42356: "spark_types" wenzelm@25176: "statespace" wenzelm@11538: "syntax" wenzelm@40784: "syntax_declaration" wenzelm@11538: "text" wenzelm@11538: "text_raw" wenzelm@11538: "theorems" wenzelm@11538: "translations" wenzelm@35414: "type_notation" wenzelm@41249: "type_synonym" wenzelm@11538: "typed_print_translation" wenzelm@11538: "typedecl" wenzelm@26482: "use")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-script bulwahn@37734: '("inductive_cases" bulwahn@37734: "inductive_simps")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-theory-goal skalberg@14223: '("ax_specification" blanchet@48981: "bnf_def" wenzelm@33687: "boogie_vc" bulwahn@31106: "code_pred" skalberg@14223: "corollary" huffman@16701: "cpodef" wenzelm@41530: "enriched_type" krauss@19564: "function" wenzelm@11746: "instance" ballarin@15598: "interpretation" wenzelm@11538: "lemma" huffman@47354: "lift_definition" wenzelm@24904: "nominal_inductive" berghofe@28656: "nominal_inductive2" wenzelm@24904: "nominal_primrec" huffman@16701: "pcpodef" kuncar@47098: "quotient_definition" kaliszyk@35279: "quotient_type" wenzelm@11538: "recdef_tc" haftmann@27102: "rep_datatype" wenzelm@36321: "schematic_corollary" wenzelm@36321: "schematic_lemma" wenzelm@36321: "schematic_theorem" berghofe@41564: "spark_vc" skalberg@14115: "specification" haftmann@24919: "subclass" ballarin@28895: "sublocale" krauss@19564: "termination" wenzelm@11538: "theorem" blanchet@49074: "typedef" blanchet@49074: "wrap_data")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-qed wenzelm@11538: '("\\." wenzelm@11538: "\\.\\." wenzelm@11538: "by" wenzelm@11538: "done" wenzelm@11538: "sorry")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-qed-block wenzelm@11538: '("qed")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-qed-global wenzelm@11538: '("oops")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-heading wenzelm@11538: '("sect" wenzelm@11538: "subsect" wenzelm@11538: "subsubsect")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-goal wenzelm@29607: '("have" wenzelm@11538: "hence" wenzelm@29607: "interpret")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-block wenzelm@11538: '("next" wenzelm@11538: "proof")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-open wenzelm@11538: '("{")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-close wenzelm@11538: '("}")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-chain wenzelm@11538: '("finally" wenzelm@11538: "from" wenzelm@11538: "then" wenzelm@11538: "ultimately" wenzelm@11538: "with")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-decl wenzelm@28280: '("ML_prf" wenzelm@28280: "also" wenzelm@47057: "include" wenzelm@47057: "including" wenzelm@11538: "let" wenzelm@11538: "moreover" wenzelm@11538: "note" wenzelm@11538: "txt" wenzelm@12926: "txt_raw" wenzelm@18541: "unfolding" wenzelm@36505: "using" wenzelm@36505: "write")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-asm wenzelm@11538: '("assume" wenzelm@11538: "case" wenzelm@11538: "def" wenzelm@11538: "fix" wenzelm@11538: "presume")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-asm-goal wenzelm@17850: '("guess" wenzelm@21806: "obtain" wenzelm@21806: "show" wenzelm@21806: "thus")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-proof-script wenzelm@11538: '("apply" wenzelm@11538: "apply_end" wenzelm@11538: "back" wenzelm@11538: "defer" wenzelm@11538: "prefer")) wenzelm@11538: wenzelm@11538: (provide 'isar-keywords)