{
  "name": "Isabelle Theory",
  "scopeName": "source.isabelle.theory",
  "patterns": [
    {
      "name": "comment.block.documentation",
      "begin": "\\{\\*",
      "end": "\\*\\}"
    },
    {
      "name": "comment.block.documentation",
      "begin": "\\\\\\\u003copen\\\u003e",
      "end": "\\\\\\\u003cclose\\\u003e"
    },
    {
      "name": "comment.block",
      "begin": "\\(\\*",
      "end": "\\*\\)"
    },
    {
      "name": "comment.line",
      "match": "--([ ]*\"[^\"]+\")?"
    },
    {
      "match": "\\b(theory)[ ]+([a-zA-Z0-9_]+)",
      "captures": {
        "1": {
          "name": "keyword.other.isabelle.theory"
        },
        "2": {
          "name": "storage"
        }
      }
    },
    {
      "name": "markup.heading",
      "match": "\\b(header|chapter|section|subsection|subsubsection|sect|subsect|subsubsect)\\b"
    },
    {
      "name": "keyword.other.minor",
      "match": "\\b(and|assumes|attach|avoids|binder|checking|class_instance|class_relation|code_module|congs|constant|constrains|datatypes|defines|file|fixes|for|functions|hints|identifier|if|imports|in|includes|infix|infixl|infixr|is|keywords|lazy|module_name|monos|morphisms|no_discs_sels|notes|obtains|open|output|overloaded|parametric|permissive|pervasive|rep_compat|shows|structure|type_class|type_constructor|unchecked|unsafe|where|begin|end)\\b"
    },
    {
      "name": "keyword.other.diagnostic",
      "match": "\\b(ML_command|ML_val|class_deps|code_deps|code_thms|display_drafts|find_consts|find_theorems|find_unused_assms|full_prf|help|locale_deps|nitpick|pr|prf|print_abbrevs|print_antiquotations|print_attributes|print_binds|print_bnfs|print_bundles|print_case_translations|print_cases|print_claset|print_classes|print_codeproc|print_codesetup|print_coercions|print_commands|print_context|print_defn_rules|print_dependencies|print_facts|print_induct_rules|print_inductives|print_interps|print_locale|print_locales|print_methods|print_options|print_orders|print_quot_maps|print_quotconsts|print_quotients|print_quotientsQ3|print_quotmapsQ3|print_rules|print_simpset|print_state|print_statement|print_syntax|print_theorems|print_theory|print_trans_rules|prop|pwd|quickcheck|refute|sledgehammer|smt_status|solve_direct|spark_status|term|thm|thm_deps|thy_deps|try|try0|typ|unused_thms|value|values|welcome|print_ML_antiquotations|print_term_bindings|values_prolog)\\b"
    },
    {
      "name": "keyword.other.declaration",
      "match": "\\b(ML|ML_file|abbreviation|adhoc_overloading|arities|atom_decl|attribute_setup|axiomatization|bundle|case_of_simps|class|classes|classrel|codatatype|code_abort|code_class|code_const|code_datatype|code_identifier|code_include|code_instance|code_modulename|code_monad|code_printing|code_reflect|code_reserved|code_type|coinductive|coinductive_set|consts|context|datatype|datatype_new|datatype_new_compat|declaration|declare|default_sort|defer_recdef|definition|defs|domain|domain_isomorphism|domaindef|equivariance|export_code|extract|extract_type|fixrec|fun|fun_cases|hide_class|hide_const|hide_fact|hide_type|import_const_map|import_file|import_tptp|import_type_map|inductive|inductive_set|instantiation|judgment|lifting_forget|lifting_update|local_setup|locale|method_setup|nitpick_params|no_adhoc_overloading|no_notation|no_syntax|no_translations|no_type_notation|nominal_datatype|nonterminal|notation|notepad|oracle|overloading|parse_ast_translation|parse_translation|partial_function|primcorec|primrec|primrec_new|print_ast_translation|print_translation|quickcheck_generator|quickcheck_params|realizability|realizers|recdef|record|refute_params|setup|setup_lifting|simproc_setup|simps_of_case|sledgehammer_params|spark_end|spark_open|spark_open_siv|spark_open_vcg|spark_proof_functions|spark_types|statespace|syntax|syntax_declaration|text|text_raw|txt|txt_raw|theorems|translations|type_notation|type_synonym|typed_print_translation|typedecl|hoarestate|install_C_file|install_C_types|wpc_setup|c_defs|c_types|memsafe|SML_export|SML_file|SML_import|approximate|bnf_axiomatization|cartouche|datatype_compat|free_constructors|functor|nominal_function|nominal_termination|permanent_interpretation|binds|defining|smt2_status|term_cartouche|boogie_file|text_cartouche|autocorres|sep_instance)\\b"
    },
    {
      "name": "keyword.other.script",
      "match": "\\b(inductive_cases|inductive_simps|crunch)\\b"
    },
    {
      "name": "keyword.other.goal",
      "match": "\\b(ax_specification|bnf|code_pred|corollary|cpodef|crunch_ignore|enriched_type|function|instance|interpretation|lift_definition|nominal_inductive|nominal_inductive2|nominal_primrec|pcpodef|primcorecursive|quotient_definition|quotient_type|recdef_tc|rep_datatype|spark_vc|specification|subclass|sublocale|termination|theorem|typedef|wrap_free_constructors)\\b"
    },
    {
      "name": "keyword.control.proof",
      "match": "\\b(have|hence|interpret|next|proof|finally|from|then|ultimately|with|ML_prf|also|include|including|let|moreover|note|unfolding|using|write|ML_prf|also|include|including|let|moreover|note|txt|txt_raw|unfolding|using|write|assume|case|def|fix|presume|guess|obtain|show|thus|apply|apply_end|apply_trace|back|defer|prefer|and|by|done|qed)\\b"
    },
    {
      "name": "support.constant",
      "match": "\\b(lemma|schematic_lemma|theorem|schematic_theorem|corollary|schematic_corollary|lemmas)\\b"
    },
    {
      "name": "invalid.illegal.abandon-proof",
      "match": "\\b(sorry|oops)\\b"
    },
    {
      "name": "string",
      "begin": "\"",
      "end": "\""
    },
    {
      "name": "string",
      "begin": "`",
      "end": "`"
    },
    {
      "name": "variable.other",
      "match": "\\??'?([^\\W\\d]|\\\\\u003c\\w+\\\u003e)([.\\w\\']|\\\\\u003c\\w+\\\u003e)*"
    },
    {
      "name": "keyword.operator",
      "match": "::|:|\\(|\\)|\\[|\\]|_|\\=|\\,|\\+|\\-|\\!|\\?|\\|"
    },
    {
      "name": "keyword.operator.proof",
      "match": "\\.\\.|\\{|\\}|\\."
    },
    {
      "name": "punctuation.terminator.isabelle",
      "match": ";"
    },
    {
      "name": "constant.numeric",
      "match": "[0-9]+"
    }
  ]
}