wneuper/isa: etc/isar-keywords.el@87ba9d3e1020 (annotated)

wenzelm@11538	1	;;
wenzelm@11538	2	;; Keyword classification tables for Isabelle/Isar.
wenzelm@48133	3	;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-HOL_Light.
wenzelm@24904	4	;; * DO NOT EDIT * DO NOT EDIT * DO NOT EDIT *
wenzelm@11538	5	;;
wenzelm@11538	6
wenzelm@11538	7	(defconst isar-keywords-major
wenzelm@11538	8	'("\\."
wenzelm@15762	9	"\\.\\."
wenzelm@25577	10	"Isabelle\\.command"
wenzelm@11538	11	"ML"
wenzelm@11538	12	"ML_command"
wenzelm@28280	13	"ML_prf"
wenzelm@26394	14	"ML_val"
wenzelm@11538	15	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	16	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	17	"ProofGeneral\\.kill_proof"
wenzelm@33874	18	"ProofGeneral\\.pr"
wenzelm@14938	19	"ProofGeneral\\.process_pgip"
wenzelm@11538	20	"ProofGeneral\\.restart"
wenzelm@11538	21	"ProofGeneral\\.undo"
wenzelm@19069	22	"abbreviation"
wenzelm@11538	23	"also"
wenzelm@11538	24	"apply"
wenzelm@11538	25	"apply_end"
wenzelm@11538	26	"arities"
wenzelm@11538	27	"assume"
wenzelm@24904	28	"atom_decl"
wenzelm@30529	29	"attribute_setup"
skalberg@14223	30	"ax_specification"
wenzelm@18612	31	"axiomatization"
wenzelm@11538	32	"axioms"
wenzelm@11538	33	"back"
wenzelm@33687	34	"boogie_end"
wenzelm@33687	35	"boogie_open"
wenzelm@33687	36	"boogie_status"
wenzelm@33687	37	"boogie_vc"
wenzelm@47928	38	"bundle"
wenzelm@11538	39	"by"
wenzelm@11538	40	"cannot_undo"
wenzelm@11538	41	"case"
wenzelm@11538	42	"cd"
wenzelm@11538	43	"chapter"
haftmann@18552	44	"class"
wenzelm@20568	45	"class_deps"
wenzelm@11538	46	"classes"
wenzelm@11538	47	"classrel"
haftmann@27102	48	"code_abort"
haftmann@20424	49	"code_class"
haftmann@20453	50	"code_const"
haftmann@22486	51	"code_datatype"
wenzelm@22864	52	"code_deps"
haftmann@24997	53	"code_include"
haftmann@20424	54	"code_instance"
wenzelm@21203	55	"code_modulename"
wenzelm@22084	56	"code_monad"
bulwahn@31106	57	"code_pred"
haftmann@36468	58	"code_reflect"
wenzelm@21028	59	"code_reserved"
haftmann@22288	60	"code_thms"
haftmann@20453	61	"code_type"
wenzelm@11538	62	"coinductive"
berghofe@23732	63	"coinductive_set"
wenzelm@11538	64	"commit"
wenzelm@11538	65	"consts"
wenzelm@11538	66	"context"
wenzelm@11746	67	"corollary"
huffman@16701	68	"cpodef"
wenzelm@11538	69	"datatype"
wenzelm@22084	70	"declaration"
wenzelm@11538	71	"declare"
wenzelm@11538	72	"def"
wenzelm@36455	73	"default_sort"
wenzelm@11538	74	"defer"
wenzelm@11538	75	"defer_recdef"
wenzelm@18775	76	"definition"
wenzelm@11538	77	"defs"
wenzelm@11538	78	"disable_pr"
wenzelm@14938	79	"display_drafts"
wenzelm@12040	80	"domain"
wenzelm@33840	81	"domain_isomorphism"
haftmann@40822	82	"domaindef"
wenzelm@11538	83	"done"
wenzelm@11538	84	"enable_pr"
wenzelm@11538	85	"end"
wenzelm@41778	86	"enriched_type"
wenzelm@24904	87	"equivariance"
wenzelm@11538	88	"exit"
haftmann@24343	89	"export_code"
berghofe@13407	90	"extract"
berghofe@13407	91	"extract_type"
wenzelm@11538	92	"finally"
kleing@29819	93	"find_consts"
wenzelm@17220	94	"find_theorems"
bulwahn@47460	95	"find_unused_assms"
wenzelm@11538	96	"fix"
huffman@16231	97	"fixrec"
wenzelm@11538	98	"from"
wenzelm@11538	99	"full_prf"
krauss@20523	100	"fun"
krauss@19564	101	"function"
wenzelm@17850	102	"guess"
wenzelm@11538	103	"have"
wenzelm@11538	104	"header"
wenzelm@21732	105	"help"
wenzelm@11538	106	"hence"
wenzelm@36180	107	"hide_class"
wenzelm@36180	108	"hide_const"
wenzelm@36180	109	"hide_fact"
wenzelm@36180	110	"hide_type"
wenzelm@48133	111	"import_const_map"
wenzelm@48133	112	"import_file"
wenzelm@47825	113	"import_tptp"
wenzelm@48133	114	"import_type_map"
wenzelm@47928	115	"include"
wenzelm@47928	116	"including"
wenzelm@11538	117	"inductive"
wenzelm@11538	118	"inductive_cases"
berghofe@23732	119	"inductive_set"
bulwahn@37733	120	"inductive_simps"
wenzelm@11538	121	"init_toplevel"
wenzelm@11538	122	"instance"
haftmann@24437	123	"instantiation"
ballarin@15624	124	"interpret"
ballarin@15598	125	"interpretation"
wenzelm@11538	126	"judgment"
wenzelm@11538	127	"kill"
wenzelm@11538	128	"kill_thy"
wenzelm@11538	129	"lemma"
wenzelm@11538	130	"lemmas"
wenzelm@11538	131	"let"
wenzelm@27538	132	"linear_undo"
wenzelm@30463	133	"local_setup"
wenzelm@12059	134	"locale"
wenzelm@11538	135	"method_setup"
wenzelm@11538	136	"moreover"
wenzelm@11538	137	"next"
blanchet@33198	138	"nitpick"
blanchet@33198	139	"nitpick_params"
wenzelm@24945	140	"no_notation"
wenzelm@15703	141	"no_syntax"
wenzelm@19255	142	"no_translations"
wenzelm@35419	143	"no_type_notation"
wenzelm@24904	144	"nominal_datatype"
wenzelm@24904	145	"nominal_inductive"
berghofe@28656	146	"nominal_inductive2"
wenzelm@24904	147	"nominal_primrec"
wenzelm@41495	148	"nonterminal"
wenzelm@21203	149	"notation"
wenzelm@11538	150	"note"
wenzelm@41208	151	"notepad"
wenzelm@11538	152	"obtain"
wenzelm@11538	153	"oops"
wenzelm@11538	154	"oracle"
haftmann@25516	155	"overloading"
wenzelm@11538	156	"parse_ast_translation"
wenzelm@11538	157	"parse_translation"
haftmann@40356	158	"partial_function"
huffman@16701	159	"pcpodef"
wenzelm@11538	160	"pr"
wenzelm@11538	161	"prefer"
wenzelm@11538	162	"presume"
wenzelm@11538	163	"pretty_setmargin"
wenzelm@11538	164	"prf"
wenzelm@11538	165	"primrec"
wenzelm@21732	166	"print_abbrevs"
wenzelm@11538	167	"print_antiquotations"
wenzelm@11538	168	"print_ast_translation"
wenzelm@11538	169	"print_attributes"
wenzelm@11538	170	"print_binds"
wenzelm@47928	171	"print_bundles"
wenzelm@11538	172	"print_cases"
wenzelm@11538	173	"print_claset"
haftmann@20378	174	"print_classes"
haftmann@31130	175	"print_codeproc"
haftmann@22288	176	"print_codesetup"
berghofe@45927	177	"print_coercion_maps"
berghofe@45927	178	"print_coercions"
wenzelm@11538	179	"print_commands"
wenzelm@24120	180	"print_configs"
wenzelm@11538	181	"print_context"
ballarin@41683	182	"print_dependencies"
wenzelm@14938	183	"print_drafts"
wenzelm@11538	184	"print_facts"
wenzelm@11661	185	"print_induct_rules"
ballarin@32788	186	"print_interps"
wenzelm@12059	187	"print_locale"
wenzelm@12059	188	"print_locales"
wenzelm@11538	189	"print_methods"
ballarin@24642	190	"print_orders"
kaliszyk@35279	191	"print_quotconsts"
kaliszyk@35279	192	"print_quotients"
kaliszyk@35279	193	"print_quotmaps"
wenzelm@12365	194	"print_rules"
wenzelm@11538	195	"print_simpset"
wenzelm@19272	196	"print_statement"
wenzelm@11538	197	"print_syntax"
wenzelm@11538	198	"print_theorems"
wenzelm@11538	199	"print_theory"
wenzelm@11538	200	"print_trans_rules"
wenzelm@11538	201	"print_translation"
wenzelm@11538	202	"proof"
wenzelm@11538	203	"prop"
wenzelm@11538	204	"pwd"
wenzelm@11538	205	"qed"
berghofe@14109	206	"quickcheck"
bulwahn@46797	207	"quickcheck_generator"
berghofe@14109	208	"quickcheck_params"
wenzelm@11538	209	"quit"
kaliszyk@35279	210	"quotient_definition"
kaliszyk@35279	211	"quotient_type"
berghofe@13407	212	"realizability"
berghofe@13407	213	"realizers"
wenzelm@11538	214	"recdef"
wenzelm@11538	215	"recdef_tc"
wenzelm@11538	216	"record"
webertj@14349	217	"refute"
webertj@14349	218	"refute_params"
wenzelm@11538	219	"remove_thy"
wenzelm@11538	220	"rep_datatype"
wenzelm@36321	221	"schematic_corollary"
wenzelm@36321	222	"schematic_lemma"
wenzelm@36321	223	"schematic_theorem"
wenzelm@11538	224	"sect"
wenzelm@11538	225	"section"
wenzelm@11538	226	"setup"
kuncar@47968	227	"setup_lifting"
wenzelm@11538	228	"show"
wenzelm@22200	229	"simproc_setup"
wenzelm@22864	230	"sledgehammer"
haftmann@36114	231	"sledgehammer_params"
wenzelm@33898	232	"smt_status"
blanchet@40361	233	"solve_direct"
wenzelm@11538	234	"sorry"
berghofe@41812	235	"spark_end"
berghofe@41812	236	"spark_open"
berghofe@41812	237	"spark_proof_functions"
berghofe@41812	238	"spark_status"
berghofe@43227	239	"spark_types"
berghofe@41812	240	"spark_vc"
skalberg@14115	241	"specification"
wenzelm@25176	242	"statespace"
haftmann@24919	243	"subclass"
ballarin@28895	244	"sublocale"
wenzelm@11538	245	"subsect"
wenzelm@11538	246	"subsection"
wenzelm@11538	247	"subsubsect"
wenzelm@11538	248	"subsubsection"
wenzelm@11538	249	"syntax"
wenzelm@41034	250	"syntax_declaration"
wenzelm@11538	251	"term"
krauss@19564	252	"termination"
wenzelm@11538	253	"text"
wenzelm@11538	254	"text_raw"
wenzelm@11538	255	"then"
wenzelm@11538	256	"theorem"
wenzelm@11538	257	"theorems"
wenzelm@11538	258	"theory"
wenzelm@11538	259	"thm"
wenzelm@11538	260	"thm_deps"
wenzelm@11538	261	"thus"
haftmann@22486	262	"thy_deps"
wenzelm@11538	263	"translations"
blanchet@39169	264	"try"
blanchet@47512	265	"try0"
wenzelm@11538	266	"txt"
wenzelm@11538	267	"txt_raw"
wenzelm@11538	268	"typ"
wenzelm@35419	269	"type_notation"
wenzelm@41497	270	"type_synonym"
wenzelm@11538	271	"typed_print_translation"
wenzelm@11538	272	"typedecl"
wenzelm@11538	273	"typedef"
wenzelm@11538	274	"ultimately"
wenzelm@11538	275	"undo"
wenzelm@11538	276	"undos_proof"
wenzelm@18541	277	"unfolding"
berghofe@26184	278	"unused_thms"
wenzelm@11538	279	"use"
wenzelm@11538	280	"use_thy"
wenzelm@12926	281	"using"
berghofe@17552	282	"value"
haftmann@31130	283	"values"
wenzelm@11538	284	"welcome"
wenzelm@11538	285	"with"
wenzelm@36521	286	"write"
wenzelm@11538	287	"{"
wenzelm@11538	288	"}"))
wenzelm@11538	289
wenzelm@11538	290	(defconst isar-keywords-minor
wenzelm@37785	291	'("advanced"
wenzelm@12040	292	"and"
wenzelm@12042	293	"assumes"
berghofe@16771	294	"attach"
wenzelm@24904	295	"avoids"
nipkow@15135	296	"begin"
wenzelm@11538	297	"binder"
haftmann@37824	298	"checking"
wenzelm@11538	299	"congs"
ballarin@16168	300	"constrains"
haftmann@36468	301	"datatypes"
wenzelm@12042	302	"defines"
berghofe@17147	303	"file"
wenzelm@12042	304	"fixes"
wenzelm@19797	305	"for"
haftmann@36468	306	"functions"
wenzelm@11538	307	"hints"
haftmann@22288	308	"identifier"
wenzelm@19797	309	"if"
nipkow@15141	310	"imports"
wenzelm@11538	311	"in"
wenzelm@47946	312	"includes"
wenzelm@11661	313	"infix"
wenzelm@11538	314	"infixl"
wenzelm@11538	315	"infixr"
wenzelm@11538	316	"is"
wenzelm@47812	317	"keywords"
wenzelm@12040	318	"lazy"
haftmann@24249	319	"module_name"
wenzelm@11538	320	"monos"
wenzelm@11746	321	"morphisms"
wenzelm@12042	322	"notes"
wenzelm@18888	323	"obtains"
wenzelm@13364	324	"open"
wenzelm@11538	325	"output"
wenzelm@11538	326	"overloaded"
wenzelm@11618	327	"permissive"
wenzelm@33685	328	"pervasive"
wenzelm@12935	329	"shows"
wenzelm@12042	330	"structure"
wenzelm@19633	331	"unchecked"
wenzelm@40632	332	"unsafe"
wenzelm@16419	333	"uses"
wenzelm@11538	334	"where"))
wenzelm@11538	335
wenzelm@11538	336	(defconst isar-keywords-control
wenzelm@25577	337	'("Isabelle\\.command"
wenzelm@25577	338	"ProofGeneral\\.inform_file_processed"
wenzelm@11538	339	"ProofGeneral\\.inform_file_retracted"
wenzelm@11538	340	"ProofGeneral\\.kill_proof"
wenzelm@14938	341	"ProofGeneral\\.process_pgip"
wenzelm@11538	342	"ProofGeneral\\.restart"
wenzelm@11538	343	"ProofGeneral\\.undo"
wenzelm@11538	344	"cannot_undo"
wenzelm@40675	345	"cd"
wenzelm@40675	346	"commit"
wenzelm@38276	347	"disable_pr"
wenzelm@38276	348	"enable_pr"
wenzelm@11538	349	"exit"
wenzelm@11538	350	"init_toplevel"
wenzelm@11538	351	"kill"
wenzelm@38276	352	"kill_thy"
wenzelm@27538	353	"linear_undo"
wenzelm@11538	354	"quit"
wenzelm@38276	355	"remove_thy"
wenzelm@11538	356	"undo"
wenzelm@38276	357	"undos_proof"
wenzelm@38276	358	"use_thy"))
wenzelm@11538	359
wenzelm@11538	360	(defconst isar-keywords-diag
wenzelm@26482	361	'("ML_command"
wenzelm@26394	362	"ML_val"
wenzelm@33874	363	"ProofGeneral\\.pr"
wenzelm@33687	364	"boogie_status"
wenzelm@20568	365	"class_deps"
wenzelm@22864	366	"code_deps"
haftmann@22288	367	"code_thms"
wenzelm@14938	368	"display_drafts"
haftmann@24343	369	"export_code"
kleing@29819	370	"find_consts"
wenzelm@17220	371	"find_theorems"
bulwahn@47460	372	"find_unused_assms"
wenzelm@11538	373	"full_prf"
wenzelm@11538	374	"header"
wenzelm@21732	375	"help"
blanchet@33198	376	"nitpick"
wenzelm@11538	377	"pr"
wenzelm@11538	378	"pretty_setmargin"
wenzelm@11538	379	"prf"
wenzelm@21732	380	"print_abbrevs"
wenzelm@11538	381	"print_antiquotations"
wenzelm@11538	382	"print_attributes"
wenzelm@11538	383	"print_binds"
wenzelm@47928	384	"print_bundles"
wenzelm@11538	385	"print_cases"
wenzelm@11538	386	"print_claset"
haftmann@20378	387	"print_classes"
haftmann@31130	388	"print_codeproc"
haftmann@22288	389	"print_codesetup"
berghofe@45927	390	"print_coercion_maps"
berghofe@45927	391	"print_coercions"
wenzelm@11538	392	"print_commands"
wenzelm@24120	393	"print_configs"
wenzelm@11538	394	"print_context"
ballarin@41683	395	"print_dependencies"
wenzelm@14938	396	"print_drafts"
wenzelm@11538	397	"print_facts"
wenzelm@11661	398	"print_induct_rules"
ballarin@32788	399	"print_interps"
wenzelm@12059	400	"print_locale"
wenzelm@12059	401	"print_locales"
wenzelm@11538	402	"print_methods"
ballarin@24642	403	"print_orders"
kaliszyk@35279	404	"print_quotconsts"
kaliszyk@35279	405	"print_quotients"
kaliszyk@35279	406	"print_quotmaps"
wenzelm@12365	407	"print_rules"
wenzelm@11538	408	"print_simpset"
wenzelm@19272	409	"print_statement"
wenzelm@11538	410	"print_syntax"
wenzelm@11538	411	"print_theorems"
wenzelm@11538	412	"print_theory"
wenzelm@11538	413	"print_trans_rules"
wenzelm@11538	414	"prop"
wenzelm@11538	415	"pwd"
berghofe@14109	416	"quickcheck"
webertj@14349	417	"refute"
wenzelm@22864	418	"sledgehammer"
wenzelm@33898	419	"smt_status"
blanchet@40361	420	"solve_direct"
berghofe@41812	421	"spark_status"
wenzelm@11538	422	"term"
wenzelm@11538	423	"thm"
wenzelm@11538	424	"thm_deps"
haftmann@22486	425	"thy_deps"
blanchet@39169	426	"try"
blanchet@47512	427	"try0"
wenzelm@11538	428	"typ"
berghofe@26184	429	"unused_thms"
berghofe@17552	430	"value"
haftmann@31130	431	"values"
wenzelm@11538	432	"welcome"))
wenzelm@11538	433
wenzelm@11538	434	(defconst isar-keywords-theory-begin
wenzelm@11538	435	'("theory"))
wenzelm@11538	436
wenzelm@11538	437	(defconst isar-keywords-theory-switch
wenzelm@21302	438	'())
wenzelm@11538	439
wenzelm@11538	440	(defconst isar-keywords-theory-end
wenzelm@11538	441	'("end"))
wenzelm@11538	442
wenzelm@11538	443	(defconst isar-keywords-theory-heading
wenzelm@11538	444	'("chapter"
wenzelm@11538	445	"section"
wenzelm@11538	446	"subsection"
wenzelm@11538	447	"subsubsection"))
wenzelm@11538	448
wenzelm@11538	449	(defconst isar-keywords-theory-decl
wenzelm@26482	450	'("ML"
wenzelm@19069	451	"abbreviation"
wenzelm@11538	452	"arities"
wenzelm@24904	453	"atom_decl"
wenzelm@30529	454	"attribute_setup"
wenzelm@18612	455	"axiomatization"
wenzelm@11538	456	"axioms"
wenzelm@33687	457	"boogie_end"
wenzelm@33687	458	"boogie_open"
wenzelm@47928	459	"bundle"
haftmann@18552	460	"class"
wenzelm@11538	461	"classes"
wenzelm@11538	462	"classrel"
haftmann@27102	463	"code_abort"
haftmann@20424	464	"code_class"
haftmann@20453	465	"code_const"
haftmann@22486	466	"code_datatype"
haftmann@24997	467	"code_include"
haftmann@20424	468	"code_instance"
wenzelm@21203	469	"code_modulename"
wenzelm@22084	470	"code_monad"
haftmann@36468	471	"code_reflect"
wenzelm@21028	472	"code_reserved"
haftmann@20453	473	"code_type"
wenzelm@11538	474	"coinductive"
berghofe@23732	475	"coinductive_set"
wenzelm@11538	476	"consts"
wenzelm@21302	477	"context"
wenzelm@11538	478	"datatype"
wenzelm@22084	479	"declaration"
wenzelm@23804	480	"declare"
wenzelm@36455	481	"default_sort"
wenzelm@11538	482	"defer_recdef"
wenzelm@18775	483	"definition"
wenzelm@11538	484	"defs"
wenzelm@12040	485	"domain"
wenzelm@33840	486	"domain_isomorphism"
haftmann@40822	487	"domaindef"
wenzelm@24904	488	"equivariance"
berghofe@13407	489	"extract"
berghofe@13407	490	"extract_type"
huffman@16231	491	"fixrec"
krauss@20523	492	"fun"
wenzelm@36180	493	"hide_class"
wenzelm@36180	494	"hide_const"
wenzelm@36180	495	"hide_fact"
wenzelm@36180	496	"hide_type"
wenzelm@48133	497	"import_const_map"
wenzelm@48133	498	"import_file"
wenzelm@47825	499	"import_tptp"
wenzelm@48133	500	"import_type_map"
wenzelm@11538	501	"inductive"
berghofe@23732	502	"inductive_set"
haftmann@24437	503	"instantiation"
wenzelm@11538	504	"judgment"
wenzelm@11538	505	"lemmas"
wenzelm@30463	506	"local_setup"
wenzelm@12059	507	"locale"
wenzelm@11538	508	"method_setup"
blanchet@33198	509	"nitpick_params"
wenzelm@24945	510	"no_notation"
wenzelm@15703	511	"no_syntax"
wenzelm@19255	512	"no_translations"
wenzelm@35419	513	"no_type_notation"
wenzelm@24904	514	"nominal_datatype"
wenzelm@41495	515	"nonterminal"
wenzelm@21203	516	"notation"
wenzelm@41208	517	"notepad"
wenzelm@11538	518	"oracle"
haftmann@25516	519	"overloading"
wenzelm@11538	520	"parse_ast_translation"
wenzelm@11538	521	"parse_translation"
krauss@40450	522	"partial_function"
wenzelm@11538	523	"primrec"
wenzelm@11538	524	"print_ast_translation"
wenzelm@11538	525	"print_translation"
bulwahn@46797	526	"quickcheck_generator"
berghofe@14109	527	"quickcheck_params"
berghofe@13407	528	"realizability"
berghofe@13407	529	"realizers"
wenzelm@11538	530	"recdef"
wenzelm@11538	531	"record"
webertj@14349	532	"refute_params"
wenzelm@11538	533	"setup"
kuncar@47968	534	"setup_lifting"
wenzelm@22200	535	"simproc_setup"
haftmann@36114	536	"sledgehammer_params"
berghofe@41812	537	"spark_end"
berghofe@41812	538	"spark_open"
berghofe@41812	539	"spark_proof_functions"
berghofe@43227	540	"spark_types"
wenzelm@25176	541	"statespace"
wenzelm@11538	542	"syntax"
wenzelm@41034	543	"syntax_declaration"
wenzelm@11538	544	"text"
wenzelm@11538	545	"text_raw"
wenzelm@11538	546	"theorems"
wenzelm@11538	547	"translations"
wenzelm@35419	548	"type_notation"
wenzelm@41497	549	"type_synonym"
wenzelm@11538	550	"typed_print_translation"
wenzelm@11538	551	"typedecl"
wenzelm@26482	552	"use"))
wenzelm@11538	553
wenzelm@11538	554	(defconst isar-keywords-theory-script
bulwahn@37733	555	'("inductive_cases"
bulwahn@37733	556	"inductive_simps"))
wenzelm@11538	557
wenzelm@11538	558	(defconst isar-keywords-theory-goal
skalberg@14223	559	'("ax_specification"
wenzelm@33687	560	"boogie_vc"
bulwahn@31106	561	"code_pred"
skalberg@14223	562	"corollary"
huffman@16701	563	"cpodef"
wenzelm@41778	564	"enriched_type"
krauss@19564	565	"function"
wenzelm@11746	566	"instance"
ballarin@15598	567	"interpretation"
wenzelm@11538	568	"lemma"
wenzelm@24904	569	"nominal_inductive"
berghofe@28656	570	"nominal_inductive2"
wenzelm@24904	571	"nominal_primrec"
huffman@16701	572	"pcpodef"
kuncar@47968	573	"quotient_definition"
kaliszyk@35279	574	"quotient_type"
wenzelm@11538	575	"recdef_tc"
haftmann@27102	576	"rep_datatype"
wenzelm@36321	577	"schematic_corollary"
wenzelm@36321	578	"schematic_lemma"
wenzelm@36321	579	"schematic_theorem"
berghofe@41812	580	"spark_vc"
skalberg@14115	581	"specification"
haftmann@24919	582	"subclass"
ballarin@28895	583	"sublocale"
krauss@19564	584	"termination"
wenzelm@11538	585	"theorem"
wenzelm@11538	586	"typedef"))
wenzelm@11538	587
wenzelm@11538	588	(defconst isar-keywords-qed
wenzelm@11538	589	'("\\."
wenzelm@11538	590	"\\.\\."
wenzelm@11538	591	"by"
wenzelm@11538	592	"done"
wenzelm@11538	593	"sorry"))
wenzelm@11538	594
wenzelm@11538	595	(defconst isar-keywords-qed-block
wenzelm@11538	596	'("qed"))
wenzelm@11538	597
wenzelm@11538	598	(defconst isar-keywords-qed-global
wenzelm@11538	599	'("oops"))
wenzelm@11538	600
wenzelm@11538	601	(defconst isar-keywords-proof-heading
wenzelm@11538	602	'("sect"
wenzelm@11538	603	"subsect"
wenzelm@11538	604	"subsubsect"))
wenzelm@11538	605
wenzelm@11538	606	(defconst isar-keywords-proof-goal
wenzelm@29607	607	'("have"
wenzelm@11538	608	"hence"
wenzelm@29607	609	"interpret"))
wenzelm@11538	610
wenzelm@11538	611	(defconst isar-keywords-proof-block
wenzelm@11538	612	'("next"
wenzelm@11538	613	"proof"))
wenzelm@11538	614
wenzelm@11538	615	(defconst isar-keywords-proof-open
wenzelm@11538	616	'("{"))
wenzelm@11538	617
wenzelm@11538	618	(defconst isar-keywords-proof-close
wenzelm@11538	619	'("}"))
wenzelm@11538	620
wenzelm@11538	621	(defconst isar-keywords-proof-chain
wenzelm@11538	622	'("finally"
wenzelm@11538	623	"from"
wenzelm@11538	624	"then"
wenzelm@11538	625	"ultimately"
wenzelm@11538	626	"with"))
wenzelm@11538	627
wenzelm@11538	628	(defconst isar-keywords-proof-decl
wenzelm@28280	629	'("ML_prf"
wenzelm@28280	630	"also"
wenzelm@47928	631	"include"
wenzelm@47928	632	"including"
wenzelm@11538	633	"let"
wenzelm@11538	634	"moreover"
wenzelm@11538	635	"note"
wenzelm@11538	636	"txt"
wenzelm@12926	637	"txt_raw"
wenzelm@18541	638	"unfolding"
wenzelm@36521	639	"using"
wenzelm@36521	640	"write"))
wenzelm@11538	641
wenzelm@11538	642	(defconst isar-keywords-proof-asm
wenzelm@11538	643	'("assume"
wenzelm@11538	644	"case"
wenzelm@11538	645	"def"
wenzelm@11538	646	"fix"
wenzelm@11538	647	"presume"))
wenzelm@11538	648
wenzelm@11538	649	(defconst isar-keywords-proof-asm-goal
wenzelm@17850	650	'("guess"
wenzelm@21806	651	"obtain"
wenzelm@21806	652	"show"
wenzelm@21806	653	"thus"))
wenzelm@11538	654
wenzelm@11538	655	(defconst isar-keywords-proof-script
wenzelm@11538	656	'("apply"
wenzelm@11538	657	"apply_end"
wenzelm@11538	658	"back"
wenzelm@11538	659	"defer"
wenzelm@11538	660	"prefer"))
wenzelm@11538	661
wenzelm@11538	662	(provide 'isar-keywords)

author	wenzelm
	Sun, 01 Apr 2012 22:58:05 +0200
changeset 48133	87ba9d3e1020
parent 47968	bab1c32c201e
child 48138	4c7548e7df86
permissions	-rw-r--r--