wneuper/isa: etc/isar-keywords-ZF.el@fcd5af4aac2b (annotated)

wenzelm@12176	1	;;
wenzelm@12176	2	;; Keyword classification tables for Isabelle/Isar.
wenzelm@49724	3	;; Generated from ZF.
wenzelm@24904	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
wenzelm@12176	5	;;
wenzelm@12176	6
wenzelm@12176	7	(defconst isar-keywords-major
wenzelm@12176	8	'("\\."
wenzelm@12176	9	"\\.\\."
wenzelm@25577	10	"Isabelle\\.command"
wenzelm@12176	11	"ML"
wenzelm@12176	12	"ML_command"
wenzelm@49882	13	"ML_file"
wenzelm@28261	14	"ML_prf"
wenzelm@26394	15	"ML_val"
wenzelm@12176	16	"ProofGeneral\\.inform_file_processed"
wenzelm@12176	17	"ProofGeneral\\.inform_file_retracted"
wenzelm@12176	18	"ProofGeneral\\.kill_proof"
wenzelm@33874	19	"ProofGeneral\\.pr"
wenzelm@14937	20	"ProofGeneral\\.process_pgip"
wenzelm@12176	21	"ProofGeneral\\.restart"
wenzelm@12176	22	"ProofGeneral\\.undo"
wenzelm@19069	23	"abbreviation"
wenzelm@12176	24	"also"
wenzelm@12176	25	"apply"
wenzelm@12176	26	"apply_end"
wenzelm@12176	27	"arities"
wenzelm@12176	28	"assume"
wenzelm@30529	29	"attribute_setup"
haftmann@18702	30	"axiomatization"
wenzelm@12176	31	"back"
wenzelm@47928	32	"bundle"
wenzelm@12176	33	"by"
wenzelm@12176	34	"cannot_undo"
wenzelm@12176	35	"case"
wenzelm@12176	36	"cd"
wenzelm@12176	37	"chapter"
haftmann@18552	38	"class"
wenzelm@20568	39	"class_deps"
wenzelm@12176	40	"classes"
wenzelm@12176	41	"classrel"
bulwahn@31107	42	"codatatype"
haftmann@22486	43	"code_datatype"
bulwahn@31107	44	"coinductive"
wenzelm@12176	45	"commit"
wenzelm@12176	46	"consts"
wenzelm@12176	47	"context"
wenzelm@12176	48	"corollary"
bulwahn@31107	49	"datatype"
wenzelm@22084	50	"declaration"
wenzelm@12176	51	"declare"
wenzelm@12176	52	"def"
wenzelm@36455	53	"default_sort"
wenzelm@12176	54	"defer"
wenzelm@18775	55	"definition"
wenzelm@12176	56	"defs"
wenzelm@12176	57	"disable_pr"
wenzelm@14937	58	"display_drafts"
wenzelm@12176	59	"done"
wenzelm@12176	60	"enable_pr"
wenzelm@12176	61	"end"
wenzelm@12176	62	"exit"
berghofe@13407	63	"extract"
berghofe@13407	64	"extract_type"
wenzelm@12176	65	"finally"
kleing@29819	66	"find_consts"
wenzelm@17220	67	"find_theorems"
wenzelm@12176	68	"fix"
wenzelm@12176	69	"from"
wenzelm@12176	70	"full_prf"
wenzelm@17850	71	"guess"
wenzelm@12176	72	"have"
wenzelm@12176	73	"header"
wenzelm@21732	74	"help"
wenzelm@12176	75	"hence"
wenzelm@36180	76	"hide_class"
wenzelm@36180	77	"hide_const"
wenzelm@36180	78	"hide_fact"
wenzelm@36180	79	"hide_type"
wenzelm@47928	80	"include"
wenzelm@47928	81	"including"
bulwahn@31107	82	"inductive"
bulwahn@31107	83	"inductive_cases"
wenzelm@12176	84	"init_toplevel"
wenzelm@12176	85	"instance"
wenzelm@24866	86	"instantiation"
ballarin@15624	87	"interpret"
ballarin@15598	88	"interpretation"
wenzelm@12176	89	"judgment"
wenzelm@12176	90	"kill"
wenzelm@12176	91	"kill_thy"
wenzelm@12176	92	"lemma"
wenzelm@12176	93	"lemmas"
wenzelm@12176	94	"let"
wenzelm@27538	95	"linear_undo"
wenzelm@30463	96	"local_setup"
wenzelm@12176	97	"locale"
wenzelm@50586	98	"locale_deps"
wenzelm@12176	99	"method_setup"
wenzelm@12176	100	"moreover"
wenzelm@12176	101	"next"
wenzelm@24945	102	"no_notation"
wenzelm@15762	103	"no_syntax"
wenzelm@19255	104	"no_translations"
wenzelm@35419	105	"no_type_notation"
wenzelm@41495	106	"nonterminal"
wenzelm@21203	107	"notation"
wenzelm@12176	108	"note"
wenzelm@41208	109	"notepad"
wenzelm@12176	110	"obtain"
wenzelm@12176	111	"oops"
wenzelm@12176	112	"oracle"
haftmann@25516	113	"overloading"
wenzelm@12176	114	"parse_ast_translation"
wenzelm@12176	115	"parse_translation"
wenzelm@12176	116	"pr"
wenzelm@12176	117	"prefer"
wenzelm@12176	118	"presume"
wenzelm@12176	119	"pretty_setmargin"
wenzelm@12176	120	"prf"
bulwahn@31107	121	"primrec"
wenzelm@21732	122	"print_abbrevs"
wenzelm@12176	123	"print_antiquotations"
wenzelm@12176	124	"print_ast_translation"
wenzelm@12176	125	"print_attributes"
wenzelm@12176	126	"print_binds"
wenzelm@47928	127	"print_bundles"
wenzelm@12176	128	"print_cases"
wenzelm@12176	129	"print_claset"
haftmann@20378	130	"print_classes"
haftmann@22288	131	"print_codesetup"
wenzelm@12176	132	"print_commands"
wenzelm@24111	133	"print_configs"
wenzelm@12176	134	"print_context"
wenzelm@52722	135	"print_defn_rules"
ballarin@41683	136	"print_dependencies"
wenzelm@14937	137	"print_drafts"
wenzelm@12176	138	"print_facts"
wenzelm@12176	139	"print_induct_rules"
ballarin@32788	140	"print_interps"
wenzelm@12176	141	"print_locale"
wenzelm@12176	142	"print_locales"
wenzelm@12176	143	"print_methods"
wenzelm@12365	144	"print_rules"
wenzelm@12176	145	"print_simpset"
wenzelm@19272	146	"print_statement"
wenzelm@12176	147	"print_syntax"
bulwahn@31107	148	"print_tcset"
wenzelm@12176	149	"print_theorems"
wenzelm@12176	150	"print_theory"
wenzelm@12176	151	"print_trans_rules"
wenzelm@12176	152	"print_translation"
wenzelm@12176	153	"proof"
wenzelm@12176	154	"prop"
wenzelm@12176	155	"pwd"
wenzelm@12176	156	"qed"
wenzelm@12176	157	"quit"
berghofe@13407	158	"realizability"
berghofe@13407	159	"realizers"
wenzelm@12176	160	"remove_thy"
bulwahn@31107	161	"rep_datatype"
wenzelm@36321	162	"schematic_corollary"
wenzelm@36321	163	"schematic_lemma"
wenzelm@36321	164	"schematic_theorem"
wenzelm@12176	165	"sect"
wenzelm@12176	166	"section"
wenzelm@12176	167	"setup"
wenzelm@12176	168	"show"
wenzelm@22200	169	"simproc_setup"
wenzelm@12176	170	"sorry"
haftmann@24919	171	"subclass"
ballarin@28895	172	"sublocale"
wenzelm@12176	173	"subsect"
wenzelm@12176	174	"subsection"
wenzelm@12176	175	"subsubsect"
wenzelm@12176	176	"subsubsection"
wenzelm@12176	177	"syntax"
wenzelm@41034	178	"syntax_declaration"
wenzelm@12176	179	"term"
wenzelm@12176	180	"text"
wenzelm@12176	181	"text_raw"
wenzelm@12176	182	"then"
wenzelm@12176	183	"theorem"
wenzelm@12176	184	"theorems"
wenzelm@12176	185	"theory"
wenzelm@12176	186	"thm"
wenzelm@12176	187	"thm_deps"
wenzelm@12176	188	"thus"
haftmann@22486	189	"thy_deps"
wenzelm@12176	190	"translations"
wenzelm@12176	191	"txt"
wenzelm@12176	192	"txt_raw"
wenzelm@12176	193	"typ"
wenzelm@35419	194	"type_notation"
wenzelm@41497	195	"type_synonym"
wenzelm@12176	196	"typed_print_translation"
wenzelm@12176	197	"typedecl"
wenzelm@12176	198	"ultimately"
wenzelm@12176	199	"undo"
wenzelm@12176	200	"undos_proof"
wenzelm@18541	201	"unfolding"
berghofe@26184	202	"unused_thms"
wenzelm@12176	203	"use_thy"
wenzelm@12926	204	"using"
wenzelm@12176	205	"welcome"
wenzelm@12176	206	"with"
wenzelm@36521	207	"write"
wenzelm@12176	208	"{"
wenzelm@12176	209	"}"))
wenzelm@12176	210
wenzelm@12176	211	(defconst isar-keywords-minor
wenzelm@14660	212	'("advanced"
wenzelm@14660	213	"and"
wenzelm@12176	214	"assumes"
berghofe@17147	215	"attach"
nipkow@15135	216	"begin"
wenzelm@12176	217	"binder"
bulwahn@31107	218	"case_eqns"
bulwahn@31107	219	"con_defs"
ballarin@16168	220	"constrains"
wenzelm@12176	221	"defines"
bulwahn@31107	222	"domains"
bulwahn@31107	223	"elimination"
wenzelm@12176	224	"fixes"
wenzelm@19797	225	"for"
haftmann@22288	226	"identifier"
wenzelm@19797	227	"if"
nipkow@15141	228	"imports"
wenzelm@12176	229	"in"
wenzelm@47946	230	"includes"
bulwahn@31107	231	"induction"
wenzelm@12176	232	"infix"
wenzelm@12176	233	"infixl"
wenzelm@12176	234	"infixr"
bulwahn@31107	235	"intros"
wenzelm@12176	236	"is"
wenzelm@47812	237	"keywords"
bulwahn@31107	238	"monos"
wenzelm@12176	239	"notes"
wenzelm@18888	240	"obtains"
wenzelm@13364	241	"open"
wenzelm@12176	242	"output"
wenzelm@12176	243	"overloaded"
wenzelm@33685	244	"pervasive"
bulwahn@31107	245	"recursor_eqns"
wenzelm@12935	246	"shows"
wenzelm@12176	247	"structure"
bulwahn@31107	248	"type_elims"
bulwahn@31107	249	"type_intros"
wenzelm@19633	250	"unchecked"
wenzelm@12176	251	"where"))
wenzelm@12176	252
wenzelm@12176	253	(defconst isar-keywords-control
wenzelm@25577	254	'("Isabelle\\.command"
wenzelm@25577	255	"ProofGeneral\\.inform_file_processed"
wenzelm@12176	256	"ProofGeneral\\.inform_file_retracted"
wenzelm@12176	257	"ProofGeneral\\.kill_proof"
wenzelm@14937	258	"ProofGeneral\\.process_pgip"
wenzelm@12176	259	"ProofGeneral\\.restart"
wenzelm@12176	260	"ProofGeneral\\.undo"
wenzelm@12176	261	"cannot_undo"
wenzelm@40675	262	"cd"
wenzelm@40675	263	"commit"
wenzelm@38276	264	"disable_pr"
wenzelm@38276	265	"enable_pr"
wenzelm@12176	266	"exit"
wenzelm@12176	267	"init_toplevel"
wenzelm@12176	268	"kill"
wenzelm@38276	269	"kill_thy"
wenzelm@27538	270	"linear_undo"
wenzelm@52407	271	"pretty_setmargin"
wenzelm@12176	272	"quit"
wenzelm@38276	273	"remove_thy"
wenzelm@12176	274	"undo"
wenzelm@38276	275	"undos_proof"
wenzelm@38276	276	"use_thy"))
wenzelm@12176	277
wenzelm@12176	278	(defconst isar-keywords-diag
wenzelm@26482	279	'("ML_command"
wenzelm@26394	280	"ML_val"
wenzelm@33874	281	"ProofGeneral\\.pr"
wenzelm@20568	282	"class_deps"
wenzelm@14937	283	"display_drafts"
kleing@29819	284	"find_consts"
wenzelm@17220	285	"find_theorems"
wenzelm@12176	286	"full_prf"
wenzelm@12176	287	"header"
wenzelm@21732	288	"help"
wenzelm@50586	289	"locale_deps"
wenzelm@12176	290	"pr"
wenzelm@12176	291	"prf"
wenzelm@21732	292	"print_abbrevs"
wenzelm@12176	293	"print_antiquotations"
wenzelm@12176	294	"print_attributes"
wenzelm@12176	295	"print_binds"
wenzelm@47928	296	"print_bundles"
wenzelm@12176	297	"print_cases"
wenzelm@12176	298	"print_claset"
haftmann@20378	299	"print_classes"
haftmann@22288	300	"print_codesetup"
wenzelm@12176	301	"print_commands"
wenzelm@24111	302	"print_configs"
wenzelm@12176	303	"print_context"
wenzelm@52722	304	"print_defn_rules"
ballarin@41683	305	"print_dependencies"
wenzelm@14937	306	"print_drafts"
wenzelm@12176	307	"print_facts"
wenzelm@12176	308	"print_induct_rules"
ballarin@32788	309	"print_interps"
wenzelm@12176	310	"print_locale"
wenzelm@12176	311	"print_locales"
wenzelm@12176	312	"print_methods"
wenzelm@12365	313	"print_rules"
wenzelm@12176	314	"print_simpset"
wenzelm@19272	315	"print_statement"
wenzelm@12176	316	"print_syntax"
bulwahn@31107	317	"print_tcset"
wenzelm@12176	318	"print_theorems"
wenzelm@12176	319	"print_theory"
wenzelm@12176	320	"print_trans_rules"
wenzelm@12176	321	"prop"
wenzelm@12176	322	"pwd"
wenzelm@12176	323	"term"
wenzelm@12176	324	"thm"
wenzelm@12176	325	"thm_deps"
haftmann@22486	326	"thy_deps"
wenzelm@12176	327	"typ"
berghofe@26184	328	"unused_thms"
wenzelm@12176	329	"welcome"))
wenzelm@12176	330
wenzelm@12176	331	(defconst isar-keywords-theory-begin
wenzelm@12176	332	'("theory"))
wenzelm@12176	333
wenzelm@12176	334	(defconst isar-keywords-theory-switch
wenzelm@21302	335	'())
wenzelm@12176	336
wenzelm@12176	337	(defconst isar-keywords-theory-end
wenzelm@12176	338	'("end"))
wenzelm@12176	339
wenzelm@12176	340	(defconst isar-keywords-theory-heading
wenzelm@12176	341	'("chapter"
wenzelm@12176	342	"section"
wenzelm@12176	343	"subsection"
wenzelm@12176	344	"subsubsection"))
wenzelm@12176	345
wenzelm@12176	346	(defconst isar-keywords-theory-decl
wenzelm@26482	347	'("ML"
wenzelm@49882	348	"ML_file"
wenzelm@19069	349	"abbreviation"
wenzelm@12176	350	"arities"
wenzelm@30529	351	"attribute_setup"
haftmann@18702	352	"axiomatization"
wenzelm@47928	353	"bundle"
haftmann@18552	354	"class"
wenzelm@12176	355	"classes"
wenzelm@12176	356	"classrel"
bulwahn@31107	357	"codatatype"
haftmann@22486	358	"code_datatype"
bulwahn@31107	359	"coinductive"
wenzelm@12176	360	"consts"
wenzelm@21302	361	"context"
bulwahn@31107	362	"datatype"
wenzelm@22084	363	"declaration"
wenzelm@23804	364	"declare"
wenzelm@36455	365	"default_sort"
wenzelm@18775	366	"definition"
wenzelm@12176	367	"defs"
berghofe@13407	368	"extract"
berghofe@13407	369	"extract_type"
wenzelm@36180	370	"hide_class"
wenzelm@36180	371	"hide_const"
wenzelm@36180	372	"hide_fact"
wenzelm@36180	373	"hide_type"
bulwahn@31107	374	"inductive"
wenzelm@24866	375	"instantiation"
wenzelm@12176	376	"judgment"
wenzelm@12176	377	"lemmas"
wenzelm@30463	378	"local_setup"
wenzelm@12176	379	"locale"
wenzelm@12176	380	"method_setup"
wenzelm@24945	381	"no_notation"
wenzelm@15762	382	"no_syntax"
wenzelm@19255	383	"no_translations"
wenzelm@35419	384	"no_type_notation"
wenzelm@41495	385	"nonterminal"
wenzelm@21203	386	"notation"
wenzelm@41208	387	"notepad"
wenzelm@12176	388	"oracle"
haftmann@25516	389	"overloading"
wenzelm@12176	390	"parse_ast_translation"
wenzelm@12176	391	"parse_translation"
bulwahn@31107	392	"primrec"
wenzelm@12176	393	"print_ast_translation"
wenzelm@12176	394	"print_translation"
berghofe@13407	395	"realizability"
berghofe@13407	396	"realizers"
bulwahn@31107	397	"rep_datatype"
wenzelm@12176	398	"setup"
wenzelm@22200	399	"simproc_setup"
wenzelm@12176	400	"syntax"
wenzelm@41034	401	"syntax_declaration"
wenzelm@12176	402	"text"
wenzelm@12176	403	"text_raw"
wenzelm@12176	404	"theorems"
wenzelm@12176	405	"translations"
wenzelm@35419	406	"type_notation"
wenzelm@41497	407	"type_synonym"
wenzelm@12176	408	"typed_print_translation"
wenzelm@52432	409	"typedecl"))
wenzelm@12176	410
wenzelm@12176	411	(defconst isar-keywords-theory-script
bulwahn@31107	412	'("inductive_cases"))
wenzelm@12176	413
wenzelm@12176	414	(defconst isar-keywords-theory-goal
haftmann@36114	415	'("corollary"
wenzelm@12176	416	"instance"
ballarin@15598	417	"interpretation"
wenzelm@12176	418	"lemma"
wenzelm@36321	419	"schematic_corollary"
wenzelm@36321	420	"schematic_lemma"
wenzelm@36321	421	"schematic_theorem"
haftmann@24919	422	"subclass"
ballarin@28895	423	"sublocale"
wenzelm@12176	424	"theorem"))
wenzelm@12176	425
wenzelm@12176	426	(defconst isar-keywords-qed
wenzelm@12176	427	'("\\."
wenzelm@12176	428	"\\.\\."
wenzelm@12176	429	"by"
wenzelm@12176	430	"done"
wenzelm@12176	431	"sorry"))
wenzelm@12176	432
wenzelm@12176	433	(defconst isar-keywords-qed-block
wenzelm@12176	434	'("qed"))
wenzelm@12176	435
wenzelm@12176	436	(defconst isar-keywords-qed-global
wenzelm@12176	437	'("oops"))
wenzelm@12176	438
wenzelm@12176	439	(defconst isar-keywords-proof-heading
wenzelm@12176	440	'("sect"
wenzelm@12176	441	"subsect"
wenzelm@12176	442	"subsubsect"))
wenzelm@12176	443
wenzelm@12176	444	(defconst isar-keywords-proof-goal
wenzelm@12176	445	'("have"
wenzelm@12176	446	"hence"
wenzelm@29607	447	"interpret"))
wenzelm@12176	448
wenzelm@12176	449	(defconst isar-keywords-proof-block
wenzelm@12176	450	'("next"
wenzelm@12176	451	"proof"))
wenzelm@12176	452
wenzelm@12176	453	(defconst isar-keywords-proof-open
wenzelm@12176	454	'("{"))
wenzelm@12176	455
wenzelm@12176	456	(defconst isar-keywords-proof-close
wenzelm@12176	457	'("}"))
wenzelm@12176	458
wenzelm@12176	459	(defconst isar-keywords-proof-chain
wenzelm@12176	460	'("finally"
wenzelm@12176	461	"from"
wenzelm@12176	462	"then"
wenzelm@12176	463	"ultimately"
wenzelm@12176	464	"with"))
wenzelm@12176	465
wenzelm@12176	466	(defconst isar-keywords-proof-decl
wenzelm@28261	467	'("ML_prf"
wenzelm@28261	468	"also"
wenzelm@47928	469	"include"
wenzelm@47928	470	"including"
wenzelm@12176	471	"let"
wenzelm@12176	472	"moreover"
wenzelm@12176	473	"note"
wenzelm@12176	474	"txt"
wenzelm@12926	475	"txt_raw"
wenzelm@18541	476	"unfolding"
wenzelm@36521	477	"using"
wenzelm@36521	478	"write"))
wenzelm@12176	479
wenzelm@12176	480	(defconst isar-keywords-proof-asm
wenzelm@12176	481	'("assume"
wenzelm@12176	482	"case"
wenzelm@12176	483	"def"
wenzelm@12176	484	"fix"
wenzelm@12176	485	"presume"))
wenzelm@12176	486
wenzelm@12176	487	(defconst isar-keywords-proof-asm-goal
wenzelm@17850	488	'("guess"
wenzelm@21806	489	"obtain"
wenzelm@21806	490	"show"
wenzelm@21806	491	"thus"))
wenzelm@12176	492
wenzelm@12176	493	(defconst isar-keywords-proof-script
wenzelm@12176	494	'("apply"
wenzelm@12176	495	"apply_end"
wenzelm@12176	496	"back"
wenzelm@12176	497	"defer"
wenzelm@12176	498	"prefer"))
wenzelm@12176	499
wenzelm@12176	500	(provide 'isar-keywords)

author	wenzelm
	Sat, 30 Mar 2013 14:57:06 +0100
changeset 52722	fcd5af4aac2b
parent 52450	102a0a0718c5
child 53197	179236c82c2a
permissions	-rw-r--r--