isabelle-cookbook: ProgTutorial/Package/simple-keyword/isar-keywords-simple.el@0753bc271fd5 (annotated)

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

author	Christian Sternagel
	Tue, 19 Jun 2012 12:45:22 +0900
changeset 523	0753bc271fd5
parent 206	096776f180fc
permissions	-rw-r--r--