nominal2: isar-keywords-quot.el@d6acae26d027 (annotated)

764 a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	;;
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	2	;; Keyword classification tables for Isabelle/Isar.
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure.
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	5	;;
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	6
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	(defconst isar-keywords-major
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	'("\\."
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	9	"\\.\\."
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	"Isabelle\\.command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	"Isar\\.begin_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	12	"Isar\\.define_command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	"Isar\\.edit_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	"Isar\\.end_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	15	"ML"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	"ML_command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	17	"ML_prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	"ML_val"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	19	"ProofGeneral\\.inform_file_processed"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	20	"ProofGeneral\\.inform_file_retracted"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	"ProofGeneral\\.kill_proof"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	22	"ProofGeneral\\.pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	"ProofGeneral\\.process_pgip"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	"ProofGeneral\\.restart"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	"ProofGeneral\\.undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	"abbreviation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	"also"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	"apply"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	29	"apply_end"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	30	"arities"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	31	"assume"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	32	"atom_decl"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	33	"atp_info"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	34	"atp_kill"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	35	"atp_messages"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	36	"atp_minimize"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	37	"attribute_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	38	"ax_specification"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	39	"axclass"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	40	"axiomatization"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	41	"axioms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	42	"back"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	43	"by"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	44	"cannot_undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	45	"case"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	46	"cd"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	47	"chapter"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	48	"class"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	49	"class_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	50	"classes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	51	"classrel"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	52	"code_abort"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	53	"code_class"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	54	"code_const"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	55	"code_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	"code_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	57	"code_include"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	"code_instance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	"code_library"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	"code_module"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	61	"code_modulename"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	62	"code_monad"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	63	"code_pred"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	64	"code_reserved"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	65	"code_thms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	"code_type"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	67	"coinductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	68	"coinductive_set"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	69	"commit"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	70	"constdefs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	71	"consts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	72	"consts_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	73	"context"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	74	"corollary"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	75	"datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	76	"declaration"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	77	"declare"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	78	"def"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	79	"defaultsort"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	"defer"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	"defer_recdef"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	"definition"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	"defs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	"disable_pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	"display_drafts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	86	"done"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	"enable_pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	"end"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	"equivariance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	"exit"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	"export_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	"extract"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	"extract_type"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	"finalconsts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	"finally"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	96	"find_consts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	"find_theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	"fix"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	"from"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	"full_prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	101	"fun"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	"function"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	"global"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	"guess"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	"have"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	"header"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	"help"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	"hence"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	"hide"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	"inductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	"inductive_cases"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	"inductive_set"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	113	"init_toplevel"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	114	"instance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	115	"instantiation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	116	"interpret"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	117	"interpretation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	118	"judgment"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	119	"kill"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	120	"kill_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	121	"lemma"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	122	"lemmas"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	123	"let"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	124	"linear_undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	125	"local"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	126	"local_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	127	"locale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	128	"method_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	129	"moreover"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	130	"next"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	131	"nitpick"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	132	"nitpick_params"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	133	"no_notation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	134	"no_syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	135	"no_translations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	136	"nominal_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	137	"nominal_inductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	138	"nominal_inductive2"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	139	"nominal_primrec"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	140	"nonterminals"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	"normal_form"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	142	"notation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	143	"note"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	144	"obtain"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	145	"oops"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	146	"oracle"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	147	"overloading"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	148	"parse_ast_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	149	"parse_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	150	"pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	151	"prefer"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	152	"presume"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	153	"pretty_setmargin"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	154	"prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	155	"primrec"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	156	"print_abbrevs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	157	"print_antiquotations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	158	"print_ast_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	159	"print_atps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	160	"print_attributes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	161	"print_binds"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	162	"print_cases"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	163	"print_claset"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	164	"print_classes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	165	"print_codeproc"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	166	"print_codesetup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	167	"print_commands"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	168	"print_configs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	169	"print_context"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	170	"print_drafts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	171	"print_facts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	172	"print_induct_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	173	"print_interps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	174	"print_locale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	175	"print_locales"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	176	"print_methods"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	177	"print_orders"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	178	"print_quotconsts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	179	"print_quotients"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	180	"print_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	181	"print_simpset"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	182	"print_statement"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	183	"print_syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	184	"print_theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	185	"print_theory"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	186	"print_trans_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	187	"print_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	188	"proof"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	189	"prop"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	190	"prove"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	191	"pwd"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	192	"qed"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	193	"quickcheck"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	194	"quickcheck_params"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	195	"quit"
767 37285ec4387d on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file Christian Urban <urbanc@in.tum.de> parents: 766 diff changeset	196	"quotient_definition"
766 df053507edba renamed "quotient" command to "quotient_type"; needs new keyword file to be installed Christian Urban <urbanc@in.tum.de> parents: 764 diff changeset	197	"quotient_type"
764 a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	198	"realizability"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	199	"realizers"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	200	"recdef"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	201	"recdef_tc"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	202	"record"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	203	"refute"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	204	"refute_params"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	205	"remove_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	206	"rep_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	207	"sect"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	208	"section"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	209	"setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	210	"show"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	211	"simproc_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	212	"sledgehammer"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	213	"sorry"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	214	"specification"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	215	"subclass"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	216	"sublocale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	217	"subsect"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	218	"subsection"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	219	"subsubsect"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	220	"subsubsection"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	221	"syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	222	"term"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	223	"termination"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	224	"text"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	225	"text_raw"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	226	"then"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	227	"theorem"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	228	"theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	229	"theory"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	230	"thm"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	231	"thm_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	232	"thus"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	233	"thy_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	234	"touch_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	235	"translations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	236	"txt"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	237	"txt_raw"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	238	"typ"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	239	"typed_print_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	240	"typedecl"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	241	"typedef"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	242	"types"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	243	"types_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	244	"ultimately"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	245	"undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	246	"undos_proof"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	247	"unfolding"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	248	"unused_thms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	249	"use"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	250	"use_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	251	"using"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	252	"value"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	253	"values"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	254	"welcome"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	255	"with"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	256	"{"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	257	"}"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	258
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	259	(defconst isar-keywords-minor
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	260	'("advanced"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	261	"and"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	262	"as"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	263	"assumes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	264	"attach"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	265	"avoids"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	266	"begin"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	267	"binder"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	268	"congs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	269	"constrains"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	270	"contains"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	271	"defines"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	272	"file"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	273	"fixes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	274	"for"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	275	"hints"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	276	"identifier"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	277	"if"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	278	"imports"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	279	"in"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	280	"infix"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	281	"infixl"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	282	"infixr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	283	"is"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	284	"module_name"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	285	"monos"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	286	"morphisms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	287	"notes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	288	"obtains"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	289	"open"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	290	"output"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	291	"overloaded"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	292	"permissive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	293	"pervasive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	294	"shows"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	295	"structure"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	296	"unchecked"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	297	"uses"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	298	"where"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	299
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	300	(defconst isar-keywords-control
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	301	'("Isabelle\\.command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	302	"Isar\\.begin_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	303	"Isar\\.define_command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	304	"Isar\\.edit_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	305	"Isar\\.end_document"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	306	"ProofGeneral\\.inform_file_processed"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	307	"ProofGeneral\\.inform_file_retracted"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	308	"ProofGeneral\\.kill_proof"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	309	"ProofGeneral\\.process_pgip"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	310	"ProofGeneral\\.restart"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	311	"ProofGeneral\\.undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	312	"cannot_undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	313	"exit"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	314	"init_toplevel"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	315	"kill"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	316	"linear_undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	317	"quit"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	318	"undo"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	319	"undos_proof"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	320
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	321	(defconst isar-keywords-diag
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	322	'("ML_command"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	323	"ML_val"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	324	"ProofGeneral\\.pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	325	"atp_info"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	326	"atp_kill"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	327	"atp_messages"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	328	"atp_minimize"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	329	"cd"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	330	"class_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	331	"code_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	332	"code_thms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	333	"commit"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	334	"disable_pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	335	"display_drafts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	336	"enable_pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	337	"export_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	338	"find_consts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	339	"find_theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	340	"full_prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	341	"header"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	342	"help"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	343	"kill_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	344	"nitpick"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	345	"normal_form"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	346	"pr"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	347	"pretty_setmargin"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	348	"prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	349	"print_abbrevs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	350	"print_antiquotations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	351	"print_atps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	352	"print_attributes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	353	"print_binds"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	354	"print_cases"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	355	"print_claset"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	356	"print_classes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	357	"print_codeproc"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	358	"print_codesetup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	359	"print_commands"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	360	"print_configs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	361	"print_context"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	362	"print_drafts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	363	"print_facts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	364	"print_induct_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	365	"print_interps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	366	"print_locale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	367	"print_locales"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	368	"print_methods"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	369	"print_orders"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	370	"print_quotconsts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	371	"print_quotients"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	372	"print_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	373	"print_simpset"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	374	"print_statement"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	375	"print_syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	376	"print_theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	377	"print_theory"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	378	"print_trans_rules"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	379	"prop"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	380	"pwd"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	381	"quickcheck"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	382	"refute"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	383	"remove_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	384	"sledgehammer"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	385	"term"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	386	"thm"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	387	"thm_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	388	"thy_deps"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	389	"touch_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	390	"typ"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	391	"unused_thms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	392	"use_thy"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	393	"value"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	394	"values"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	395	"welcome"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	396
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	397	(defconst isar-keywords-theory-begin
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	398	'("theory"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	399
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	400	(defconst isar-keywords-theory-switch
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	401	'())
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	402
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	403	(defconst isar-keywords-theory-end
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	404	'("end"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	405
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	406	(defconst isar-keywords-theory-heading
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	407	'("chapter"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	408	"section"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	409	"subsection"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	410	"subsubsection"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	411
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	412	(defconst isar-keywords-theory-decl
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	413	'("ML"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	414	"abbreviation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	415	"arities"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	416	"atom_decl"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	417	"attribute_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	418	"axclass"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	419	"axiomatization"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	420	"axioms"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	421	"class"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	422	"classes"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	423	"classrel"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	424	"code_abort"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	425	"code_class"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	426	"code_const"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	427	"code_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	428	"code_include"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	429	"code_instance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	430	"code_library"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	431	"code_module"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	432	"code_modulename"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	433	"code_monad"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	434	"code_reserved"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	435	"code_type"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	436	"coinductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	437	"coinductive_set"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	438	"constdefs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	439	"consts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	440	"consts_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	441	"context"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	442	"datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	443	"declaration"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	444	"declare"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	445	"defaultsort"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	446	"defer_recdef"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	447	"definition"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	448	"defs"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	449	"equivariance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	450	"extract"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	451	"extract_type"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	452	"finalconsts"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	453	"fun"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	454	"global"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	455	"hide"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	456	"inductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	457	"inductive_set"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	458	"instantiation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	459	"judgment"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	460	"lemmas"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	461	"local"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	462	"local_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	463	"locale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	464	"method_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	465	"nitpick_params"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	466	"no_notation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	467	"no_syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	468	"no_translations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	469	"nominal_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	470	"nonterminals"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	471	"notation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	472	"oracle"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	473	"overloading"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	474	"parse_ast_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	475	"parse_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	476	"primrec"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	477	"print_ast_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	478	"print_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	479	"quickcheck_params"
767 37285ec4387d on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file Christian Urban <urbanc@in.tum.de> parents: 766 diff changeset	480	"quotient_definition"
764 a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	481	"realizability"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	482	"realizers"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	483	"recdef"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	484	"record"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	485	"refute_params"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	486	"setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	487	"simproc_setup"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	488	"syntax"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	489	"text"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	490	"text_raw"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	491	"theorems"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	492	"translations"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	493	"typed_print_translation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	494	"typedecl"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	495	"types"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	496	"types_code"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	497	"use"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	498
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	499	(defconst isar-keywords-theory-script
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	500	'("inductive_cases"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	501
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	502	(defconst isar-keywords-theory-goal
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	503	'("ax_specification"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	504	"code_pred"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	505	"corollary"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	506	"function"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	507	"instance"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	508	"interpretation"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	509	"lemma"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	510	"nominal_inductive"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	511	"nominal_inductive2"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	512	"nominal_primrec"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	513	"prove"
766 df053507edba renamed "quotient" command to "quotient_type"; needs new keyword file to be installed Christian Urban <urbanc@in.tum.de> parents: 764 diff changeset	514	"quotient_type"
764 a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	515	"recdef_tc"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	516	"rep_datatype"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	517	"specification"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	518	"subclass"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	519	"sublocale"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	520	"termination"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	521	"theorem"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	522	"typedef"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	523
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	524	(defconst isar-keywords-qed
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	525	'("\\."
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	526	"\\.\\."
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	527	"by"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	528	"done"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	529	"sorry"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	530
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	531	(defconst isar-keywords-qed-block
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	532	'("qed"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	533
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	534	(defconst isar-keywords-qed-global
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	535	'("oops"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	536
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	537	(defconst isar-keywords-proof-heading
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	538	'("sect"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	539	"subsect"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	540	"subsubsect"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	541
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	542	(defconst isar-keywords-proof-goal
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	543	'("have"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	544	"hence"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	545	"interpret"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	546
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	547	(defconst isar-keywords-proof-block
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	548	'("next"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	549	"proof"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	550
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	551	(defconst isar-keywords-proof-open
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	552	'("{"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	553
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	554	(defconst isar-keywords-proof-close
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	555	'("}"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	556
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	557	(defconst isar-keywords-proof-chain
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	558	'("finally"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	559	"from"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	560	"then"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	561	"ultimately"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	562	"with"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	563
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	564	(defconst isar-keywords-proof-decl
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	565	'("ML_prf"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	566	"also"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	567	"let"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	568	"moreover"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	569	"note"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	570	"txt"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	571	"txt_raw"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	572	"unfolding"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	573	"using"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	574
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	575	(defconst isar-keywords-proof-asm
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	576	'("assume"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	577	"case"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	578	"def"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	579	"fix"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	580	"presume"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	581
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	582	(defconst isar-keywords-proof-asm-goal
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	583	'("guess"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	584	"obtain"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	585	"show"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	586	"thus"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	587
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	588	(defconst isar-keywords-proof-script
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	589	'("apply"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	590	"apply_end"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	591	"back"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	592	"defer"
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	593	"prefer"))
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	594
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	595	(provide 'isar-keywords)

author	Christian Urban <urbanc@in.tum.de>
	Tue, 22 Dec 2009 20:51:37 +0100
changeset 773	d6acae26d027
parent 767	37285ec4387d
child 777	2f72662d21f3
permissions	-rw-r--r--