wneuper/isa: etc/isar-keywords.el@30911da9fb27 (annotated)

wenzelm@11538	1	;;
wenzelm@11538	2	;; Keyword classification tables for Isabelle/Isar.
berghofe@17552	3	;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
wenzelm@11538	4	;;
wenzelm@11538	5	;; $Id$
wenzelm@11538	6	;;
wenzelm@11538	7
wenzelm@11538	8	(defconst isar-keywords-major
wenzelm@11538	9	'("\\."
wenzelm@15762	10	"\\.\\."
wenzelm@11538	11	"ML"
wenzelm@11538	12	"ML_command"
wenzelm@11538	13	"ML_setup"
paulson@17091	14	"ProofGeneral\\.call_atp"
wenzelm@11538	15	"ProofGeneral\\.context_thy_only"
wenzelm@11538	16	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	17	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	18	"ProofGeneral\\.kill_proof"
wenzelm@14938	19	"ProofGeneral\\.process_pgip"
wenzelm@15762	20	"ProofGeneral\\.redo"
wenzelm@11538	21	"ProofGeneral\\.restart"
wenzelm@11538	22	"ProofGeneral\\.try_context_thy_only"
wenzelm@11538	23	"ProofGeneral\\.undo"
wenzelm@11538	24	"also"
wenzelm@11538	25	"apply"
wenzelm@11538	26	"apply_end"
wenzelm@11538	27	"arities"
wenzelm@11538	28	"assume"
wenzelm@12040	29	"automaton"
skalberg@14223	30	"ax_specification"
wenzelm@11538	31	"axclass"
wenzelm@11538	32	"axioms"
wenzelm@11538	33	"back"
wenzelm@11538	34	"by"
wenzelm@11538	35	"cannot_undo"
wenzelm@11538	36	"case"
wenzelm@11538	37	"cd"
wenzelm@11538	38	"chapter"
haftmann@18552	39	"class"
wenzelm@11538	40	"classes"
wenzelm@11538	41	"classrel"
wenzelm@11538	42	"clear_undos"
haftmann@18332	43	"code_alias"
haftmann@18332	44	"code_class"
haftmann@18219	45	"code_generate"
berghofe@17147	46	"code_library"
berghofe@17147	47	"code_module"
haftmann@18519	48	"code_primclass"
haftmann@18519	49	"code_primconst"
haftmann@18519	50	"code_primtyco"
haftmann@18221	51	"code_serialize"
haftmann@18219	52	"code_syntax_const"
haftmann@18219	53	"code_syntax_tyco"
wenzelm@11538	54	"coinductive"
wenzelm@11538	55	"commit"
wenzelm@11538	56	"constdefs"
wenzelm@11538	57	"consts"
wenzelm@11538	58	"consts_code"
wenzelm@11538	59	"context"
wenzelm@11746	60	"corollary"
huffman@16701	61	"cpodef"
wenzelm@11538	62	"datatype"
wenzelm@11538	63	"declare"
wenzelm@11538	64	"def"
wenzelm@11538	65	"defaultsort"
wenzelm@11538	66	"defer"
wenzelm@11538	67	"defer_recdef"
wenzelm@11538	68	"defs"
wenzelm@11538	69	"disable_pr"
wenzelm@14938	70	"display_drafts"
wenzelm@12040	71	"domain"
wenzelm@11538	72	"done"
wenzelm@11538	73	"enable_pr"
wenzelm@11538	74	"end"
wenzelm@11538	75	"exit"
berghofe@13407	76	"extract"
berghofe@13407	77	"extract_type"
skalberg@14223	78	"finalconsts"
wenzelm@11538	79	"finally"
wenzelm@17220	80	"find_theorems"
wenzelm@11538	81	"fix"
wenzelm@16419	82	"fixpat"
huffman@16231	83	"fixrec"
wenzelm@11538	84	"from"
wenzelm@11538	85	"full_prf"
wenzelm@11538	86	"global"
wenzelm@17850	87	"guess"
wenzelm@11538	88	"have"
wenzelm@11538	89	"header"
wenzelm@11538	90	"hence"
wenzelm@11538	91	"hide"
wenzelm@11538	92	"inductive"
wenzelm@11538	93	"inductive_cases"
wenzelm@11538	94	"init_toplevel"
wenzelm@11538	95	"instance"
ballarin@15624	96	"interpret"
ballarin@15598	97	"interpretation"
wenzelm@11538	98	"judgment"
wenzelm@11538	99	"kill"
wenzelm@11538	100	"kill_thy"
wenzelm@11538	101	"lemma"
wenzelm@11538	102	"lemmas"
wenzelm@11538	103	"let"
wenzelm@11538	104	"local"
wenzelm@12059	105	"locale"
wenzelm@11538	106	"method_setup"
wenzelm@11538	107	"moreover"
wenzelm@11538	108	"next"
wenzelm@15703	109	"no_syntax"
wenzelm@11538	110	"nonterminals"
wenzelm@11538	111	"note"
wenzelm@11538	112	"obtain"
wenzelm@11538	113	"oops"
wenzelm@11538	114	"oracle"
wenzelm@11538	115	"parse_ast_translation"
wenzelm@11538	116	"parse_translation"
huffman@16701	117	"pcpodef"
wenzelm@11538	118	"pr"
wenzelm@11538	119	"prefer"
wenzelm@11538	120	"presume"
wenzelm@11538	121	"pretty_setmargin"
wenzelm@11538	122	"prf"
wenzelm@11538	123	"primrec"
wenzelm@11538	124	"print_antiquotations"
wenzelm@11538	125	"print_ast_translation"
wenzelm@11538	126	"print_attributes"
wenzelm@11538	127	"print_binds"
wenzelm@11538	128	"print_cases"
wenzelm@11538	129	"print_claset"
wenzelm@11538	130	"print_commands"
wenzelm@11538	131	"print_context"
wenzelm@14938	132	"print_drafts"
wenzelm@11538	133	"print_facts"
wenzelm@11661	134	"print_induct_rules"
ballarin@15598	135	"print_interps"
wenzelm@12059	136	"print_locale"
wenzelm@12059	137	"print_locales"
wenzelm@11538	138	"print_methods"
wenzelm@12365	139	"print_rules"
wenzelm@11538	140	"print_simpset"
wenzelm@11538	141	"print_syntax"
wenzelm@11538	142	"print_theorems"
wenzelm@11538	143	"print_theory"
wenzelm@11538	144	"print_trans_rules"
wenzelm@11538	145	"print_translation"
wenzelm@11538	146	"proof"
wenzelm@11538	147	"prop"
wenzelm@11538	148	"pwd"
wenzelm@11538	149	"qed"
berghofe@14109	150	"quickcheck"
berghofe@14109	151	"quickcheck_params"
wenzelm@11538	152	"quit"
berghofe@13407	153	"realizability"
berghofe@13407	154	"realizers"
wenzelm@11538	155	"recdef"
wenzelm@11538	156	"recdef_tc"
wenzelm@11538	157	"record"
wenzelm@11538	158	"redo"
webertj@14349	159	"refute"
webertj@14349	160	"refute_params"
wenzelm@11538	161	"remove_thy"
wenzelm@11538	162	"rep_datatype"
wenzelm@11538	163	"sect"
wenzelm@11538	164	"section"
wenzelm@11538	165	"setup"
wenzelm@11538	166	"show"
wenzelm@11538	167	"sorry"
skalberg@14115	168	"specification"
wenzelm@11538	169	"subsect"
wenzelm@11538	170	"subsection"
wenzelm@11538	171	"subsubsect"
wenzelm@11538	172	"subsubsection"
wenzelm@11538	173	"syntax"
wenzelm@11538	174	"term"
wenzelm@11538	175	"text"
wenzelm@11538	176	"text_raw"
wenzelm@11538	177	"then"
wenzelm@11538	178	"theorem"
wenzelm@11538	179	"theorems"
wenzelm@11538	180	"theory"
wenzelm@11538	181	"thm"
wenzelm@11538	182	"thm_deps"
wenzelm@11538	183	"thus"
wenzelm@11538	184	"token_translation"
wenzelm@11538	185	"touch_all_thys"
wenzelm@11538	186	"touch_child_thys"
wenzelm@11538	187	"touch_thy"
wenzelm@11538	188	"translations"
wenzelm@11538	189	"txt"
wenzelm@11538	190	"txt_raw"
wenzelm@11538	191	"typ"
wenzelm@11538	192	"typed_print_translation"
wenzelm@11538	193	"typedecl"
wenzelm@11538	194	"typedef"
wenzelm@11538	195	"types"
wenzelm@11538	196	"types_code"
wenzelm@11538	197	"ultimately"
wenzelm@11538	198	"undo"
wenzelm@11538	199	"undos_proof"
wenzelm@18541	200	"unfolding"
wenzelm@11538	201	"update_thy"
wenzelm@11538	202	"update_thy_only"
wenzelm@11538	203	"use"
wenzelm@11538	204	"use_thy"
wenzelm@11538	205	"use_thy_only"
wenzelm@12926	206	"using"
berghofe@17552	207	"value"
wenzelm@11538	208	"welcome"
wenzelm@11538	209	"with"
wenzelm@11538	210	"{"
wenzelm@11538	211	"}"))
wenzelm@11538	212
wenzelm@11538	213	(defconst isar-keywords-minor
wenzelm@12040	214	'("actions"
wenzelm@14660	215	"advanced"
wenzelm@12040	216	"and"
wenzelm@12042	217	"assumes"
berghofe@16771	218	"attach"
nipkow@15135	219	"begin"
wenzelm@11538	220	"binder"
wenzelm@12040	221	"compose"
wenzelm@11538	222	"concl"
wenzelm@11538	223	"congs"
haftmann@18380	224	"constants"
ballarin@16168	225	"constrains"
berghofe@17147	226	"contains"
wenzelm@12042	227	"defines"
haftmann@18219	228	"depending_on"
wenzelm@11538	229	"distinct"
berghofe@17147	230	"file"
wenzelm@11538	231	"files"
wenzelm@12042	232	"fixes"
wenzelm@12040	233	"hide_action"
wenzelm@11538	234	"hints"
nipkow@15141	235	"imports"
wenzelm@11538	236	"in"
wenzelm@12954	237	"includes"
wenzelm@11538	238	"induction"
wenzelm@11661	239	"infix"
wenzelm@11538	240	"infixl"
wenzelm@11538	241	"infixr"
wenzelm@12040	242	"initially"
wenzelm@11538	243	"inject"
wenzelm@12040	244	"inputs"
wenzelm@12040	245	"internals"
wenzelm@11538	246	"intros"
wenzelm@11538	247	"is"
wenzelm@12040	248	"lazy"
wenzelm@11538	249	"monos"
wenzelm@11746	250	"morphisms"
wenzelm@12042	251	"notes"
wenzelm@13364	252	"open"
wenzelm@11538	253	"output"
wenzelm@12040	254	"outputs"
wenzelm@11538	255	"overloaded"
wenzelm@11618	256	"permissive"
wenzelm@12040	257	"post"
wenzelm@12040	258	"pre"
wenzelm@12040	259	"rename"
wenzelm@12040	260	"restrict"
wenzelm@12935	261	"shows"
wenzelm@12040	262	"signature"
wenzelm@12040	263	"states"
wenzelm@12042	264	"structure"
wenzelm@12040	265	"to"
wenzelm@12040	266	"transitions"
wenzelm@12040	267	"transrel"
wenzelm@16419	268	"uses"
wenzelm@11538	269	"where"))
wenzelm@11538	270
wenzelm@11538	271	(defconst isar-keywords-control
wenzelm@11538	272	'("ProofGeneral\\.context_thy_only"
wenzelm@11538	273	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	274	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	275	"ProofGeneral\\.kill_proof"
wenzelm@14938	276	"ProofGeneral\\.process_pgip"
wenzelm@15762	277	"ProofGeneral\\.redo"
wenzelm@11538	278	"ProofGeneral\\.restart"
wenzelm@11538	279	"ProofGeneral\\.try_context_thy_only"
wenzelm@11538	280	"ProofGeneral\\.undo"
wenzelm@11538	281	"cannot_undo"
wenzelm@11538	282	"clear_undos"
wenzelm@11538	283	"exit"
wenzelm@11538	284	"init_toplevel"
wenzelm@11538	285	"kill"
wenzelm@11538	286	"quit"
wenzelm@11538	287	"redo"
wenzelm@11538	288	"undo"
wenzelm@11538	289	"undos_proof"))
wenzelm@11538	290
wenzelm@11538	291	(defconst isar-keywords-diag
wenzelm@11538	292	'("ML"
wenzelm@11538	293	"ML_command"
paulson@17091	294	"ProofGeneral\\.call_atp"
wenzelm@11538	295	"cd"
wenzelm@11538	296	"commit"
wenzelm@11538	297	"disable_pr"
wenzelm@14938	298	"display_drafts"
wenzelm@11538	299	"enable_pr"
wenzelm@17220	300	"find_theorems"
wenzelm@11538	301	"full_prf"
wenzelm@11538	302	"header"
wenzelm@11538	303	"kill_thy"
wenzelm@11538	304	"pr"
wenzelm@11538	305	"pretty_setmargin"
wenzelm@11538	306	"prf"
wenzelm@11538	307	"print_antiquotations"
wenzelm@11538	308	"print_attributes"
wenzelm@11538	309	"print_binds"
wenzelm@11538	310	"print_cases"
wenzelm@11538	311	"print_claset"
wenzelm@11538	312	"print_commands"
wenzelm@11538	313	"print_context"
wenzelm@14938	314	"print_drafts"
wenzelm@11538	315	"print_facts"
wenzelm@11661	316	"print_induct_rules"
ballarin@15598	317	"print_interps"
wenzelm@12059	318	"print_locale"
wenzelm@12059	319	"print_locales"
wenzelm@11538	320	"print_methods"
wenzelm@12365	321	"print_rules"
wenzelm@11538	322	"print_simpset"
wenzelm@11538	323	"print_syntax"
wenzelm@11538	324	"print_theorems"
wenzelm@11538	325	"print_theory"
wenzelm@11538	326	"print_trans_rules"
wenzelm@11538	327	"prop"
wenzelm@11538	328	"pwd"
berghofe@14109	329	"quickcheck"
webertj@14349	330	"refute"
wenzelm@11538	331	"remove_thy"
wenzelm@11538	332	"term"
wenzelm@11538	333	"thm"
wenzelm@11538	334	"thm_deps"
wenzelm@11538	335	"touch_all_thys"
wenzelm@11538	336	"touch_child_thys"
wenzelm@11538	337	"touch_thy"
wenzelm@11538	338	"typ"
wenzelm@11538	339	"update_thy"
wenzelm@11538	340	"update_thy_only"
wenzelm@11538	341	"use"
wenzelm@11538	342	"use_thy"
wenzelm@11538	343	"use_thy_only"
berghofe@17552	344	"value"
wenzelm@11538	345	"welcome"))
wenzelm@11538	346
wenzelm@11538	347	(defconst isar-keywords-theory-begin
wenzelm@11538	348	'("theory"))
wenzelm@11538	349
wenzelm@11538	350	(defconst isar-keywords-theory-switch
wenzelm@11538	351	'("context"))
wenzelm@11538	352
wenzelm@11538	353	(defconst isar-keywords-theory-end
wenzelm@11538	354	'("end"))
wenzelm@11538	355
wenzelm@11538	356	(defconst isar-keywords-theory-heading
wenzelm@11538	357	'("chapter"
wenzelm@11538	358	"section"
wenzelm@11538	359	"subsection"
wenzelm@11538	360	"subsubsection"))
wenzelm@11538	361
wenzelm@11538	362	(defconst isar-keywords-theory-decl
wenzelm@11538	363	'("ML_setup"
wenzelm@11538	364	"arities"
wenzelm@12040	365	"automaton"
wenzelm@11538	366	"axclass"
wenzelm@11538	367	"axioms"
haftmann@18552	368	"class"
wenzelm@11538	369	"classes"
wenzelm@11538	370	"classrel"
haftmann@18332	371	"code_alias"
haftmann@18332	372	"code_class"
haftmann@18219	373	"code_generate"
berghofe@17147	374	"code_library"
berghofe@17147	375	"code_module"
haftmann@18519	376	"code_primclass"
haftmann@18519	377	"code_primconst"
haftmann@18519	378	"code_primtyco"
haftmann@18221	379	"code_serialize"
haftmann@18219	380	"code_syntax_const"
haftmann@18219	381	"code_syntax_tyco"
wenzelm@11538	382	"coinductive"
wenzelm@11538	383	"constdefs"
wenzelm@11538	384	"consts"
wenzelm@11538	385	"consts_code"
wenzelm@11538	386	"datatype"
wenzelm@11538	387	"defaultsort"
wenzelm@11538	388	"defer_recdef"
wenzelm@11538	389	"defs"
wenzelm@12040	390	"domain"
berghofe@13407	391	"extract"
berghofe@13407	392	"extract_type"
skalberg@14223	393	"finalconsts"
wenzelm@16419	394	"fixpat"
huffman@16231	395	"fixrec"
wenzelm@11538	396	"global"
wenzelm@11538	397	"hide"
wenzelm@11538	398	"inductive"
wenzelm@11538	399	"judgment"
wenzelm@11538	400	"lemmas"
wenzelm@11538	401	"local"
wenzelm@12059	402	"locale"
wenzelm@11538	403	"method_setup"
wenzelm@15703	404	"no_syntax"
wenzelm@11538	405	"nonterminals"
wenzelm@11538	406	"oracle"
wenzelm@11538	407	"parse_ast_translation"
wenzelm@11538	408	"parse_translation"
wenzelm@11538	409	"primrec"
wenzelm@11538	410	"print_ast_translation"
wenzelm@11538	411	"print_translation"
berghofe@14109	412	"quickcheck_params"
berghofe@13407	413	"realizability"
berghofe@13407	414	"realizers"
wenzelm@11538	415	"recdef"
wenzelm@11538	416	"record"
webertj@14349	417	"refute_params"
wenzelm@11538	418	"rep_datatype"
wenzelm@11538	419	"setup"
wenzelm@11538	420	"syntax"
wenzelm@11538	421	"text"
wenzelm@11538	422	"text_raw"
wenzelm@11538	423	"theorems"
wenzelm@11538	424	"token_translation"
wenzelm@11538	425	"translations"
wenzelm@11538	426	"typed_print_translation"
wenzelm@11538	427	"typedecl"
wenzelm@11538	428	"types"
wenzelm@11538	429	"types_code"))
wenzelm@11538	430
wenzelm@11538	431	(defconst isar-keywords-theory-script
wenzelm@11538	432	'("declare"
wenzelm@11538	433	"inductive_cases"))
wenzelm@11538	434
wenzelm@11538	435	(defconst isar-keywords-theory-goal
skalberg@14223	436	'("ax_specification"
skalberg@14223	437	"corollary"
huffman@16701	438	"cpodef"
wenzelm@11746	439	"instance"
ballarin@15598	440	"interpretation"
wenzelm@11538	441	"lemma"
huffman@16701	442	"pcpodef"
wenzelm@11538	443	"recdef_tc"
skalberg@14115	444	"specification"
wenzelm@11538	445	"theorem"
wenzelm@11538	446	"typedef"))
wenzelm@11538	447
wenzelm@11538	448	(defconst isar-keywords-qed
wenzelm@11538	449	'("\\."
wenzelm@11538	450	"\\.\\."
wenzelm@11538	451	"by"
wenzelm@11538	452	"done"
wenzelm@11538	453	"sorry"))
wenzelm@11538	454
wenzelm@11538	455	(defconst isar-keywords-qed-block
wenzelm@11538	456	'("qed"))
wenzelm@11538	457
wenzelm@11538	458	(defconst isar-keywords-qed-global
wenzelm@11538	459	'("oops"))
wenzelm@11538	460
wenzelm@11538	461	(defconst isar-keywords-proof-heading
wenzelm@11538	462	'("sect"
wenzelm@11538	463	"subsect"
wenzelm@11538	464	"subsubsect"))
wenzelm@11538	465
wenzelm@11538	466	(defconst isar-keywords-proof-goal
wenzelm@11538	467	'("have"
wenzelm@11538	468	"hence"
ballarin@15624	469	"interpret"
wenzelm@11538	470	"show"
wenzelm@11538	471	"thus"))
wenzelm@11538	472
wenzelm@11538	473	(defconst isar-keywords-proof-block
wenzelm@11538	474	'("next"
wenzelm@11538	475	"proof"))
wenzelm@11538	476
wenzelm@11538	477	(defconst isar-keywords-proof-open
wenzelm@11538	478	'("{"))
wenzelm@11538	479
wenzelm@11538	480	(defconst isar-keywords-proof-close
wenzelm@11538	481	'("}"))
wenzelm@11538	482
wenzelm@11538	483	(defconst isar-keywords-proof-chain
wenzelm@11538	484	'("finally"
wenzelm@11538	485	"from"
wenzelm@11538	486	"then"
wenzelm@11538	487	"ultimately"
wenzelm@11538	488	"with"))
wenzelm@11538	489
wenzelm@11538	490	(defconst isar-keywords-proof-decl
wenzelm@11538	491	'("also"
wenzelm@11538	492	"let"
wenzelm@11538	493	"moreover"
wenzelm@11538	494	"note"
wenzelm@11538	495	"txt"
wenzelm@12926	496	"txt_raw"
wenzelm@18541	497	"unfolding"
wenzelm@12926	498	"using"))
wenzelm@11538	499
wenzelm@11538	500	(defconst isar-keywords-proof-asm
wenzelm@11538	501	'("assume"
wenzelm@11538	502	"case"
wenzelm@11538	503	"def"
wenzelm@11538	504	"fix"
wenzelm@11538	505	"presume"))
wenzelm@11538	506
wenzelm@11538	507	(defconst isar-keywords-proof-asm-goal
wenzelm@17850	508	'("guess"
wenzelm@17850	509	"obtain"))
wenzelm@11538	510
wenzelm@11538	511	(defconst isar-keywords-proof-script
wenzelm@11538	512	'("apply"
wenzelm@11538	513	"apply_end"
wenzelm@11538	514	"back"
wenzelm@11538	515	"defer"
wenzelm@11538	516	"prefer"))
wenzelm@11538	517
wenzelm@11538	518	(provide 'isar-keywords)

author	haftmann
	Tue, 03 Jan 2006 11:33:18 +0100
changeset 18552	30911da9fb27
parent 18541	00890455e95f
child 18612	7300f75028dc
permissions	-rw-r--r--