isar-keywords-major;

1 files changed, 147 insertions, 0 deletions

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index dbb678e5..02026f7b 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -5,6 +5,153 @@
 ;; $Id$
 ;;
 
+(defconst isar-keywords-major
+  '("\\."
+    "\\.\\."
+    "ML"
+    "ML_command"
+    "ML_setup"
+    "ProofGeneral\\.context_thy_only"
+    "ProofGeneral\\.inform_file_processed"
+    "ProofGeneral\\.inform_file_retracted"
+    "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.restart"
+    "ProofGeneral\\.try_context_thy_only"
+    "ProofGeneral\\.undo"
+    "also"
+    "apply"
+    "apply_end"
+    "arities"
+    "assume"
+    "axclass"
+    "axioms"
+    "back"
+    "by"
+    "cannot_undo"
+    "case"
+    "cd"
+    "chapter"
+    "classes"
+    "classrel"
+    "clear_undos"
+    "coinductive"
+    "commit"
+    "constdefs"
+    "consts"
+    "context"
+    "datatype"
+    "def"
+    "defaultsort"
+    "defer"
+    "defer_recdef"
+    "defs"
+    "disable_pr"
+    "done"
+    "enable_pr"
+    "end"
+    "exit"
+    "finally"
+    "fix"
+    "from"
+    "global"
+    "have"
+    "header"
+    "help"
+    "hence"
+    "hide"
+    "inductive"
+    "inductive_cases"
+    "init_toplevel"
+    "instance"
+    "judgment"
+    "kill"
+    "kill_thy"
+    "lemma"
+    "lemmas"
+    "let"
+    "local"
+    "moreover"
+    "next"
+    "nonterminals"
+    "note"
+    "obtain"
+    "oops"
+    "oracle"
+    "parse_ast_translation"
+    "parse_translation"
+    "pr"
+    "prefer"
+    "presume"
+    "pretty_setmargin"
+    "primrec"
+    "print_ast_translation"
+    "print_attributes"
+    "print_binds"
+    "print_cases"
+    "print_claset"
+    "print_context"
+    "print_facts"
+    "print_methods"
+    "print_simpset"
+    "print_syntax"
+    "print_theorems"
+    "print_theory"
+    "print_translation"
+    "proof"
+    "prop"
+    "pwd"
+    "qed"
+    "quit"
+    "recdef"
+    "record"
+    "redo"
+    "remove_thy"
+    "rep_datatype"
+    "sect"
+    "section"
+    "setup"
+    "show"
+    "sorry"
+    "subsect"
+    "subsection"
+    "subsubsect"
+    "subsubsection"
+    "syntax"
+    "term"
+    "text"
+    "text_raw"
+    "then"
+    "theorem"
+    "theorems"
+    "theory"
+    "thm"
+    "thms_containing"
+    "thus"
+    "token_translation"
+    "touch_all_thys"
+    "touch_child_thys"
+    "touch_thy"
+    "translations"
+    "txt"
+    "txt_raw"
+    "typ"
+    "typed_print_translation"
+    "typedecl"
+    "typedef"
+    "types"
+    "ultimately"
+    "undo"
+    "undos_proof"
+    "update_thy"
+    "update_thy_only"
+    "use"
+    "use_thy"
+    "use_thy_only"
+    "welcome"
+    "with"
+    "{"
+    "}"))
+
 (defconst isar-keywords-minor
   '("and"
     "binder"