nominal2: isar-keywords-quot.el@0c3c66f5c0e7 (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"
777 2f72662d21f3 added a print_maps command; updated the keyword file accordingly Christian Urban <urbanc@in.tum.de> parents: 767 diff changeset	176	"print_maps"
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	177	"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	178	"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	179	"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	180	"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	181	"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	182	"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	183	"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	184	"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	185	"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	186	"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	187	"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	188	"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	189	"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	190	"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	191	"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	192	"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	193	"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	194	"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	195	"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	196	"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	197	"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	198	"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	199	"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	200	"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	201	"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	202	"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	203	"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	204	"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	205	"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	206	"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	207	"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	208	"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	209	"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	210	"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	211	"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	212	"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	213	"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	214	"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	215	"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	216	"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	217	"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	218	"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	219	"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	220	"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	221	"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	222	"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	223	"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	224	"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	225	"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	226	"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	227	"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	228	"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	229	"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	230	"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	231	"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	232	"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	233	"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	234	"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	235	"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	236	"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	237	"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	238	"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	239	"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	240	"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	241	"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	242	"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	243	"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	244	"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	245	"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	246	"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	247	"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	248	"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	249	"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	250	"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	251	"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	252	"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	253	"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	254	"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	255	"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	256	"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	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
a603aa6c9d01 with "isabelle 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	(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	261	'("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	262	"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	263	"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	264	"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	265	"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	266	"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	267	"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	268	"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	269	"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	270	"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	271	"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	272	"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	273	"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	274	"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	275	"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	276	"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	277	"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	278	"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	279	"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	280	"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	281	"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	282	"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	283	"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	284	"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	285	"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	286	"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	287	"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	288	"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	289	"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	290	"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	291	"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	292	"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	293	"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	294	"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	295	"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	296	"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	297	"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	298	"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	299	"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	300
a603aa6c9d01 with "isabelle 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	(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	302	'("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	303	"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	304	"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	305	"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	306	"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	307	"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	308	"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	309	"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	310	"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	311	"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	312	"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	313	"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	314	"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	315	"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	316	"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	317	"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	318	"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	319	"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	320	"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	321
a603aa6c9d01 with "isabelle 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	(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	323	'("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	324	"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	325	"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	326	"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	327	"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	328	"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	329	"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	330	"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	331	"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	332	"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	333	"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	334	"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	335	"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	336	"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	337	"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	338	"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	339	"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	340	"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	341	"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	342	"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	343	"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	344	"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	345	"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	346	"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	347	"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	348	"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	349	"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	350	"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	351	"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	352	"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	353	"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	354	"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	355	"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	356	"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	357	"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	358	"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	359	"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	360	"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	361	"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	362	"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	363	"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	364	"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	365	"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	366	"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	367	"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	368	"print_locales"
777 2f72662d21f3 added a print_maps command; updated the keyword file accordingly Christian Urban <urbanc@in.tum.de> parents: 767 diff changeset	369	"print_maps"
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	370	"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	371	"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	372	"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	373	"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	374	"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	375	"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	376	"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	377	"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	378	"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	379	"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	380	"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	381	"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	382	"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	383	"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	384	"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	385	"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	386	"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	387	"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	388	"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	389	"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	390	"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	391	"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	392	"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	393	"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	394	"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	395	"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	396	"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	397	"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	398
a603aa6c9d01 with "isabelle 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	(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	400	'("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	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	(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	403	'())
a603aa6c9d01 with "isabelle 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
a603aa6c9d01 with "isabelle 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	(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	406	'("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	407
a603aa6c9d01 with "isabelle 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	(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	409	'("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	410	"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	411	"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	412	"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	413
a603aa6c9d01 with "isabelle 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	(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	415	'("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	416	"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	417	"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	418	"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	419	"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	420	"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	421	"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	422	"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	423	"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	424	"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	425	"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	426	"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	427	"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	428	"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	429	"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	430	"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	431	"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	432	"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	433	"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	434	"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	435	"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	436	"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	437	"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	438	"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	439	"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	440	"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	441	"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	442	"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	443	"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	444	"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	445	"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	446	"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	447	"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	448	"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	449	"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	450	"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	451	"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	452	"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	453	"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	454	"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	455	"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	456	"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	457	"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	458	"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	459	"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	460	"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	461	"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	462	"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	463	"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	464	"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	465	"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	466	"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	467	"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	468	"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	469	"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	470	"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	471	"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	472	"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	473	"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	474	"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	475	"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	476	"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	477	"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	478	"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	479	"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	480	"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	481	"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	482	"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	483	"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	484	"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	485	"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	486	"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	487	"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	488	"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	489	"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	490	"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	491	"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	492	"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	493	"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	494	"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	495	"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	496	"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	497	"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	498	"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	499	"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	500
a603aa6c9d01 with "isabelle 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	(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	502	'("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	503
a603aa6c9d01 with "isabelle 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	(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	505	'("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	506	"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	507	"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	508	"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	509	"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	510	"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	511	"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	512	"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	513	"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	514	"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	515	"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	516	"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	517	"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	518	"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	519	"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	520	"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	521	"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	522	"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	523	"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	524	"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	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	(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	527	'("\\."
a603aa6c9d01 with "isabelle 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	"\\.\\."
a603aa6c9d01 with "isabelle 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	"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	530	"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	531	"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	532
a603aa6c9d01 with "isabelle 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	(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	534	'("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	535
a603aa6c9d01 with "isabelle 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	(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	537	'("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	538
a603aa6c9d01 with "isabelle 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	(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	540	'("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	541	"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	542	"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	543
a603aa6c9d01 with "isabelle 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	(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	545	'("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	546	"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	547	"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	548
a603aa6c9d01 with "isabelle 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	(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	550	'("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	551	"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	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	(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	554	'("{"))
a603aa6c9d01 with "isabelle 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	(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	557	'("}"))
a603aa6c9d01 with "isabelle 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
a603aa6c9d01 with "isabelle 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	(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	560	'("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	561	"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	562	"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	563	"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	564	"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	565
a603aa6c9d01 with "isabelle 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	(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	567	'("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	568	"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	569	"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	570	"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	571	"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	572	"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	573	"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	574	"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	575	"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	576
a603aa6c9d01 with "isabelle 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	(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	578	'("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	579	"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	580	"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	581	"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	582	"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	583
a603aa6c9d01 with "isabelle 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	(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	585	'("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	586	"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	587	"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	588	"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	589
a603aa6c9d01 with "isabelle 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	(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	591	'("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	592	"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	593	"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	594	"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	595	"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	596
a603aa6c9d01 with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place Christian Urban <urbanc@in.tum.de> parents: diff changeset	597	(provide 'isar-keywords)

author	Christian Urban <urbanc@in.tum.de>
	Tue, 30 Mar 2010 16:59:00 +0200
changeset 1719	0c3c66f5c0e7
parent 777	2f72662d21f3
child 2079	b1d64b7ce2b7
permissions	-rw-r--r--