etc/isar-keywords.el
author krauss
Mon, 23 Jan 2006 15:23:31 +0100
changeset 18759 2f55e3e47355
parent 18757 f0d901bc0686
child 18775 becdbf57eeb8
permissions -rw-r--r--
Updated to Isabelle 2006-01-23

;;
;; Keyword classification tables for Isabelle/Isar.
;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
;;
;; $Id$
;;

(defconst isar-keywords-major
  '("\\."
    "\\.\\."
    "ML"
    "ML_command"
    "ML_setup"
    "ProofGeneral\\.call_atp"
    "ProofGeneral\\.context_thy_only"
    "ProofGeneral\\.inform_file_processed"
    "ProofGeneral\\.inform_file_retracted"
    "ProofGeneral\\.kill_proof"
    "ProofGeneral\\.process_pgip"
    "ProofGeneral\\.redo"
    "ProofGeneral\\.restart"
    "ProofGeneral\\.try_context_thy_only"
    "ProofGeneral\\.undo"
    "also"
    "apply"
    "apply_end"
    "arities"
    "assume"
    "automaton"
    "ax_specification"
    "axclass"
    "axiomatization"
    "axioms"
    "back"
    "by"
    "cannot_undo"
    "case"
    "cd"
    "chapter"
    "class"
    "class_instance"
    "classes"
    "classrel"
    "clear_undos"
    "code_alias"
    "code_class"
    "code_generate"
    "code_library"
    "code_module"
    "code_primclass"
    "code_primconst"
    "code_primtyco"
    "code_serialize"
    "code_syntax_const"
    "code_syntax_tyco"
    "coinductive"
    "commit"
    "constdefs"
    "consts"
    "consts_code"
    "context"
    "corollary"
    "cpodef"
    "datatype"
    "declare"
    "def"
    "defaultsort"
    "defer"
    "defer_recdef"
    "defs"
    "disable_pr"
    "display_drafts"
    "domain"
    "done"
    "enable_pr"
    "end"
    "exit"
    "extract"
    "extract_type"
    "finalconsts"
    "finally"
    "find_theorems"
    "fix"
    "fixpat"
    "fixrec"
    "from"
    "full_prf"
    "global"
    "guess"
    "have"
    "header"
    "hence"
    "hide"
    "inductive"
    "inductive_cases"
    "init_toplevel"
    "instance"
    "interpret"
    "interpretation"
    "judgment"
    "kill"
    "kill_thy"
    "lemma"
    "lemmas"
    "let"
    "local"
    "locale"
    "method_setup"
    "moreover"
    "next"
    "no_syntax"
    "nonterminals"
    "note"
    "obtain"
    "oops"
    "oracle"
    "parse_ast_translation"
    "parse_translation"
    "pcpodef"
    "pr"
    "prefer"
    "presume"
    "pretty_setmargin"
    "prf"
    "primrec"
    "print_antiquotations"
    "print_ast_translation"
    "print_attributes"
    "print_binds"
    "print_cases"
    "print_claset"
    "print_commands"
    "print_context"
    "print_drafts"
    "print_facts"
    "print_induct_rules"
    "print_interps"
    "print_locale"
    "print_locales"
    "print_methods"
    "print_rules"
    "print_simpset"
    "print_syntax"
    "print_theorems"
    "print_theory"
    "print_trans_rules"
    "print_translation"
    "proof"
    "prop"
    "pwd"
    "qed"
    "quickcheck"
    "quickcheck_params"
    "quit"
    "realizability"
    "realizers"
    "recdef"
    "recdef_tc"
    "record"
    "redo"
    "refute"
    "refute_params"
    "remove_thy"
    "rep_datatype"
    "sect"
    "section"
    "setup"
    "show"
    "sorry"
    "specification"
    "subsect"
    "subsection"
    "subsubsect"