--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/isar-keywords-quot.el Mon Jul 26 09:19:28 2010 +0200
@@ -0,0 +1,616 @@
+;;
+;; Keyword classification tables for Isabelle/Isar.
+;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure.
+;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
+;;
+
+(defconst isar-keywords-major
+ '("\\."
+ "\\.\\."
+ "Isabelle\\.command"
+ "Isar\\.begin_document"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
+ "ML"
+ "ML_command"
+ "ML_prf"
+ "ML_val"
+ "ProofGeneral\\.inform_file_processed"
+ "ProofGeneral\\.inform_file_retracted"
+ "ProofGeneral\\.kill_proof"
+ "ProofGeneral\\.pr"
+ "ProofGeneral\\.process_pgip"
+ "ProofGeneral\\.restart"
+ "ProofGeneral\\.undo"
+ "abbreviation"
+ "also"
+ "apply"
+ "apply_end"
+ "arities"
+ "assume"
+ "atom_decl"
+ "atp_info"
+ "atp_kill"
+ "atp_messages"
+ "atp_minimize"
+ "attribute_setup"
+ "ax_specification"
+ "axclass"
+ "axiomatization"
+ "axioms"
+ "back"
+ "by"
+ "cannot_undo"
+ "case"
+ "cd"
+ "chapter"
+ "class"
+ "class_deps"
+ "classes"
+ "classrel"
+ "code_abort"
+ "code_class"
+ "code_const"
+ "code_datatype"
+ "code_deps"
+ "code_include"
+ "code_instance"
+ "code_library"
+ "code_module"
+ "code_modulename"
+ "code_monad"
+ "code_pred"
+ "code_reflect"
+ "code_reserved"
+ "code_thms"
+ "code_type"
+ "coinductive"
+ "coinductive_set"
+ "commit"
+ "constdefs"
+ "consts"
+ "consts_code"
+ "context"
+ "corollary"
+ "datatype"
+ "declaration"
+ "declare"
+ "def"
+ "default_sort"
+ "defer"
+ "defer_recdef"
+ "definition"
+ "defs"
+ "disable_pr"
+ "display_drafts"
+ "done"
+ "enable_pr"
+ "end"
+ "equivariance"
+ "exit"
+ "export_code"
+ "extract"
+ "extract_type"
+ "finalconsts"
+ "finally"
+ "find_consts"
+ "find_theorems"
+ "fix"
+ "from"
+ "full_prf"
+ "fun"
+ "function"
+ "global"
+ "guess"
+ "have"
+ "header"
+ "help"
+ "hence"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
+ "inductive"
+ "inductive_cases"
+ "inductive_set"
+ "init_toplevel"
+ "instance"
+ "instantiation"
+ "interpret"
+ "interpretation"
+ "judgment"
+ "kill"
+ "kill_thy"
+ "lemma"
+ "lemmas"
+ "let"
+ "linear_undo"
+ "local"
+ "local_setup"
+ "locale"
+ "method_setup"
+ "moreover"
+ "next"
+ "nitpick"
+ "nitpick_params"
+ "no_notation"
+ "no_syntax"
+ "no_translations"
+ "nominal_datatype"
+ "nominal_inductive"
+ "nominal_inductive2"
+ "nominal_primrec"
+ "nonterminals"
+ "normal_form"
+ "notation"
+ "note"
+ "obtain"
+ "oops"
+ "oracle"
+ "overloading"
+ "parse_ast_translation"
+ "parse_translation"
+ "pr"
+ "prefer"
+ "presume"
+ "pretty_setmargin"
+ "prf"
+ "primrec"
+ "print_abbrevs"
+ "print_antiquotations"
+ "print_ast_translation"
+ "print_atps"
+ "print_attributes"
+ "print_binds"
+ "print_cases"
+ "print_claset"
+ "print_classes"
+ "print_codeproc"
+ "print_codesetup"
+ "print_commands"
+ "print_configs"
+ "print_context"
+ "print_drafts"
+ "print_facts"
+ "print_induct_rules"
+ "print_interps"
+ "print_locale"
+ "print_locales"
+ "print_maps"
+ "print_methods"
+ "print_orders"
+ "print_quotconsts"
+ "print_quotients"
+ "print_rules"
+ "print_simpset"
+ "print_statement"
+ "print_syntax"
+ "print_theorems"
+ "print_theory"
+ "print_trans_rules"
+ "print_translation"
+ "proof"
+ "prop"
+ "prove"
+ "pwd"
+ "qed"
+ "quickcheck"
+ "quickcheck_params"
+ "quit"
+ "quotient_definition"
+ "quotient_type"
+ "realizability"
+ "realizers"
+ "recdef"
+ "recdef_tc"
+ "record"
+ "refute"
+ "refute_params"
+ "remove_thy"
+ "rep_datatype"
+ "repdef"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
+ "sect"
+ "section"
+ "setup"
+ "show"
+ "simproc_setup"
+ "sledgehammer"
+ "sledgehammer_params"
+ "smt_status"
+ "sorry"
+ "specification"
+ "subclass"
+ "sublocale"
+ "subsect"
+ "subsection"
+ "subsubsect"
+ "subsubsection"
+ "syntax"
+ "term"
+ "termination"
+ "text"
+ "text_raw"
+ "then"
+ "theorem"
+ "theorems"
+ "theory"
+ "thm"
+ "thm_deps"
+ "thus"
+ "thy_deps"
+ "touch_thy"
+ "translations"
+ "txt"
+ "txt_raw"
+ "typ"
+ "typed_print_translation"
+ "typedecl"
+ "typedef"
+ "types"
+ "types_code"
+ "ultimately"
+ "undo"
+ "undos_proof"
+ "unfolding"
+ "unused_thms"
+ "use"
+ "use_thy"
+ "using"
+ "value"
+ "values"
+ "welcome"
+ "with"
+ "{"
+ "}"))
+
+(defconst isar-keywords-minor
+ '("advanced"
+ "and"
+ "as"
+ "assumes"
+ "attach"
+ "avoids"
+ "begin"
+ "binder"
+ "congs"
+ "constrains"
+ "contains"
+ "defines"
+ "file"
+ "fixes"
+ "for"
+ "hints"
+ "identifier"
+ "if"
+ "imports"
+ "in"
+ "infix"
+ "infixl"
+ "infixr"
+ "is"
+ "module_name"
+ "monos"
+ "morphisms"
+ "notes"
+ "obtains"
+ "open"
+ "output"
+ "overloaded"
+ "permissive"
+ "pervasive"
+ "shows"
+ "structure"
+ "unchecked"
+ "uses"
+ "where"))
+
+(defconst isar-keywords-control
+ '("Isabelle\\.command"
+ "Isar\\.begin_document"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
+ "ProofGeneral\\.inform_file_processed"
+ "ProofGeneral\\.inform_file_retracted"
+ "ProofGeneral\\.kill_proof"
+ "ProofGeneral\\.process_pgip"
+ "ProofGeneral\\.restart"
+ "ProofGeneral\\.undo"
+ "cannot_undo"
+ "exit"
+ "init_toplevel"
+ "kill"
+ "linear_undo"
+ "quit"
+ "undo"
+ "undos_proof"))
+
+(defconst isar-keywords-diag
+ '("ML_command"
+ "ML_val"
+ "ProofGeneral\\.pr"
+ "atp_info"
+ "atp_kill"
+ "atp_messages"
+ "atp_minimize"
+ "cd"
+ "class_deps"
+ "code_deps"
+ "code_thms"
+ "commit"
+ "disable_pr"
+ "display_drafts"
+ "enable_pr"
+ "export_code"
+ "find_consts"
+ "find_theorems"
+ "full_prf"
+ "header"
+ "help"
+ "kill_thy"
+ "nitpick"
+ "normal_form"
+ "pr"
+ "pretty_setmargin"
+ "prf"
+ "print_abbrevs"
+ "print_antiquotations"
+ "print_atps"
+ "print_attributes"
+ "print_binds"
+ "print_cases"
+ "print_claset"
+ "print_classes"
+ "print_codeproc"
+ "print_codesetup"
+ "print_commands"
+ "print_configs"
+ "print_context"
+ "print_drafts"
+ "print_facts"
+ "print_induct_rules"
+ "print_interps"
+ "print_locale"
+ "print_locales"
+ "print_maps"
+ "print_methods"
+ "print_orders"
+ "print_quotconsts"
+ "print_quotients"
+ "print_rules"
+ "print_simpset"
+ "print_statement"
+ "print_syntax"
+ "print_theorems"
+ "print_theory"
+ "print_trans_rules"
+ "prop"
+ "pwd"
+ "quickcheck"
+ "refute"
+ "remove_thy"
+ "sledgehammer"
+ "term"
+ "thm"
+ "thm_deps"
+ "thy_deps"
+ "touch_thy"
+ "typ"
+ "unused_thms"
+ "use_thy"
+ "value"
+ "values"
+ "welcome"))
+
+(defconst isar-keywords-theory-begin
+ '("theory"))
+
+(defconst isar-keywords-theory-switch
+ '())
+
+(defconst isar-keywords-theory-end
+ '("end"))
+
+(defconst isar-keywords-theory-heading
+ '("chapter"
+ "section"
+ "subsection"
+ "subsubsection"))
+
+(defconst isar-keywords-theory-decl
+ '("ML"
+ "abbreviation"
+ "arities"
+ "atom_decl"
+ "attribute_setup"
+ "axclass"
+ "axiomatization"
+ "axioms"
+ "class"
+ "classes"
+ "classrel"
+ "code_abort"
+ "code_class"
+ "code_const"
+ "code_datatype"
+ "code_include"
+ "code_instance"
+ "code_library"
+ "code_module"
+ "code_modulename"
+ "code_monad"
+ "code_reflect"
+ "code_reserved"
+ "code_type"
+ "coinductive"
+ "coinductive_set"
+ "constdefs"
+ "consts"
+ "consts_code"
+ "context"
+ "datatype"
+ "declaration"
+ "declare"
+ "defaultsort"
+ "defer_recdef"
+ "definition"
+ "defs"
+ "equivariance"
+ "extract"
+ "extract_type"
+ "finalconsts"
+ "fun"
+ "global"
+ "hide_class"
+ "hide_const"
+ "hide_fact"
+ "hide_type"
+ "inductive"
+ "inductive_set"
+ "instantiation"
+ "judgment"
+ "lemmas"
+ "local"
+ "local_setup"
+ "locale"
+ "method_setup"
+ "nitpick_params"
+ "no_notation"
+ "no_syntax"
+ "no_translations"
+ "nominal_datatype"
+ "nonterminals"
+ "notation"
+ "oracle"
+ "overloading"
+ "parse_ast_translation"
+ "parse_translation"
+ "primrec"
+ "print_ast_translation"
+ "print_translation"
+ "quickcheck_params"
+ "quotient_definition"
+ "realizability"
+ "realizers"
+ "recdef"
+ "record"
+ "refute_params"
+ "setup"
+ "simproc_setup"
+ "sledgehammer_params"
+ "statespace"
+ "syntax"
+ "text"
+ "text_raw"
+ "theorems"
+ "translations"
+ "typed_print_translation"
+ "typedecl"
+ "types"
+ "types_code"
+ "use"))
+
+(defconst isar-keywords-theory-script
+ '("inductive_cases"))
+
+(defconst isar-keywords-theory-goal
+ '("ax_specification"
+ "code_pred"
+ "corollary"
+ "function"
+ "instance"
+ "interpretation"
+ "lemma"
+ "nominal_inductive"
+ "nominal_inductive2"
+ "nominal_primrec"
+ "prove"
+ "quotient_type"
+ "recdef_tc"
+ "rep_datatype"
+ "schematic_corollary"
+ "schematic_lemma"
+ "schematic_theorem"
+ "specification"
+ "subclass"
+ "sublocale"
+ "termination"
+ "theorem"
+ "typedef"))
+
+(defconst isar-keywords-qed
+ '("\\."
+ "\\.\\."
+ "by"
+ "done"
+ "sorry"))
+
+(defconst isar-keywords-qed-block
+ '("qed"))
+
+(defconst isar-keywords-qed-global
+ '("oops"))
+
+(defconst isar-keywords-proof-heading
+ '("sect"
+ "subsect"
+ "subsubsect"))
+
+(defconst isar-keywords-proof-goal
+ '("have"
+ "hence"
+ "interpret"))
+
+(defconst isar-keywords-proof-block
+ '("next"
+ "proof"))
+
+(defconst isar-keywords-proof-open
+ '("{"))
+
+(defconst isar-keywords-proof-close
+ '("}"))
+
+(defconst isar-keywords-proof-chain
+ '("finally"
+ "from"
+ "then"
+ "ultimately"
+ "with"))
+
+(defconst isar-keywords-proof-decl
+ '("ML_prf"
+ "also"
+ "let"
+ "moreover"
+ "note"
+ "txt"
+ "txt_raw"
+ "unfolding"
+ "using"))
+
+(defconst isar-keywords-proof-asm
+ '("assume"
+ "case"
+ "def"
+ "fix"
+ "presume"))
+
+(defconst isar-keywords-proof-asm-goal
+ '("guess"
+ "obtain"
+ "show"
+ "thus"))
+
+(defconst isar-keywords-proof-script
+ '("apply"
+ "apply_end"
+ "back"
+ "defer"
+ "prefer"))
+
+(provide 'isar-keywords)
--- a/TODO Sun Jul 25 22:42:21 2010 +0200
+++ b/TODO Mon Jul 26 09:19:28 2010 +0200
@@ -35,30 +35,6 @@
- Parser adds syntax for raw datatype, but should
add for lifted datatype.
-- the alpha equivalence for
-
- Let as::assn t::trm bind "bn as" in t
-
- creates as premise
-
- EX pi. as ~~bn as' /\ (bn as, t) ~~lst (bn as', t')
-
- but I think it should be
-
- as ~~bn as' /\ EX pi. (bn as, t) ~~lst (bn as', t')
-
- (both are equivalent, but the second seems to be closer to
- the fv-function)
-
-- when there are more than one shallow binder, then alpha
- equivalence creates more than one permutation. According
- to the paper, this is incorrect.
-
- Example in Classical.thy.
-
-- check whether weirdo example in TestMorePerm works
- with shallow binders
-
- nested recursion, like types "trm list" in a constructor
- define permute_bn automatically and prove properties of it
--- a/isar-keywords-quot.el Sun Jul 25 22:42:21 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,616 +0,0 @@
-;;
-;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure.
-;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
-;;
-
-(defconst isar-keywords-major
- '("\\."
- "\\.\\."
- "Isabelle\\.command"
- "Isar\\.begin_document"
- "Isar\\.define_command"
- "Isar\\.edit_document"
- "Isar\\.end_document"
- "ML"
- "ML_command"
- "ML_prf"
- "ML_val"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.pr"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "abbreviation"
- "also"
- "apply"
- "apply_end"
- "arities"
- "assume"
- "atom_decl"
- "atp_info"
- "atp_kill"
- "atp_messages"
- "atp_minimize"
- "attribute_setup"
- "ax_specification"
- "axclass"
- "axiomatization"
- "axioms"
- "back"
- "by"
- "cannot_undo"
- "case"
- "cd"
- "chapter"
- "class"
- "class_deps"
- "classes"
- "classrel"
- "code_abort"
- "code_class"
- "code_const"
- "code_datatype"
- "code_deps"
- "code_include"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_monad"
- "code_pred"
- "code_reflect"
- "code_reserved"
- "code_thms"
- "code_type"
- "coinductive"
- "coinductive_set"
- "commit"
- "constdefs"
- "consts"
- "consts_code"
- "context"
- "corollary"
- "datatype"
- "declaration"
- "declare"
- "def"
- "default_sort"
- "defer"
- "defer_recdef"
- "definition"
- "defs"
- "disable_pr"
- "display_drafts"
- "done"
- "enable_pr"
- "end"
- "equivariance"
- "exit"
- "export_code"
- "extract"
- "extract_type"
- "finalconsts"
- "finally"
- "find_consts"
- "find_theorems"
- "fix"
- "from"
- "full_prf"
- "fun"
- "function"
- "global"
- "guess"
- "have"
- "header"
- "help"
- "hence"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "inductive"
- "inductive_cases"
- "inductive_set"
- "init_toplevel"
- "instance"
- "instantiation"
- "interpret"
- "interpretation"
- "judgment"
- "kill"
- "kill_thy"
- "lemma"
- "lemmas"
- "let"
- "linear_undo"
- "local"
- "local_setup"
- "locale"
- "method_setup"
- "moreover"
- "next"
- "nitpick"
- "nitpick_params"
- "no_notation"
- "no_syntax"
- "no_translations"
- "nominal_datatype"
- "nominal_inductive"
- "nominal_inductive2"
- "nominal_primrec"
- "nonterminals"
- "normal_form"
- "notation"
- "note"
- "obtain"
- "oops"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "pr"
- "prefer"
- "presume"
- "pretty_setmargin"
- "prf"
- "primrec"
- "print_abbrevs"
- "print_antiquotations"
- "print_ast_translation"
- "print_atps"
- "print_attributes"
- "print_binds"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codeproc"
- "print_codesetup"
- "print_commands"
- "print_configs"
- "print_context"
- "print_drafts"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_maps"
- "print_methods"
- "print_orders"
- "print_quotconsts"
- "print_quotients"
- "print_rules"
- "print_simpset"
- "print_statement"
- "print_syntax"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "print_translation"
- "proof"
- "prop"
- "prove"
- "pwd"
- "qed"
- "quickcheck"
- "quickcheck_params"
- "quit"
- "quotient_definition"
- "quotient_type"
- "realizability"
- "realizers"
- "recdef"
- "recdef_tc"
- "record"
- "refute"
- "refute_params"
- "remove_thy"
- "rep_datatype"
- "repdef"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "sect"
- "section"
- "setup"
- "show"
- "simproc_setup"
- "sledgehammer"
- "sledgehammer_params"
- "smt_status"
- "sorry"
- "specification"
- "subclass"
- "sublocale"
- "subsect"
- "subsection"
- "subsubsect"
- "subsubsection"
- "syntax"
- "term"
- "termination"
- "text"
- "text_raw"
- "then"
- "theorem"
- "theorems"
- "theory"
- "thm"
- "thm_deps"
- "thus"
- "thy_deps"
- "touch_thy"
- "translations"
- "txt"
- "txt_raw"
- "typ"
- "typed_print_translation"
- "typedecl"
- "typedef"
- "types"
- "types_code"
- "ultimately"
- "undo"
- "undos_proof"
- "unfolding"
- "unused_thms"
- "use"
- "use_thy"
- "using"
- "value"
- "values"
- "welcome"
- "with"
- "{"
- "}"))
-
-(defconst isar-keywords-minor
- '("advanced"
- "and"
- "as"
- "assumes"
- "attach"
- "avoids"
- "begin"
- "binder"
- "congs"
- "constrains"
- "contains"
- "defines"
- "file"
- "fixes"
- "for"
- "hints"
- "identifier"
- "if"
- "imports"
- "in"
- "infix"
- "infixl"
- "infixr"
- "is"
- "module_name"
- "monos"
- "morphisms"
- "notes"
- "obtains"
- "open"
- "output"
- "overloaded"
- "permissive"
- "pervasive"
- "shows"
- "structure"
- "unchecked"
- "uses"
- "where"))
-
-(defconst isar-keywords-control
- '("Isabelle\\.command"
- "Isar\\.begin_document"
- "Isar\\.define_command"
- "Isar\\.edit_document"
- "Isar\\.end_document"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "cannot_undo"
- "exit"
- "init_toplevel"
- "kill"
- "linear_undo"
- "quit"
- "undo"
- "undos_proof"))
-
-(defconst isar-keywords-diag
- '("ML_command"
- "ML_val"
- "ProofGeneral\\.pr"
- "atp_info"
- "atp_kill"
- "atp_messages"
- "atp_minimize"
- "cd"
- "class_deps"
- "code_deps"
- "code_thms"
- "commit"
- "disable_pr"
- "display_drafts"
- "enable_pr"
- "export_code"
- "find_consts"
- "find_theorems"
- "full_prf"
- "header"
- "help"
- "kill_thy"
- "nitpick"
- "normal_form"
- "pr"
- "pretty_setmargin"
- "prf"
- "print_abbrevs"
- "print_antiquotations"
- "print_atps"
- "print_attributes"
- "print_binds"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codeproc"
- "print_codesetup"
- "print_commands"
- "print_configs"
- "print_context"
- "print_drafts"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_maps"
- "print_methods"
- "print_orders"
- "print_quotconsts"
- "print_quotients"
- "print_rules"
- "print_simpset"
- "print_statement"
- "print_syntax"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "prop"
- "pwd"
- "quickcheck"
- "refute"
- "remove_thy"
- "sledgehammer"
- "term"
- "thm"
- "thm_deps"
- "thy_deps"
- "touch_thy"
- "typ"
- "unused_thms"
- "use_thy"
- "value"
- "values"
- "welcome"))
-
-(defconst isar-keywords-theory-begin
- '("theory"))
-
-(defconst isar-keywords-theory-switch
- '())
-
-(defconst isar-keywords-theory-end
- '("end"))
-
-(defconst isar-keywords-theory-heading
- '("chapter"
- "section"
- "subsection"
- "subsubsection"))
-
-(defconst isar-keywords-theory-decl
- '("ML"
- "abbreviation"
- "arities"
- "atom_decl"
- "attribute_setup"
- "axclass"
- "axiomatization"
- "axioms"
- "class"
- "classes"
- "classrel"
- "code_abort"
- "code_class"
- "code_const"
- "code_datatype"
- "code_include"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_monad"
- "code_reflect"
- "code_reserved"
- "code_type"
- "coinductive"
- "coinductive_set"
- "constdefs"
- "consts"
- "consts_code"
- "context"
- "datatype"
- "declaration"
- "declare"
- "defaultsort"
- "defer_recdef"
- "definition"
- "defs"
- "equivariance"
- "extract"
- "extract_type"
- "finalconsts"
- "fun"
- "global"
- "hide_class"
- "hide_const"
- "hide_fact"
- "hide_type"
- "inductive"
- "inductive_set"
- "instantiation"
- "judgment"
- "lemmas"
- "local"
- "local_setup"
- "locale"
- "method_setup"
- "nitpick_params"
- "no_notation"
- "no_syntax"
- "no_translations"
- "nominal_datatype"
- "nonterminals"
- "notation"
- "oracle"
- "overloading"
- "parse_ast_translation"
- "parse_translation"
- "primrec"
- "print_ast_translation"
- "print_translation"
- "quickcheck_params"
- "quotient_definition"
- "realizability"
- "realizers"
- "recdef"
- "record"
- "refute_params"
- "setup"
- "simproc_setup"
- "sledgehammer_params"
- "statespace"
- "syntax"
- "text"
- "text_raw"
- "theorems"
- "translations"
- "typed_print_translation"
- "typedecl"
- "types"
- "types_code"
- "use"))
-
-(defconst isar-keywords-theory-script
- '("inductive_cases"))
-
-(defconst isar-keywords-theory-goal
- '("ax_specification"
- "code_pred"
- "corollary"
- "function"
- "instance"
- "interpretation"
- "lemma"
- "nominal_inductive"
- "nominal_inductive2"
- "nominal_primrec"
- "prove"
- "quotient_type"
- "recdef_tc"
- "rep_datatype"
- "schematic_corollary"
- "schematic_lemma"
- "schematic_theorem"
- "specification"
- "subclass"
- "sublocale"
- "termination"
- "theorem"
- "typedef"))
-
-(defconst isar-keywords-qed
- '("\\."
- "\\.\\."
- "by"
- "done"
- "sorry"))
-
-(defconst isar-keywords-qed-block
- '("qed"))
-
-(defconst isar-keywords-qed-global
- '("oops"))
-
-(defconst isar-keywords-proof-heading
- '("sect"
- "subsect"
- "subsubsect"))
-
-(defconst isar-keywords-proof-goal
- '("have"
- "hence"
- "interpret"))
-
-(defconst isar-keywords-proof-block
- '("next"
- "proof"))
-
-(defconst isar-keywords-proof-open
- '("{"))
-
-(defconst isar-keywords-proof-close
- '("}"))
-
-(defconst isar-keywords-proof-chain
- '("finally"
- "from"
- "then"
- "ultimately"
- "with"))
-
-(defconst isar-keywords-proof-decl
- '("ML_prf"
- "also"
- "let"
- "moreover"
- "note"
- "txt"
- "txt_raw"
- "unfolding"
- "using"))
-
-(defconst isar-keywords-proof-asm
- '("assume"
- "case"
- "def"
- "fix"
- "presume"))
-
-(defconst isar-keywords-proof-asm-goal
- '("guess"
- "obtain"
- "show"
- "thus"))
-
-(defconst isar-keywords-proof-script
- '("apply"
- "apply_end"
- "back"
- "defer"
- "prefer"))
-
-(provide 'isar-keywords)